saturation
plain-language theorem explainer
Cumulative geometric measure on recognition rungs 0 through N: the Z-saturation fraction. Cosmology and BIT-amplitude work cite it whenever an occupancy depth must be turned into a filled fraction of the ledger. Defined as the partial sum of the forced per-rung masses; the geometric series closes to 1 − ρ^{N+1}.
Claim. For $N \in \mathbb{N}$, the saturation fraction is $\mathrm{sat}(N) := \sum_{n=0}^{N} P(n)$, where $P(n) = (1-\rho)\,\rho^n$ is the normalized probability mass at rung $n$ and $\rho = \varphi^{-1}$ is the forced per-step weight.
background
Module T9 forces the weighting on recognition states after T0–T8 have fixed the law's shape (unique J-cost, φ-scale, eight-tick period, D = 3). Any admissible weight must factorize over independent composition and obey per-step self-similar balance ρ = 1/(1+ρ), which pins ρ = φ^{-1}. The resulting discrete masses are the geometric law P(n) = (1−ρ) ρ^n.
Saturation is the cumulative of those masses from rung 0 through N. It is the natural “how full is the ledger up to depth N” quantity. Downstream objects such as the equilibrium BIT amplitude δw₀(N) = J(φ)·sat(N) reduce a free real parameter to a single integer occupancy depth via this cumulative.
proof idea
Pure definition: sum probMass n over Finset.range (N+1). No tactics. The adjacent closed-form remark follows at once from the finite geometric series: ∑_{n=0}^N (1−ρ) ρ^n = 1 − ρ^{N+1} (using 0 < ρ < 1).
why it matters
This is the primitive that turns the forced geometric measure into a depth-dependent filled fraction. In-module it feeds deltaW0, deltaW0_gt_004, and deltaW0_near_ceiling, collapsing today's BIT amplitude to J(φ) times saturation at integer N. Cosmology uses it for baryon-asymmetry rung arithmetic (eta_B_rung, saturation_exponent), phase-saturation vacuum consistency (cosmic_phase_equilibrium_consistent, no_dark_energy_evolution), and the reionization epoch ladder (the saturation constructor). It is the concrete projection of T9's missing weighting rule onto every instance-selection problem the module was written to close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.