frequentist_vindicated
plain-language theorem explainer
The theorem establishes that the projection map from real states to finite-resolution observer outcomes is deterministic, so long-run frequencies of outcomes depend only on input distribution and fiber structure. Researchers grounding frequentist statistics in deterministic ledger models would cite it. The proof is a direct rewriting that substitutes the input equality into the projection definition.
Claim. For any observer with positive finite resolution and any real number $x$, the projection satisfies: for all real $y$, if $x = y$ then the projected value of $x$ equals the projected value of $y$, where the projection maps $x$ to the floor of $x$ scaled by resolution, taken modulo the resolution.
background
The module resolves probability interpretations under Recognition Science by treating probability as J-cost projection weight. Reality remains deterministic at the ledger level while observers apply finite coarse-graining. The Observer structure is a positive integer resolution counting distinguishable states. The project map is defined by scaling the input by this resolution, taking the floor, and reducing modulo the resolution to produce an element of the finite set of outcomes.
proof idea
The term proof introduces the equality hypothesis and rewrites the goal by substitution. This yields immediate reflexivity because the projection definition depends only on the input value. No additional lemmas are invoked beyond the definition of project.
why it matters
The result completes the frequentist vindication step inside the PH-006 module on probability meaning. It confirms that long-run frequencies are objective properties fixed by the deterministic projection fibers, consistent with the ledger factorization and observer forcing upstream. The module uses this to unify interpretations while keeping probability epistemic rather than ontic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.