probability_meaning_implies_lossy
plain-language theorem explainer
If a probability-meaning structure holds from the ledger, then every finite-resolution observer experiences lossy projection: distinct underlying states map to the same observed outcome. Foundations researchers in probability and quantum mechanics cite this to establish that apparent randomness is epistemic, arising from coarse-graining rather than ontic indeterminacy. The proof is a direct one-line application of the ledger hypothesis to the supplied observer.
Claim. Assume a probability-meaning structure derived from the ledger. Then for any observer with finite positive resolution, there exist distinct real numbers $x$ and $y$ such that the projection of $x$ equals the projection of $y$ under that observer.
background
The module PH-006 resolves probability interpretations in Recognition Science by treating probability as J-cost projection weight on a deterministic ledger. Reality has a unique J-minimizer at each step, but observers possess finite resolution. The Observer structure from Determinism is a record with a positive natural number resolution (number of distinguishable states) and a positivity proof. The project function maps any real $x$ to an element of Fin resolution by scaling, flooring, and reducing modulo the resolution count. This construction makes probability the normalized size of the preimage fiber under projection.
proof idea
The proof is a one-line term wrapper that applies the hypothesis probability_meaning_from_ledger directly to the given observer, producing the required existential pair of distinct reals with equal projections.
why it matters
This result anchors the epistemic character of probability within the Recognition framework by linking ledger determinism to observer lossiness. It supports the module's unification of frequentist (long-run fiber frequencies) and Bayesian (information-limited credence) views. The theorem fills the step showing that Born-rule-like distributions emerge from J-cost landscape projections without separate postulates, and it relies on the deterministic ledger and finite-resolution observer definitions from upstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.