Observer
plain-language theorem explainer
Finite-resolution observers coarse-grain deterministic ledger states into a finite number of bins, producing the appearance of randomness from unique J-cost minimizers. Researchers deriving quantum probabilities from classical determinism cite this structure when projecting the unique next state onto an observer's resolution. The definition is a direct structure with a single field for positive natural-number resolution.
Claim. An observer is a structure consisting of a positive integer $resolution > 0$ that sets the number of distinguishable coarse-grained states visible to the observer.
background
The Determinism module formalizes F-007 by showing that strict convexity of the J-cost function forces unique minimizers for ledger updates, hence deterministic dynamics. Apparent randomness arises when a finite-resolution observer projects these unique states onto a coarse grid. J-cost is the recognition cost function whose second derivative is positive, ensuring convexity. Upstream, the ObserverForcing.Observer equips a coherent recognition structure with a persistent reference event. The phi-ladder places physical quantities on discrete tiers scaled by powers of phi.
proof idea
Direct structure definition introducing the resolution field and the positivity hypothesis res_pos.
why it matters
This definition supplies the finite-resolution observer required by the projection theorems in the same module, which establish that distinct deterministic states can map to the same observation. It feeds the ObserverForcing results that construct observers from nontrivial recognition streams. In the framework it realizes the step from deterministic J-cost minimization (T5 uniqueness) to the emergence of Born-rule probabilities for finite observers, closing part of the determinism question F-007.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.