dark_energy_implies_ne_zero
plain-language theorem explainer
The theorem shows that the ledger-derived dark energy evolution structure forces the density parameter Ω_Λ away from zero. Recognition Science cosmologists cite it when confirming that dark energy must be present rather than absent under the structural bounds. The proof is a one-line wrapper applying ne_of_gt to the positivity conjunct of the hypothesis.
Claim. If $0 < Ω_Λ < 1$, then $Ω_Λ ≠ 0$, where $Ω_Λ = 11/16 - α_{lock}/π$ is the RS dark energy density parameter.
background
Module D-006 formalizes the RS framework for dark-energy equation-of-state behavior, starting from the ledger resolution of the cosmological constant. The hypothesis dark_energy_evolution_from_ledger is the proposition $0 < Ω_Λ < 1$. Upstream, omega_lambda is defined as the noncomputable real $Ω_Λ := 11/16 - α_{lock}/π$, whose positivity follows from the fraction of unexcited ledger modes in the eight-tick cycle.
proof idea
The proof is a one-line wrapper that applies ne_of_gt to the first conjunct of the hypothesis, which asserts that omega_lambda is strictly positive.
why it matters
This result excludes the degenerate Ω_Λ = 0 endpoint, reinforcing that dark energy exists under the ledger assumption and supporting the D-006 registry item on constant versus evolving dark energy. It aligns with the eight-tick octave (T7) in the forcing chain. No downstream uses are recorded, leaving its role in larger cosmological derivations open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.