omega_lambda
plain-language theorem explainer
The definition supplies the Recognition Science prediction for the dark energy density parameter Ω_Λ as 11/16 minus alphaLock over pi. Cosmologists working inside the RS framework cite it when bounding dark energy evolution or addressing the cosmological constant problem. It is introduced as a direct algebraic expression that pulls the locked fine-structure constant from upstream constants and the vacuum fraction from the 8-tick ledger cycle.
Claim. Ω_Λ := 11/16 − α_lock / π where α_lock = (1 − 1/φ)/2 and φ denotes the golden-ratio fixed point.
background
The EarlyUniverse module formalizes RS derivations for early-universe conditions and the dark sector, covering registry items EU-001 (t = 0), D-002 (nature of dark energy), and D-003 (small cosmological constant). The 11/16 term is the fraction of ledger modes that remain in the vacuum state inside the 8-tick cycle; the correction −α/π accounts for matter-coupled perturbations. Upstream, alphaLock from Constants supplies the locked fine-structure constant via the explicit formula α_lock = (1 − 1/φ)/2.
proof idea
Direct definition that evaluates the algebraic expression 11/16 minus alphaLock divided by pi. The only dependency is the upstream definition of alphaLock; no lemmas or tactics are invoked beyond that substitution.
why it matters
This definition supplies the baseline value consumed by dark_energy_evolution_from_ledger (the structural placeholder 0 < Ω_Λ < 1) and by omega_lambda_bounded, which asserts the same bounds via cosmological_constant_resolution. It addresses D-003 by tying the cosmological constant to the 8-tick octave (T7) and the alpha band. Downstream theorems quote it to exclude the degenerate endpoints Ω_Λ = 0 and Ω_Λ = 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.