probability_sums_to_one
plain-language theorem explainer
The theorem establishes that for any observer with finite positive resolution N, the epistemic probabilities over the N distinguishable outcomes sum exactly to one. Researchers formalizing probability as J-cost projection weights in deterministic ledger models cite it to secure normalization without invoking ontic randomness. The term proof reduces the sum by unfolding the probability definition, rewriting the constant sum, and applying field simplification after confirming nonzero resolution.
Claim. For any observer $obs$ with resolution $N>0$, let $p(v)$ denote the J-cost projection weight assigned to outcome $v$ in the finite set of $N$ states. Then $p(0) + p(1) + ... + p(N-1) = 1$.
background
The module PH-006 resolves probability interpretations inside Recognition Science by treating probability as an epistemic quantity arising from finite-resolution projections of a deterministic J-cost landscape. An observer is a structure equipped with a positive integer resolution $N$ (from the upstream Determinism.Observer definition: resolution : ℕ with res_pos : 0 < resolution), so that the observer distinguishes exactly N coarse-grained states. The probability of each outcome v is the normalized measure of the fiber of underlying ledger states that project to v, yielding a discrete distribution that sums to one by construction.
proof idea
The term proof first applies simp to unfold obs_probability together with the Finset sum of a constant and the cardinality of Fin N. It rewrites the resulting nsmul expression via nsmul_eq_mul, introduces the auxiliary fact that the cast of resolution to ℝ is nonzero (using Nat.cast_ne_zero and the res_pos hypothesis), and finishes with field_simp to obtain the equality.
why it matters
The result supplies the normalization step required by the RS probability structure in PH-006, where probability equals J-cost projection weight and the four classical interpretations are recovered as different readings of the same finite-resolution fibers. It directly supports the module claim that the Born rule emerges from the projection geometry rather than as an extra postulate, and it anchors the epistemic (non-ontic) character of probability in the deterministic ledger. No downstream uses are recorded yet, but the theorem closes the basic measure-theoretic requirement for any later development of relational or higher-resolution probability statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.