saturation_closed
plain-language theorem explainer
The cumulative geometric measure on recognition rungs 0 through N equals 1 minus ρ to the power N+1, with ρ = φ⁻¹ the forced per-step weight. Foundation and cosmology workers cite it whenever a Z-saturation fraction must become an explicit closed form. The proof evaluates the finite geometric series of normalized probability masses and simplifies.
Claim. For every natural number $N$, the cumulative measure of rungs $0,\ldots,N$ equals $1-\rho^{N+1}$, where $\rho=\varphi^{-1}$ is the forced per-step recognition weight and the mass at rung $n$ is $(1-\rho)\rho^n$.
background
Module T9 forces the weighting on recognition states after the T0–T8 chain has fixed the law's shape (J-cost, φ, eight-tick period, D=3). Any admissible weight factorizes over independent steps and obeys the reciprocal self-similarity balance, which pins the per-step factor to $\rho=\varphi^{-1}$.
The normalized mass at rung $n$ is $P(n)=(1-\rho)\rho^n$. Saturation at depth $N$ is the partial sum of those masses from $0$ through $N$: the Z-saturation fraction used later for equilibrium $\delta w_0$ bounds. Because $0<\rho<1$, the series is geometric with ratio not equal to one, so a closed form is available.
proof idea
Unfold saturation to the Finset sum of probMass, then unfold each mass to $(1-\rho)\rho^n$. Factor $(1-\rho)$ out of the sum and apply the standard finite geometric-sum identity (justified by $\rho\neq 1$). The remaining algebraic identity $(1-\rho)\cdot(1-\rho^{N+1})/(1-\rho)=1-\rho^{N+1}$ is discharged by a nonzero-denominator check on $\rho-1$, then field_simp and ring.
why it matters
Closed-form saturation is the computational hinge for the whole equilibrium-occupancy side of T9. Downstream, saturation_lt_one, saturation_monotone, and saturation_tendsto_one are one-line rewrites of this identity; they feed the $\delta w_0$ theorems that exclude exact ΛCDM under equilibrium reading ($\delta w_0(N)>0.04$ for every $N$) and pin deep occupancy ($N\ge 8$) within 5% of the phantom-Carnot ceiling $J(\varphi)$. Without the closed form those comparisons stay symbolic sums. It sits inside the forced geometric $\varphi$-measure, the missing weighting primitive after T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.