projection_lossy
plain-language theorem explainer
Any finite-resolution observer maps distinct real states to identical observed outcomes. Probability theorists cite this to ground epistemic interpretations of randomness in deterministic J-cost dynamics. The proof is a direct term-mode construction that exhibits x=0 and y=1 and verifies both the inequality and the projection equality by normalization and simplification.
Claim. For every observer with finite positive resolution $r$, there exist distinct real numbers $x,y$ such that the coarse-grained projection of $x$ equals the projection of $y$.
background
The module resolves F-007 by separating deterministic J-cost minimization from apparent randomness. The J-cost function is strictly convex on positive reals, so each constrained ledger update possesses a unique minimizer. Finite-resolution observers, however, access only a lossy projection of the underlying state. The Observer structure packages a positive natural number resolution together with its positivity witness. The project map sends a real $x$ to the integer part of $x$ scaled by resolution, reduced modulo that resolution, landing in the finite set of distinguishable outcomes.
proof idea
The proof is a one-line term-mode construction. It instantiates the existential witness with the pair 0 and 1, splits the conjunction via constructor, discharges the inequality by norm_num, and confirms equality of the two projections by simp on the definition of project.
why it matters
This lemma is invoked verbatim by probability_from_projection and prob_is_epistemic in Philosophy.ProbabilityMeaningStructure. Those theorems pair the lossy-projection fact with the unique J-minimizer from LawOfExistence to conclude that probability is epistemic. The result therefore supplies the operational content of the F-007 resolution: deterministic dynamics appear random precisely because every observer performs a finite-resolution projection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.