no_phantom
plain-language theorem explainer
Under the forced RS dark-energy equation of state with non-negative amplitude, w(z) never drops below −1 at any physical redshift. Cosmologists cite this as the F1 sign falsifier ruling out phantom crossing for the BIT kernel. The proof is a four-line positivity argument: the correction term is a non-negative quotient once 1+z>0.
Claim. If $\delta w_0 \ge 0$ and $z > -1$, then the forced RS equation of state satisfies $w_{\mathrm{RS}}(\delta w_0,z) \ge -1$, where $w_{\mathrm{RS}}(\delta w_0,z) := -1 + \delta w_0/(1+z)$.
background
The module forces the BIT dark-energy kernel from two premises: rung factorization (attenuation multiplies across independent φ-rungs) and single-rung balance (one rung attenuates by φ⁻¹, the unique positive fixed point of ρ = 1/(1+ρ)). The resulting occupation law is occ n = φ⁻ⁿ, which on the lattice 1+z = φⁿ is exactly 1/(1+z).
The RS equation of state under that forced kernel is defined by w_RS(δw₀, z) := −1 + δw₀/(1+z). Equivalently it is the CPL segment with w₀ = −1 + δw₀ and wₐ = −δw₀, lying on the thawing line wₐ = −(1+w₀). Physical redshifts obey z > −1, so the denominator 1+z is strictly positive.
Phantom crossing would mean w < −1 somewhere. The present result is the elementary sign bound that blocks that under non-negative amplitude.
proof idea
From z > −1 obtain 1+z > 0 by linarith. Non-negativity of the quotient δw₀/(1+z) then follows from div_nonneg applied to δw₀ ≥ 0 and 1+z > 0. Unfold the definition w_RS = −1 + δw₀/(1+z) and finish by linarith: adding a non-negative term to −1 cannot go below −1.
why it matters
This is the F1 sign falsifier listed in the module consequences: under the forced kernel, w(z) ≥ −1 at every physical redshift. It is conjoined into bit_kernel_shape_one_statement, the dated one-statement summary that packages rung dilution, s=1 pinning, CPL thawing geometry, the w₀ band, and no phantom crossing for DESI Y3+/Roman/Euclid adjudication.
It is also the third conjunct of omega_gap_explanation_retired. That retirement certificate uses the forced sign (together with certified Friedmann quadrature bounds) to kill the hypothesis that BIT could close the Planck–RS Ω_Λ gap: the correction always moves Ω_Λ in the adverse direction, and no shape freedom remains to flip the sign.
Within the broader RS chain the kernel shape itself traces to φ-rung self-similarity (T6) and cost additivity; the present lemma is the elementary inequality that turns that shape into a clean observational veto on phantom DE.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.