w0_band
plain-language theorem explainer
For any positive dark-energy amplitude up to the Carnot ceiling J(φ), today's equation-of-state sits in (−1, −0.88). Cosmologists using the forced BIT kernel or CPL thawing-line constraints would cite this band. The proof is a short linear-arithmetic reduction from the already-proved bound J(φ) < 0.12.
Claim. If $0 < \delta w_0 \le J(\varphi)$, where $J(x)=(x+x^{-1})/2-1$ is the recognition cost and $\varphi$ is the golden ratio, then $w_0:=-1+\delta w_0$ satisfies $-1 < w_0 < -0.88$.
background
In the BIT kernel shape-forcing module, dark energy is written $w(z)=-1+\delta w_0\cdot K(z)$, with $K$ forced by rung factorization and single-rung balance at $\varphi^{-1}$. At $z=0$ one has $K(0)=1$, so the today value is simply $w_0=-1+\delta w_0$.
The recognition cost $J(x)=(x+x^{-1})/2-1$ supplies the Carnot ceiling on admissible amplitudes: $\delta w_0\in(0,J(\varphi)]$. The upstream lemma jcost_phi_lt_012 records the closed form $J(\varphi)=\varphi-3/2$ and the numerical bound $J(\varphi)<0.12$, which pins the upper edge of the band at $-0.88$.
The module is the companion formalization of "The Forced Redshift Kernel." Its two premises force the kernel shape, the CPL identification, and the thawing-line sum rule $w_0+w_a=-1$; this declaration isolates the numerical today-value interval.
proof idea
Bring in the upstream bound $J(\varphi)<0.12$. Split the target conjunction and discharge each side by linear arithmetic from the hypotheses $0<\delta w_0\le J(\varphi)$ together with that strict upper bound. No kernel evaluation appears: the claim is purely about the admissible interval for the today amplitude.
why it matters
Completes the numerical half of the module's CPL package: forced kernel on the thawing line with sum rule $w_0+w_a=-1$ and $w_0\in(-1,-0.88)$. The lower edge is the no-phantom floor (the sign falsifier $w(z)\ge-1$ at every physical redshift); the upper edge is the Carnot ceiling $J(\varphi)$ descending from T5 J-uniqueness. The exact amplitude $\delta w_0\in(0,J(\varphi)]$ remains an open hypothesis of the framework. No downstream dependents are recorded; the result is a terminal observational constraint in the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.