omega_lambda_interval
plain-language theorem explainer
The dark-energy fraction sits strictly inside (0.683, 0.686). Cosmologists citing the RS Ω_Λ prediction against Planck 2018 use this numeric window. The proof is a one-line pairing of the already-proved lower and upper bounds on 11/16 − α/π.
Claim. The RS dark-energy density parameter $\Omega_\Lambda = 11/16 - \alpha/\pi$ satisfies $0.683 < \Omega_\Lambda < 0.686$.
background
This module derives the cosmological-constant fraction from phase saturation in the eight-tick ledger. The raw saturated fraction is the combinatorial ratio $11/16 = 0.6875$: sixteen is the $2^4$ address space of the 8-tick cycle (four-bit Gray addressing), and eleven counts the $Q_3$-symmetric vacuum modes forced by the three spatial axes plus the time sector under the $[4,2,2]$ asymmetry.
An electromagnetic one-loop correction then subtracts $\alpha/\pi$ from that raw fraction, where $\alpha$ is the single measured CODATA input. Locally one writes $\Omega_\Lambda = \omega_{\mathrm{raw}} - \mathrm{em_correction}$ with $\omega_{\mathrm{raw}} = 11/16$ and $\mathrm{em_correction} = \alpha/\pi$. Upstream, EarlyUniverse records the same closed form with $\alpha_{\mathrm{lock}}$, and the sibling bounds already pin $\mathrm{em_correction} \in (0.002, 0.004)$.
The target interval $(0.683, 0.686)$ is the tight numeric window obtained after that correction; it sits inside the coarser module claim $(0.680, 0.700)$ and overlaps Planck 2018 ($0.6889 \pm 0.0056$).
proof idea
One-line term proof: pair the two sibling inequalities. The lower bound unfolds $\Omega_\Lambda$, substitutes $\omega_{\mathrm{raw}} = 0.6875$ and $\mathrm{em_correction} < 0.004$, then finishes by linarith. The upper bound does the same with $\mathrm{em_correction} > 0.002$. The conjunction is exactly the open interval statement.
why it matters
This is the tight numeric certificate that downstream cosmology reuses. CosmologicalConstantDerivation restores THEOREM C-010.4b by identifying $\Omega_{\Lambda,\mathrm{RS}}$ with this $\omega_\Lambda$ and quoting the interval; the weaker C-010.4 only gives $0 < \Omega_\Lambda < 11/16$. The local certificate omegaLambdaCert packages the interval as its final_interval field, and Track 4.A's headline theorem cites it as the structural prediction $\Omega_\Lambda \in (0.683, 0.686)$ overlapping Planck within $2\sigma$, pinned by $D = 3$ plus one measured $\alpha$. VacuumFluctuationStructural's one-statement likewise lists the same band as item 3, stressing independence from any QFT UV cutoff.
Framework-wise the $11/16$ combinatorics sits on the eight-tick octave (T7) and the three spatial dimensions (T8). The result closes the scaffolding gap left when an earlier refactor dropped the tight window in favor of only the weak bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.