omega_lambda
plain-language theorem explainer
Defines the RS dark-energy density parameter as the raw phase-saturation fraction minus a one-loop EM correction: Ω_Λ = 11/16 − α/π, with α the measured CODATA fine-structure constant. Cosmologists and RS auditors cite it as the single numeric prediction fed into Planck-window checks and dark-energy structure lemmas. The body is a two-term difference of already-defined reals.
Claim. The dark-energy density parameter is $\Omega_\Lambda := \omega_{\mathrm{raw}} - \delta_{\mathrm{EM}}$, where $\omega_{\mathrm{raw}} = 11/16$ is the saturated vacuum-mode fraction on the 8-tick ledger and $\delta_{\mathrm{EM}} = \alpha/\pi$ is the electromagnetic one-loop correction with measured CODATA $\alpha$.
background
The module derives the cosmological constant fraction from phase saturation on the eight-tick cycle (T7). The 8-tick DFT carries a forced 44-mode budget; 11 of those modes are Q₃-symmetric (3 spatial axes plus gauge sector under the [4,2,2] Gray-code asymmetry). Addressing uses 16 = 2⁴ slots (4-bit labels on the cycle), so the raw saturated fraction is 11/16.
omega_raw is exactly that ratio: saturated modes over tick-addressing cardinality, proved equal to 11/16. em_correction is α_CODATA/π: the fraction of modes that couple electromagnetically at one loop, taken as the single measured input after the constructed-α route was reverted. Upstream EarlyUniverse and Hubble preregistration packages state the same closed form Ω_Λ = 11/16 − α/π as the RS prediction for the vacuum energy density parameter.
proof idea
Pure definitional abbreviation: subtract the already-defined real em_correction from the already-defined real omega_raw. No tactics, no lemmas, no computation. Downstream numeric bounds (omega_lambda_lt_686, omega_lambda_gt_683) and the interval theorems do the arithmetic; this declaration only names the difference.
why it matters
This is the named RS value of Ω_Λ that CosmologicalConstantDerivation identifies with Omega_Lambda_RS. Parent results include Omega_Lambda_bounds (0 < Ω_Λ < 11/16), the restored tight window Omega_Lambda_interval (Ω_Λ ∈ (0.683, 0.686)), and the dark-energy evolution structure package (positivity, subunit bound, exclusion of the degenerate endpoints 0 and 1). The module claims consistency with Planck 2018 (0.6889 ± 0.0056) inside a slightly wider (0.680, 0.700) band.
Framework landmarks: eight-tick octave (T7) supplies the 16-slot addressing; the 11-mode Q₃ count is the combinatorial numerator. The α/π correction is deliberately the one measured input, not a derived coupling. Feeds BIT-kernel and Hubble preregistration prediction points under the same closed form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.