probMass_tsum_one
plain-language theorem explainer
The forced geometric measure on recognition depth is a probability: the series Σ_n (1−ρ)ρ^n equals 1 for ρ=φ⁻¹. Anyone computing Shannon entropy, mean depth, or holographic event capacity of the ledger cites this normalization. The proof is a short geometric-series evaluation after factoring out the constant (1−ρ).
Claim. Let $\rho = \varphi^{-1}$. Define $P(n) = (1-\rho)\,\rho^n$ for $n\in\mathbb{N}$. Then $\sum_{n=0}^{\infty} P(n) = 1$.
background
Module T9 (MeasureForcing) closes the weighting gap left by the T0–T8 forcing chain. That chain fixes J, φ, the eight-tick period, and D=3, but not how much of reality sits in each recognition state. The module derives that any admissible weight is the geometric φ-measure: per-step factor ρ=φ⁻¹, equivalently Gibbs with rate pinned by the self-similar ledger.
Here rho is defined as $1/\varphi$. The lemmas rho_nonneg and rho_lt_one record $0\le\rho<1$, which is the open unit interval needed for geometric summability (φ>1 forces both). The normalized mass is probMass n := (1−ρ)·ρ^n, the unique probability on ℕ with that ratio.
Normalization is the missing arithmetic step before entropy and capacity identities can be stated as equalities rather than formal series.
proof idea
Unfold probMass to expose the constant factor $(1-\rho)$. Pull it out of the tsum via tsum_mul_left. The remaining series is geometric: apply tsum_geometric_of_lt_one with rho_nonneg and rho_lt_one to get $\sum\rho^n = 1/(1-\rho)$. The product collapses to 1 after a short nonzero check $1-\rho\ne 0$ (from rho_lt_one) and field_simp.
why it matters
This is the normalization half of the forced measure that T9 installs as the missing primitive behind Born weights, chirality selection, and rung occupancy. Downstream, forcedEntropy_eq in RecognitionEventCapacity uses it as the keystone: a single recognition event carries $(\varphi+2)\log\varphi$ nats, the Shannon entropy of this measure, computed from mean depth φ and this sum-to-one fact. The companion neglog_probMass rewrites $-\log P(n)=(n+2)\log\varphi$, so entropy sums become linear combinations of $\sum P(n)$ and $\sum n,P(n)$.
In the broader RS chain it sits after T5–T6 (J-uniqueness and φ as self-similar fixed point): ρ is forced to φ⁻¹ by the same reciprocal balance that forces φ, so the measure is not an extra postulate. Without this identity, holographic event capacity remains a formal series rather than a closed constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.