rho_pow_nine_lt
plain-language theorem explainer
Nine steps of the forced per-step weight ρ = φ⁻¹ already leave a residual mass below 0.014, so the geometric measure saturates past 98.6% by rung nine. Cosmology and measure-forcing arguments cite this to convert closed-form saturation 1 − ρ^{N+1} into a concrete numerical floor. The proof is a two-step numerical squeeze: ρ < 0.6212 raised to the ninth power, then a decimal bound.
Claim. Let $\rho = \varphi^{-1}$ be the forced per-step recognition weight. Then $\rho^9 < 0.014$.
background
Module T9 forces the measure on recognition states after the T0–T8 shape chain. Any admissible weighting must factorize over independent composition and obey the single-step self-similar balance ρ = 1/(1+ρ); that fixed point is uniquely ρ = φ⁻¹, so lattice weights are w(n) = φ⁻ⁿ.
Here ρ is defined as 1/φ. Upstream, rho_lt_06212 supplies the decimal step bound ρ < 0.6212 (from φ > 1.61), and rho_nonneg records ρ ≥ 0 so power maps stay monotone. Saturation of rungs 0..N is the cumulative measure ∑ probMass, with closed form 1 − ρ^{N+1}; the residual ρ^{N+1} is exactly what this lemma bounds at N+1 = 9.
proof idea
Two inequalities chained by linarith. First apply pow_lt_pow_left₀ to rho_lt_06212 with nonnegativity of ρ and positive exponent 9, obtaining ρ⁹ < 0.6212⁹. Second, discharge 0.6212⁹ < 0.014 by norm_num. Transitivity finishes.
why it matters
Feeds deltaW0_near_ceiling: for N ≥ 8 one rewrites saturation 8 = 1 − ρ⁹ and uses ρ⁹ < 0.014 to get saturation 8 > 0.98, which pins δw₀(N) above 95% of the phantom-Carnot ceiling J(φ). That near-ceiling claim is the concrete payoff of T9’s geometric measure for equilibrium occupancy deeper than the eight-tick octave (T7). Without a tight residual on ρ⁹, the 5%-of-ceiling numerical statement does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.