deltaW0_gt_004
plain-language theorem explainer
For every occupancy depth N, the equilibrium today-amplitude δw₀(N) strictly exceeds 0.04. Cosmologists comparing RS equilibrium occupancy to ΛCDM cite this bound: exact w₀ = −1 is incompatible with any finite N. The proof multiplies the closed lower bounds J(φ) > 0.11 and saturation(N) ≥ saturation(0) > 0.37.
Claim. For every natural number $N$, the equilibrium BIT today-amplitude satisfies $\delta w_0(N) > 0.04$, where $\delta w_0(N) = J(\varphi)\cdot\mathrm{saturation}(N)$, $J$ is the unique cost, and $\mathrm{saturation}(N)$ is the cumulative $\varphi$-measure of rungs $0..N$.
background
Module T9 forces the weighting on recognition states: any admissible lattice weight factorizes and obeys per-step self-similar balance, hence $w(n)=\varphi^{-n}$. The forced step weight is $\rho=\varphi^{-1}$.
The equilibrium today-amplitude is defined by $\delta w_0(N)=J(\varphi)\cdot\mathrm{saturation}(N)$, reducing the free real $\delta w_0$ to one integer occupancy depth. Here $J(\varphi)$ is the cost at the golden ratio (forced by T5/T6), and saturation is the cumulative measure of rungs $0..N$.
Upstream numerical pins used below: $J(\varphi)>0.11$ and $\rho<0.6212$. Saturation is monotone in $N$ and has a closed form at $N=0$ controlled by $\rho$.
proof idea
Monotonicity of saturation from $0\le N$ gives $\mathrm{saturation}(0)\le\mathrm{saturation}(N)$. At $N=0$, the closed form plus $\rho^{1}=\rho$ and $\rho<0.6212$ yield $\mathrm{saturation}(0)>0.37$, hence the same lower bound for every $N$. Unfold $\delta w_0(N)=J(\varphi)\cdot\mathrm{saturation}(N)$ and apply nonlinear arithmetic to the product of $J(\varphi)>0.11$ and $\mathrm{saturation}(N)>0.37$, which exceeds $0.04$.
why it matters
Feeds the master certificate measureForcingCert in the same module, which packages lattice forcing, continuum Gibbs form, and nonvacuity for T9. Doc-comment states the observational bite: equilibrium excludes exact ΛCDM; a confirmed $|w_0+1|<0.04$ would falsify equilibrium T9 occupancy (not T9 itself). Sits downstream of the forcing chain landmarks T5 (J-uniqueness) and T6 ($\varphi$ fixed point), which pin $J(\varphi)$ and $\rho=\varphi^{-1}$ used in the bound. Closes one recurring instance-selection gap named in the module doc: $\delta w_0$ saturation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.