saturation_monotone
plain-language theorem explainer
The cumulative geometric measure of recognition rungs 0 through N is monotone nondecreasing in the depth N. Cosmologists and RS auditors cite it when lower-bounding the equilibrium dark-energy deviation δw₀ away from ΛCDM and toward the phantom-Carnot ceiling. The proof rewrites both sides by the closed form 1−ρ^{N+1} and applies the standard power inequality for 0≤ρ≤1.
Claim. The saturation map $N \mapsto S(N)$ is monotone nondecreasing on $\mathbb{N}$: if $N \le M$ then $S(N) \le S(M)$, where $S(N) = 1 - \rho^{N+1}$ is the cumulative measure of rungs $0,\ldots,N$ and $\rho = \varphi^{-1}$.
background
Module T9 forces the weighting on recognition states once T0–T8 have fixed the shape of the law (J-cost, φ, eight-tick period, D=3). Any admissible weight factorizes over independent steps and obeys the single-step self-similar balance ρ=1/(1+ρ), which pins ρ=φ⁻¹. The resulting lattice weights are w(n)=ρ^n=φ⁻ⁿ.
Saturation is the partial sum of the normalized geometric masses on rungs 0..N. Its closed form is S(N)=1−ρ^{N+1}, obtained from the finite geometric series and ρ≠1. Because 0≤ρ≤1, the residual tail ρ^{N+1} shrinks with N, so the occupied fraction can only grow.
Upstream facts used here are exactly those bounds: ρ=1/φ, ρ≥0, and ρ≤1, together with the closed-form identity for saturation.
proof idea
Term-mode proof. Fix N≤M. Rewrite both saturations by the closed form S(K)=1−ρ^{K+1}. The needed comparison reduces to ρ^{M+1}≤ρ^{N+1}. That inequality is pow_le_pow_of_le_one applied to the already-proved facts ρ≥0 and ρ≤1, with the exponent relation M+1≥N+1 discharged by omega. A final linarith finishes the arithmetic.
why it matters
Saturation monotonicity is the elementary comparison that lets deeper occupancy only increase the cumulative measure. Downstream, deltaW0_gt_004 invokes it at N≥0 to obtain the uniform lower bound δw₀(N)>0.04, so equilibrium T9 occupancy can never sit inside a |w₀+1|<0.04 window (a confirmed tighter measurement would falsify equilibrium occupancy, not T9 itself). Likewise deltaW0_near_ceiling uses the same monotone growth past N=8 to pin δw₀ within 5% of the phantom-Carnot ceiling J(φ).
In the broader forcing chain this is a T9 lattice lemma: once the geometric φ-measure is forced, cumulative occupancy is automatically ordered by depth, which converts rung-count hypotheses into quantitative dark-energy amplitude bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.