saturation_tendsto_one
plain-language theorem explainer
Saturation of occupancy depth tends to 1 at infinity: deep stacks exhaust the available measure. Cosmology and measure-forcing arguments that pin δw₀ to its J(φ) ceiling cite this limit. The proof rewrites saturation as 1 − ρ^{N+1} and applies geometric decay of ρ = φ⁻¹ < 1.
Claim. Let $\rho = \varphi^{-1}$ be the forced per-step weight and let $\mathrm{sat}(N) = 1 - \rho^{N+1}$ be the closed-form saturation at occupancy depth $N$. Then $\mathrm{sat}(N) \to 1$ as $N \to \infty$ in the standard topology on $\mathbb{R}$.
background
Module T9 forces the weighting on recognition states after the T0–T8 chain has fixed the shape of the law (unique cost $J$, scale $\varphi$, eight-tick period, $D=3$). Any admissible weight factorizes over independent composition and obeys per-step self-similar balance, which pins the single-step factor to $\rho = \varphi^{-1}$.
Saturation is the cumulative occupancy measure built from that geometric weight. The closed form used here is $\mathrm{sat}(N) = 1 - \rho^{N+1}$, so the residual unoccupied mass is exactly one more power of $\rho$. Upstream facts $\rho \ge 0$ and $\rho < 1$ (from $\varphi > 1$) make the residual a standard geometric sequence tending to zero.
Downstream, the equilibrium BIT today-amplitude is $\delta w_0(N) = J(\varphi),\mathrm{sat}(N)$, so this limit is the bridge from integer depth $N$ to the continuous ceiling $J(\varphi)$.
proof idea
Pointwise rewrite saturation via the closed form: $\mathrm{sat} = N \mapsto 1 - \rho^{N+1}$ (function extensionality on saturation_closed). The power map $N \mapsto \rho^{N+1}$ tends to $0$ at infinity by Mathlib's tendsto_pow_atTop_nhds_zero_of_lt_one applied to $\rho \ge 0$, $\rho < 1$, composed with the shift $N \mapsto N+1$. Subtract from the constant sequence $1$ to obtain convergence to $1-0=1$, then simplify.
why it matters
Closes the deep-occupancy half of the T9 measure story: once the geometric $\varphi$-measure is forced, stacking enough recognition steps exhausts residual mass, so saturation saturates. The sole direct consumer is deltaW0_tendsto_ceiling, whose doc states "$\delta w_0(N) \to J(\varphi)$: the ceiling is the deep-occupancy limit." That theorem is a constant-multiple of the present limit, reducing the free real $\delta w_0$ to a single integer depth times the already-forced cost $J(\varphi)$.
In the broader framework this is the measure-side counterpart of T5–T6 uniqueness: $J$ and $\varphi$ fix the cost and scale; saturation-to-one says the ledger has no leftover continuum weight once occupancy is deep. It feeds every later instance-selection projection that quotes $\delta w_0$ saturation (Born weights, chirality, $\eta_B$ prefactor, rung occupancy).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.