pith. machine review for the scientific record. sign in
def definition def or abbrev high

equationOfState

show as:
view Lean formalization →

Dark energy's equation of state parameter is defined as w = -1. Cosmologists working on the accelerating expansion cite this when tracing the cosmological constant to ledger tension in Recognition Science. The assignment follows directly from equating dark energy to a constant scalar field whose pressure equals the negative of its density.

claimThe dark energy equation of state parameter is defined by $w = -1$, where $w = P/ρ$.

background

In the Cosmology.DarkEnergy module, dark energy is derived from ledger tension: the global J-cost balance constraint conflicts with expansion, which creates new spacetime volume and therefore new ledger entries. The resulting residual tension energy is identified with the cosmological constant Λ. This definition supplies the equation of state value w = P/ρ = -1, consistent with the upstream constant scalar field construction.

proof idea

The declaration is a direct noncomputable definition that assigns the real number -1.

why it matters in Recognition Science

This definition supplies the base value used by dark_energy_w (which examines the coincidence problem) and dark_energy_eos (which notes that w = -1 keeps energy density constant because ledger tension is scale-independent). It fills the COS-006 step that obtains Λ from the requirement of ledger coherence across expanding space.

scope and limits

formal statement (Lean)

 167noncomputable def equationOfState : ℝ := -1

proof body

Definition body.

 168
 169/-- **THEOREM**: Dark energy has w = -1 (cosmological constant). -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.