equilibrium_w0_band
plain-language theorem explainer
For occupancy N at least 8, the equilibrium dark-energy equation of state sits in the open interval (−0.896, −0.88). Cosmologists comparing the Recognition Science BIT prediction to DESI Y3+, Roman, or Euclid would cite this dated band. The argument sandwiches the δw₀ correction between a near-ceiling lower bound (N≥8) and a strict ceiling, using the known 0.11 < J(φ) < 0.12 window, then closes both sides by linear arithmetic.
Claim. For every natural number $N \ge 8$, writing $w_0 = -1 + \delta w_0(N)$ for the equilibrium dark-energy equation-of-state parameter, one has $-0.896 < w_0 < -0.88$.
background
Module T9 (MeasureForcing) closes the missing weighting rule on recognition states after the T0–T8 shape chain: any admissible weight is the geometric φ-measure, equivalently the Gibbs rule with rate fixed by the self-similar ledger. Among the certificate items is the δw₀ reduction for the BIT dark-energy kernel: the today-value correction is bounded, monotone, tends to J(φ), stays above 0.04, and sits near its ceiling once occupancy N is at least 8.
Here J is the unique recognition cost J(x)=(x+x^{-1})/2−1 forced at T5; on the golden ratio one has the closed form J(φ)=φ−3/2. Upstream lemmas pin the Carnot ceiling in a tight numerical window: J(φ)>0.11 and J(φ)<0.12 (the latter is jcost_phi_lt_012). The equilibrium reading identifies w₀=−1+δw₀(N), so those cost bounds translate into a concrete open band for w₀ once δw₀ is known to be near and strictly below its ceiling.
proof idea
Term-mode proof that first records four numeric facts: the near-ceiling lower bound on δw₀ for N≥8, the strict upper bound δw₀ below its ceiling (any N), the lower sandwich J(φ)>0.11, and the upstream theorem that J(φ)<0.12. The goal is the conjunction of two strict inequalities on −1+δw₀(N). constructor splits them; each side is discharged by nlinarith from the four recorded inequalities. No new algebraic identity is proved here; the work is assembling the ceiling lemmas with the J(φ) window.
why it matters
This is the dated equilibrium band (2026-06-09) listed as item 10 of the T9 master certificate and restated inside the one-statement theorem t9_measure_forced: the forced measure reduces the BIT amplitude to a single integer N with equilibrium band w₀∈(−0.896,−0.88) for N≥8. Downstream, measureForcingCert packages the band with lattice forcing, continuum uniqueness, Gibbs form, partition Z=φ², and cost-blindness.
In the broader chain it sits after T5 (J uniqueness), T6 (φ forced), and the BIT kernel shape forcing that already pinned K(z). The doc-comment is explicit that the reading is conditional on the still-open H-theorem equilibrium hypothesis; the band and that hypothesis are jointly falsified if DESI Y3+, Roman, or Euclid land outside (−0.896,−0.88).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.