saturation_lt_one
plain-language theorem explainer
Under the forced geometric φ-measure, the cumulative weight of rungs 0 through N is strictly less than 1 for every finite N. Cosmology and ledger bounds that need a strict Z-saturation gap cite this. The proof is a three-line rewrite to the closed form 1−ρ^{N+1} plus positivity of ρ=φ^{-1}.
Claim. For every natural number $N$, the cumulative geometric measure of rungs $0,\ldots,N$ satisfies $\mathrm{sat}(N)<1$. Equivalently, with $\rho=\varphi^{-1}$, one has $1-\rho^{N+1}<1$.
background
Module T9 closes the missing weighting rule on recognition states after the T0–T8 shape chain. Any admissible weight factorizes over independent composition and obeys per-step self-similar balance, forcing the single-step weight $\rho=\varphi^{-1}$ and lattice weights $w(n)=\varphi^{-n}$.
Here $\rho$ is defined as $1/\varphi$. The saturation of the first $N+1$ rungs is the partial sum of the normalized geometric masses on those rungs; its closed form is $\mathrm{sat}(N)=1-\rho^{N+1}$ (from the finite geometric series and $\rho\neq 1$). The Z-saturation fraction is therefore the residual mass beyond rung $N$, namely $\rho^{N+1}$.
Upstream facts used directly: positivity of $\rho$ and the closed-form identity for saturation.
proof idea
Term-mode proof in three steps. Rewrite the goal by the closed form $\mathrm{sat}(N)=1-\rho^{N+1}$. Produce the side fact $0<\rho^{N+1}$ from $\mathrm{pow_pos}$ applied to $\rho>0$. Finish by linear arithmetic: subtracting a positive quantity from 1 yields a strict upper bound of 1.
why it matters
Strict incompleteness of any finite rung window is the quantitative content of geometric dilution under the forced measure. Downstream, deltaW0_lt_ceiling uses this inequality (with positivity of $J(\varphi)$) to prove that the $\delta w_0$ defect never reaches the $J$-cost ceiling: the saturation gap keeps the weighted defect strictly below the ledger bound.
In the T9 program this is the elementary strictness lemma behind every “never saturates” claim (Born weights, chirality selection, $\delta w_0$, rung occupancy). It is the finite-$N$ shadow of the infinite geometric series summing to 1 only in the limit, pinned by $\rho=\varphi^{-1}$ from T6 self-similarity rather than by an external temperature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.