dark_energy_implies_ne_one
plain-language theorem explainer
The dark energy evolution structure from the ledger implies that the RS-predicted density parameter Ω_Λ cannot equal 1. Cosmologists using Recognition Science constants to model late-universe expansion would cite this to exclude the fully dark-energy-dominated endpoint. The proof is a one-line application of ne_of_lt to the strict upper bound in the hypothesis.
Claim. If $0 < Ω_Λ < 1$, then $Ω_Λ ≠ 1$.
background
The module addresses D-006 on whether dark energy is constant or evolving, formalizing bounds on Ω_Λ from ledger cosmological-constant resolution. The hypothesis dark_energy_evolution_from_ledger is the proposition 0 < EarlyUniverse.omega_lambda ∧ EarlyUniverse.omega_lambda < 1. Here omega_lambda is the RS prediction Ω_Λ = 11/16 − α/π, where 11/16 is the vacuum fraction of ledger modes in the 8-tick cycle and the α/π term is the small matter-coupled correction.
proof idea
This is a one-line wrapper that applies the lemma ne_of_lt to the second conjunct of the hypothesis dark_energy_evolution_from_ledger.
why it matters
This declaration closes the Ω_Λ = 1 boundary case inside the dark-energy evolution structure for D-006. It ensures the RS value derived from the eight-tick octave and ledger vacuum fraction remains strictly below unity, preventing the degenerate endpoint where dark energy would dominate completely. No downstream theorems are recorded yet, but the result supports further bounds on equation-of-state evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.