Omega_Lambda_interval
plain-language theorem explainer
The RS dark-energy density fraction Ω_Λ = 11/16 − α/π lies in the open interval (0.683, 0.686). Cosmologists and BIT-kernel modules cite this tight numeric window rather than the weaker 0 < Ω_Λ < 11/16 bound. The proof equates the local definition with the already-proved omega_lambda from OmegaLambdaDerivation and reuses that module's interval theorem.
Claim. Let $\Omega_\Lambda^{\mathrm{RS}} = 11/16 - \alpha/\pi$, where $\alpha$ is the CODATA fine-structure constant (the single measured input). Then $0.683 < \Omega_\Lambda^{\mathrm{RS}} < 0.686$.
background
Module C-010 addresses the cosmological-constant problem: QFT vacuum energy overshoots observation by ~10^120, while data give Ω_Λ ≈ 0.7. Recognition Science replaces that with a structural formula Ω_Λ = 11/16 − α/π. The geometric seed 11/16 comes from the D=3 ledger (eight-tick octave 2³ together with gap-45 synchronization; lcm(8,45)=360 yields the 16 in the denominator). The correction α/π is the IR electromagnetic piece; α here is the external CODATA anchor, the one measured input in the module.
Locally, Omega_Lambda_RS is defined exactly as 11/16 − α/π. A weaker sibling already proves 0 < Ω_Λ < 11/16. The present theorem restores the tight decimal window that earlier refactors had dropped. Upstream, OmegaLambdaDerivation.omega_lambda is the same algebraic expression written as omega_raw − em_correction, with omega_raw = 11/16 and em_correction = α/π, and that module already carries a proved numeric interval.
proof idea
Tactic proof in two steps. First, establish definitional equality of the local Omega_Lambda_RS with OmegaLambdaDerivation.omega_lambda by unfolding both sides to 11/16 − α/π (via omega_raw_val and the definitional identity em_correction = α/π), then norm_num. Second, rewrite the goal along that equality and apply the upstream theorem omega_lambda_interval, which already supplies 0.683 < omega_lambda < 0.686. No fresh numeric work is done here; the interval is inherited.
why it matters
Restores theorem C-010.4b, the tight observational window Ω_Λ ∈ (0.683, 0.686) that OmegaLambdaPlanckCheck and BIT-kernel code depended on after only the weak Omega_Lambda_bounds survived a refactor. Downstream, FullEFEWithDarkEnergy.Omega_Lambda_RS_pos extracts positivity from the lower bound via linarith, feeding the RS dark-energy term Λ_RS = 3 H₀² Ω_Λ in the Einstein equations with dark energy.
Framework landmarks: T8 forces D=3 and the eight-tick octave that seed the 16 in 11/16; the gap-45 / lcm structure supplies the geometric numerator. The formula is not a free fit: both 11/16 and α/π are O(1), and their difference is forced near 0.68 without Planck-scale fine-tuning. The vacuum energy is read as the J-cost of the empty ledger, consistent with the RCL cost calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.