deltaW0_lt_ceiling
plain-language theorem explainer
The equilibrium BIT today-amplitude δw₀(N) stays strictly below its deep-occupancy ceiling J(φ) for every finite occupancy depth N. Anyone citing the dated w₀ band or the measure-forcing certificate needs this open upper edge. The proof unfolds the product definition and closes by nonlinear arithmetic from J(φ)>0 and saturation(N)<1.
Claim. For every natural number $N$, the equilibrium amplitude $\delta w_0(N) := J(\varphi)\cdot\mathrm{saturation}(N)$ satisfies $\delta w_0(N) < J(\varphi)$, where $J(x)=(x+x^{-1})/2-1$ is the recognition cost and $\varphi$ is the golden ratio.
background
The MeasureForcing module (T9) supplies the missing weighting rule on recognition states after the T0–T8 chain fixed the shape of the law. Any admissible weight factorizes over independent composition and obeys per-step self-similar balance, forcing the geometric φ-measure $w(n)=\varphi^{-n}$ (equivalently the Gibbs form with rate $\ln\varphi$).
Among the instance-selection problems this closes is δw₀ saturation. The free real parameter is reduced to one integer occupancy depth via $\delta w_0(N)=J(\varphi)\cdot\mathrm{saturation}(N)$. Here $J$ is the unique T5 cost $J(x)=(x+x^{-1})/2-1$, and $J(\varphi)>0$ (equivalently $J(\varphi)=(\varphi-1)^2/(2\varphi)$). The companion fact saturation_lt_one states that the saturation factor is strictly less than one at every finite $N$, so the product never attains the ceiling. The module notes that the ceiling is the deep-occupancy limit: $\delta w_0(N)\to J(\varphi)$ as occupancy deepens.
proof idea
Unfold $\delta w_0(N)$ to the product $J(\varphi)\cdot\mathrm{saturation}(N)$. Pull in the constant lemma $0<J(\varphi)$. Feed that positivity together with $\mathrm{saturation}(N)<1$ into nlinarith, which discharges the strict product inequality against the ceiling. Five-line term proof; pure arithmetic once the two strict inequalities are available.
why it matters
Direct input to the dated equilibrium band: for occupancy $N\ge 8$, $w_0=-1+\delta w_0(N)$ lies in $(-0.896,-0.88)$, jointly falsifiable with the equilibrium reading by DESI Y3+/Roman/Euclid. The strict ceiling keeps the open interval from collapsing onto $-1+J(\varphi)$. Also wired into the master measureForcingCert inhabitation.
Lives inside T9 (forced measure), downstream of T5 J-uniqueness and T6 φ as the self-similar fixed point. The H-theorem equilibrium reading of $w_0$ remains open; this inequality itself is unconditional on that reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.