omega_lambda_lt_one
plain-language theorem explainer
Establishes that the Recognition Science dark energy density parameter satisfies Ω_Λ < 1. Early-universe cosmologists working in the RS ledger framework cite it when bounding the vacuum-mode fraction. The proof is a direct linarith reduction after unfolding the definition and invoking positivity of the locked fine-structure correction.
Claim. $Ω_Λ < 1$ where $Ω_Λ = 11/16 - α_{lock}/π$ and $α_{lock} = (1 - φ^{-1})/2$.
background
The EarlyUniverse module derives early-universe conditions and the dark sector from ledger mode counting under EU-001, D-002, and D-003. The definition of omega_lambda supplies the explicit expression Ω_Λ = 11/16 − α_lock / π, where the leading term is the vacuum fraction of ledger modes in the 8-tick cycle and the correction accounts for matter-coupled perturbations. Upstream results include alphaLock_pos, which proves 0 < α_lock, together with the positivity of π.
proof idea
Unfolds the definition of omega_lambda to obtain the expression 11/16 − alphaLock / Real.pi. Invokes alphaLock_pos and Real.pi_pos to produce a strictly positive quantity, then applies linarith to conclude the difference lies below one.
why it matters
Supplies the upper bound used in cosmological_constant_resolution to obtain 0 < omega_lambda ∧ omega_lambda < 1, completing the D-003 claim that the cosmological constant equals the ledger vacuum-mode fraction rather than QFT vacuum energy. The result rests on the eight-tick octave (T7) and the locked fine-structure constant from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.