probability_is_relational
plain-language theorem explainer
The number of distinct probability bins equals an observer's finite resolution, so probability partitions the state space according to the observer rather than being intrinsic to the underlying deterministic dynamics. Researchers resolving frequentist, Bayesian, and propensity interpretations in deterministic frameworks cite this to show that probability is epistemic and resolution-dependent. The proof is a one-line wrapper that introduces the observer and simplifies the cardinality identity.
Claim. For any observer with finite positive resolution $n$, the cardinality of the set of distinguishable states equals $n$: $|$Fin$(n)| = n$.
background
The module PH-006 resolves probability interpretations inside Recognition Science by treating probability as J-cost projection weight onto a finite-resolution observer. Reality remains deterministic with a unique J-minimizer at each ledger step; observers merely coarse-grain the state. The Observer structure (imported from Determinism) is defined as a record with field resolution : ℕ together with the positivity hypothesis 0 < resolution. Probability of outcome v is then the normalized measure of the fiber of states that project to v under the observer's partition.
proof idea
The proof is a one-line wrapper. It introduces the observer variable and applies simp, which reduces the Fintype.card (Fin obs.resolution) identity directly to the definition of Fin and the cardinality of a finite initial segment.
why it matters
This theorem supplies the formal content for the module's claim that probability is relational and epistemic rather than ontic. It supports the unification of the four interpretations by grounding fiber cardinality in observer resolution, which in turn feeds the J-cost-weighted measure used for Born-rule emergence. It sits downstream of the deterministic ledger and ObserverForcing structures and upstream of the vindication theorems for frequentist and Bayesian views within the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.