omega_lambda_bounded
plain-language theorem explainer
The theorem establishes that the RS dark energy density parameter lies strictly between zero and one. Researchers closing the D-006 registry item on dark energy constancy cite the bound when extracting ledger-derived constraints for cosmic evolution models. The proof is a one-line term application of the cosmological constant resolution theorem.
Claim. $0 < Ω_Λ < 1$, where $Ω_Λ = 11/16 - α_{lock}/π$ is the dark energy density parameter from ledger mode counting.
background
The module formalizes the RS framework for D-006 on whether dark energy is constant or evolving. It extracts bounds on the density parameter from the ledger cosmological-constant resolution, marking the item as STARTED. The upstream cosmological_constant_resolution theorem states that the cosmological constant is the fraction of vacuum modes in the ledger, not QFT vacuum energy, and supplies the explicit bounds via the definition Ω_Λ := 11/16 − α_lock / π. The 11/16 term counts unexcited modes in the eight-tick cycle while the α/π correction accounts for matter-coupled perturbations.
proof idea
The proof is a term-mode one-liner that applies the cosmological_constant_resolution theorem from the EarlyUniverse module.
why it matters
The result supplies the positivity and subunitarity of Ω_Λ required by the downstream dark_energy_evolution_structure theorem. It advances the D-006 registry item by formalizing ledger-derived bounds on the cosmological constant. The construction draws on the eight-tick octave from the forcing chain, where the vacuum-mode fraction originates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.