probability_from_projection
plain-language theorem explainer
Any finite-resolution observer in Recognition Science maps distinct real states to the same observed outcome, establishing that probability arises as epistemic uncertainty over the fiber of indistinguishable states rather than ontic randomness. Foundations researchers resolving quantum interpretations or probability meanings would cite this for the operational definition prob(v) equals fiber measure over total measure. The proof is a direct one-line application of the lossy projection result.
Claim. For any observer with finite positive resolution, there exist distinct real numbers $x$ and $y$ such that the observer's projection map sends both to the same observed bin.
background
The module PH-006 resolves probability interpretations in Recognition Science by showing probability equals J-cost projection weight. Reality remains deterministic with a unique J-minimizer at each ledger step, yet observers possess finite resolution and therefore see only a coarse-grained projection of the underlying state. An observer is defined as a structure carrying a positive integer resolution that counts distinguishable states; the projection map bins any real input $x$ into one of those resolution slots via floor scaling and modulo reduction.
proof idea
The proof is a one-line wrapper that applies the projection_lossy theorem to the supplied observer.
why it matters
This result supplies the RS operational definition of probability inside the philosophy module that unifies frequentist, Bayesian, and propensity views under epistemic projection. It directly supports the module's claim that probability is epistemic rather than ontic, consistent with the deterministic foundation and the J-cost landscape structure. The declaration closes the step showing apparent randomness originates in finite observer resolution without introducing new postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.