deviation_ceiling
plain-language theorem explainer
Under the forced RS kernel, the dark-energy equation of state never exceeds the Carnot ceiling $-1+J(\varphi)$ at any nonnegative redshift, provided the today-amplitude lies in $[0,J(\varphi)]$. Cosmologists auditing BIT kernel falsifiers (F3) would cite this bound. The proof is a short real-inequality chain after unfolding $w_{\mathrm{RS}}=-1+\delta w_0/(1+z)$.
Claim. Let $\delta w_0,z\in\mathbb{R}$ with $\delta w_0\ge 0$, $\delta w_0\le J(\varphi)$, and $z\ge 0$. Then $w_{\mathrm{RS}}(\delta w_0,z)\le -1+J(\varphi)$, where $w_{\mathrm{RS}}(\delta w_0,z)=-1+\delta w_0/(1+z)$ and $J(x)=(x+x^{-1})/2-1$.
background
This module forces the redshift kernel in the BIT dark-energy deviation $w(z)=-1+\delta w_0\cdot K(z)$ from two premises: rung factorization of aging-charge attenuation, and single-rung balance fixing the attenuation factor at $\varphi^{-1}$. The forced kernel is $K(z)=1/(1+z)$, so the RS equation of state collapses to the explicit form $w_{\mathrm{RS}}(\delta w_0,z)=-1+\delta w_0/(1+z)$.
The recognition cost $J(x)=(x+x^{-1})/2-1$ is the unique nonnegative cost fixed by the Recognition Composition Law (T5). Its value at the golden ratio, $J(\varphi)$, is the Carnot-style ceiling on admissible today-amplitudes $\delta w_0\in(0,J(\varphi)]$. The module treats that upper endpoint as the maximum amplitude still allowed by the cost bound.
F3 is the ceiling falsifier companion to the sign falsifier no_phantom ($w\ge -1$). Together they pin $w$ inside a thin band above $-1$ for all physical $z$.
proof idea
From $z\ge 0$ one gets $1+z>0$. Nonnegativity of $\delta w_0$ and positivity of the denominator then give $\delta w_0/(1+z)\le\delta w_0$ via div_le_iff₀ and a short nlinarith. Unfolding $w_{\mathrm{RS}}$ rewrites the target as $-1+\delta w_0/(1+z)\le -1+J(\varphi)$. The already-proved division inequality plus the hypothesis $\delta w_0\le J(\varphi)$ finish the claim by linarith. No kernel-family case split is needed: the forced form is already substituted into $w_{\mathrm{RS}}$.
why it matters
F3 is one of the structural falsifiers listed in the Forced Redshift Kernel companion paper: if observations ever push $w(z)$ above $-1+J(\varphi)$ at any $z\ge 0$, the forced-kernel BIT story is dead. The bound uses the T5 uniqueness of $J$ and the forced self-similar fixed point $\varphi$ (T6) only through the amplitude ceiling $\delta w_0\le J(\varphi)$; the $z$-dependence is pure forced-kernel algebra.
The nearby section retires the $\Omega_\Lambda$-gap explanation: even at maximum admissible amplitude $\delta w_0=J(\varphi)$, certified Friedmann quadrature moves $\Omega_{\Lambda,\mathrm{eff}}$ farther from Planck, not closer. This ceiling theorem supplies the amplitude endpoint used in that numerical comparison. No downstream Lean consumers are wired yet; the result stands as a standalone observational gate on the forced kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.