deltaW0
plain-language theorem explainer
The equilibrium BIT today-amplitude at occupancy depth N is J(φ) times the cumulative Z-saturation through rung N. Cosmologists and RS auditors cite it when placing the dark-energy deviation δw₀ under the equilibrium reading of T9. The free real amplitude collapses to a single integer depth. Definition is a one-line product of the forced golden-ratio cost and the geometric measure sum.
Claim. For each natural number $N$, define the equilibrium today-amplitude by $\delta w_0(N) = J(\varphi)\, S(N)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost and $S(N)=\sum_{n=0}^{N}\mathrm{probMass}(n)$ is the cumulative measure of rungs $0$ through $N$ (equivalently $S(N)=1-\rho^{N+1}$).
background
Module T9 forces the weighting on recognition states after T0–T8 have fixed the shape of the law (unique J, unique φ, eight-tick period, D=3). The missing primitive is which measure sits on the allowed states. Lattice premises (factorization over independent steps, per-step self-similar balance ρ=1/(1+ρ)) force the geometric weights w(n)=φ^{-n}, with ρ=φ^{-1}.
The recognition cost is J(x)=(x+x^{-1})/2-1, the unique T5 cost; J(φ) is the fixed positive scale that multiplies amplitudes here. Saturation S(N) is the cumulative measure of rungs 0..N, with closed form 1-ρ^{N+1}, so S(N)↑1 as N→∞ and never equals 1 for finite N.
Under the equilibrium reading, today's dark-energy deviation from −1 is identified with this product: the free real δw₀ is reduced to the single integer occupancy depth N.
proof idea
Pure definition: unfold to the product of Cost.Jcost at Constants.phi and saturation N. No tactics, no lemmas. Downstream bounds rewrite via this unfold, then apply positivity of J(φ), saturation_lt_one, saturation_monotone, and the closed form of saturation.
why it matters
Anchors the equilibrium cosmology side of T9. Parent results include deltaW0_lt_ceiling (never reaches J(φ)), deltaW0_tendsto_ceiling (deep-occupancy limit is the phantom-Carnot ceiling), deltaW0_gt_004 (excludes exact ΛCDM: δw₀(N)>0.04 for every N), and deltaW0_near_ceiling (N≥8 pins within 5% of the ceiling). Those feed equilibrium_w0_band: for N≥8, w₀=−1+δw₀(N) lies in (−0.896,−0.88), dated 2026-06-09 and jointly falsifiable with the equilibrium reading by DESI Y3+/Roman/Euclid. Also appears in MeasureForcingCert and t9_measure_forced. Landmark link: T5 J-uniqueness and T6 φ fix the prefactor; the geometric measure is the T9 output. Open: the H-theorem/equilibrium reading itself remains conditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.