deltaW0_near_ceiling
plain-language theorem explainer
For occupancy N ≥ 8, the equilibrium dark-energy amplitude δw₀(N) sits strictly above 95% of the phantom-Carnot ceiling J(φ). Anyone citing the dated RS equilibrium w₀ band uses this lower pin. The proof lifts a numerical saturation bound at the eight-tick floor by monotonicity, then multiplies by the positive cost J(φ).
Claim. For every natural number $N \ge 8$, the equilibrium amplitude satisfies $\delta w_0(N) > 0.95\, J(\varphi)$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost and $\varphi$ is the golden-ratio fixed point.
background
Module T9 (MeasureForcing) closes the weighting gap left by the T0–T8 chain: once J, φ, the eight-tick period, and D = 3 are forced, one still needs the measure on recognition states. The lattice layer forces the geometric rule w(n) = φ^{-n} from factorization plus the self-similar balance ρ = 1/(1+ρ), which pins ρ = φ^{-1}.
Saturation is the cumulative geometric weight up to occupancy N (approaching 1 as N grows). The amplitude δw₀(N) is that saturation times the single-step cost J(φ); the equation-of-state parameter is then read as w₀ = −1 + δw₀(N). The phantom-Carnot ceiling is the fully saturated value J(φ) itself.
Upstream positivity J(φ) > 0 is the standard cost lemma (φ ≠ 1), and the closed-form saturation identity plus the bound ρ^9 < 0.02 supply the numerical floor at the eight-tick rung.
proof idea
First show saturation(8) > 0.98: rewrite via the closed saturation formula, reduce ρ^{8+1} to ρ^9, and apply the pre-proved bound ρ^9 < 0.02 with linarith. Monotonicity of saturation in N (from hN : 8 ≤ N) lifts the inequality to saturation(N) > 0.98. Invoke J(φ) > 0. Unfold δw₀ (which is saturation · J(φ)) and finish by nlinarith: 0.98 > 0.95 and positivity of J give the strict 0.95 · J(φ) lower bound.
why it matters
This is the lower half of the pin that feeds equilibrium_w0_band: for N ≥ 8 one obtains w₀ = −1 + δw₀(N) ∈ (−0.896, −0.88). That band is the dated (2026-06-09) equilibrium prediction, conditional on the still-open H-theorem reading of equilibrium, and jointly falsifiable by DESI Y3+/Roman/Euclid if w₀ lands outside.
Framework-wise it sits on the eight-tick octave (T7): the numerical ceiling is already within 2% at N = 8, so deeper occupancy only tightens the amplitude toward J(φ). Together with the matching upper bound δw₀ < J(φ), it converts the forced φ-measure into a concrete cosmological observable window rather than a free dark-energy parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.