probability_meaning_from_ledger
plain-language theorem explainer
Every finite-resolution observer experiences lossy projection, with distinct real states mapping to the same observed value. Researchers on epistemic interpretations of probability in deterministic frameworks cite this as the origin of apparent randomness. The declaration packages the forall-exists claim directly as the core property of the meaning structure.
Claim. For every observer $obs$ with finite positive resolution, there exist distinct reals $x,y$ such that the projection of $x$ and of $y$ under $obs$ coincide.
background
The module develops the Recognition Science resolution of probability interpretations. Reality remains deterministic with a unique J-minimizer at each ledger step, yet observers possess only finite resolution. Probability therefore equals J-cost projection weight and is epistemic rather than ontic. The module doc states that the probability of an outcome is the measure of the fiber of states mapping to it under the observer's coarse-graining. Observer is the structure from the Determinism module requiring a positive natural number resolution. The project function maps any real to one of the finite bins by scaled floor and modulo, and its doc notes that multiple distinct states map to the same observation, the origin of apparent randomness.
proof idea
The declaration is a direct definition that sets the proposition equal to the forall-exists statement of lossy projection. No lemmas or tactics are invoked; the body simply records the mathematical content of finite-resolution collapse.
why it matters
This definition supplies the property invoked by probability_meaning_structure and probability_meaning_implies_lossy. It fills the module's step showing that probability arises from observer coarse-graining in a deterministic ledger, unifying frequentist long-run frequencies with Bayesian information states without separate postulates. It anchors the RS claim that the Born rule emerges from the J-cost landscape rather than being imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.