project
plain-language theorem explainer
The project definition supplies the map sending a real deterministic state x to its observed value in the finite set of cardinality equal to the observer's resolution. Researchers working on the emergence of apparent randomness from deterministic underlying dynamics cite this construction. The definition is realized by scaling x by the resolution, taking the floor, reducing modulo the resolution, and verifying the result lies in the correct Fin interval via the standard Nat.mod_lt lemma.
Claim. For an observer with positive integer resolution $n$, the projection map sends a real number $x$ to the element of the finite set $0,1,…,n-1$ given by $⌊x n⌋ mod n$.
background
In the Determinism module an Observer is a structure consisting of a positive integer resolution together with a proof that the resolution is positive. This captures a finite-resolution measurement device that can distinguish only n distinct states. The module F-007 argues that the universe is deterministic because the J-cost function is strictly convex, forcing unique minimizers for ledger updates. However, an observer with finite resolution sees only the projection of the true state, which produces the appearance of randomness. Upstream, the same Observer structure appears in ObserverForcing as a coherent recognition equipped with a persistent reference event.
proof idea
The definition is a direct construction: scale the input real by the observer resolution, apply the floor function, convert to natural number, reduce modulo the resolution, and supply the proof that the remainder is strictly less than the resolution using Nat.mod_lt.
why it matters
This definition is the technical core of the argument that apparent randomness arises from lossy observation of a deterministic process. It is used directly by the projection_lossy theorem, which exhibits distinct reals that map to the same observed state. In the broader framework it supports the claim that the Born rule emerges as the statistics of J-cost minimization projected onto finite resolution, consistent with the eight-tick octave and phi-ladder structure of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.