equationOfState
plain-language theorem explainer
Dark energy equation of state parameter is defined to equal -1. Cosmologists working in Recognition Science cite it when modeling accelerated expansion from a J-cost vacuum ground state. The definition is a direct constant assignment that downstream theorems discharge by reflexivity.
Claim. The dark energy equation of state parameter satisfies $w = p/ρ = -1$.
background
The CosmologicalConstant module targets derivation of Λ from RS principles, treating the vacuum as a J-cost ground state whose baseline ledger cost produces a nonzero cosmological constant. Observed Λ_obs ≈ 10^{-52} m^{-2} is noted as ~10^{120} times smaller than naive QFT predictions, with φ-scaling proposed to explain the small but nonzero value. The upstream DarkEnergy.equationOfState supplies the identical assignment, confirming w = -1 for the cosmological-constant case.
proof idea
Direct definition that assigns the constant value -1. No lemmas or tactics are invoked; the body is a literal real-number constant.
why it matters
This definition supplies the base value for the parent theorems dark_energy_w and dark_energy_eos, which establish that dark energy density remains constant during expansion because ledger tension is scale-independent. It advances the COS-013 target of obtaining Λ from J-cost principles. Within the framework it sits downstream of the phi-ladder and eight-tick octave constructions, though the full numerical resolution of the cosmological-constant problem remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.