omega_gap_explanation_retired
plain-language theorem explainer
The BIT correction cannot close the Planck–RS Ω_Λ gap: at maximum admissible amplitude the corrected fraction lies strictly below the bare RS value and outside Planck 1σ in the adverse direction, while the forced kernel keeps w(z) ≥ −1. Cosmologists comparing the RS dark-energy prediction to DESI/Euclid cite this as the structural kill of the gap-explanation hypothesis. Proof is certified numerical comparison of the three constants plus the no-phantom lemma.
Claim. The maximum-amplitude BIT-corrected dark-energy fraction is strictly less than the bare RS value $\Omega_\Lambda^{\mathrm{bare}}$, its absolute deviation from the Planck central value exceeds one Planck $\sigma$ (adverse side), and for every amplitude $dw_0 \ge 0$ and redshift $z > -1$ one has $w_{\mathrm{RS}}(dw_0,z) \ge -1$.
background
This module forces the BIT dark-energy kernel from two premises: rung factorization (attenuation across $m+n$ φ-rungs multiplies) and single-rung balance (one rung attenuates by the fixed point of $\rho=1/(1+\rho)$, namely $\varphi^{-1}$). The forced law is $K(z)=1/(1+z)$ on the lattice $1+z=\varphi^n$, which is exactly CPL on the thawing line $w_a=-(1+w_0)$ with $w_0\in(-1,-0.88)$.
The bare RS fraction is the numerical constant $\Omega_\Lambda^{\mathrm{bare}}=11/16-\alpha/\pi\approx 0.685177$. The corrected maximum-amplitude value is the Friedmann quadrature of the forced kernel at the largest admissible $dw_0$. Planck central and $\sigma$ are the usual observational anchors. Upstream, no_phantom already proves the sign bound: under non-negative amplitude and physical redshift, $w_{\mathrm{RS}}(dw_0,z)\ge -1$.
proof idea
Term-mode conjunction via refine ⟨?, ?, ?⟩.
- First conjunct: direct
norm_numon the two certified realsomega_lambda_corrected_max_amplitudeandomega_lambda_bare. - Second: rewrite the absolute value with
abs_of_neg(the corrected value sits below Planck central, again bynorm_num), thennorm_numagainstplanck_sigma. - Third: pointwise application of the already-proved
no_phantomlemma (non-negative amplitude and $z>-1$ imply $w\ge -1$).
No new analysis; the numerical certificates and the sign falsifier do all the work.
why it matters
This is the module's retirement certificate for the hypothesis that BIT aging closes the Planck–RS $\Omega_\Lambda$ gap. The master one-statement summary of the paper (dated 2026-06-09) records the forced kernel $K(z)=1/(1+z)$, the CPL thawing segment, and no phantom crossing, to be adjudicated by DESI Y3+/Roman/Euclid; the present theorem is the explicit structural kill of the gap story inside that package.
Because the forced kernel pins the deviation sign ($w\ge -1$) and the max-amplitude quadrature moves $\Omega_\Lambda$ away from Planck, neither shape nor amplitude freedom remains to flip the direction. The result sits at the end of the forcing chain that begins with rung dilution and the single-rung $\varphi^{-1}$ balance (T6 φ fixed point in the broader RS chain). Open remainder of the module: the today-amplitude $dw_0\in(0,J(\varphi)]$ and the BIT mechanism hypothesis itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.