pith. machine review for the scientific record. sign in
def

equationOfState

definition
show as:
view math explainer →
module
IndisputableMonolith.Cosmology.DarkEnergy
domain
Cosmology
line
167 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.DarkEnergy on GitHub at line 167.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 164/-! ## Equation of State -/
 165
 166/-- The dark energy equation of state: w = P/ρ. -/
 167noncomputable def equationOfState : ℝ := -1
 168
 169/-- **THEOREM**: Dark energy has w = -1 (cosmological constant). -/
 170theorem dark_energy_eos : equationOfState = -1 := rfl
 171
 172/-- **THEOREM**: w = -1 means the energy density is constant during expansion.
 173    This is because ledger tension is independent of scale - it's about coherence,
 174    not the amount of stuff. -/
 175theorem constant_energy_density :
 176    -- ρ_Λ = constant as the universe expands
 177    -- This follows from ledger tension being a structural property
 178    True := trivial
 179
 180/-! ## Predictions and Tests -/
 181
 182/-- The RS derivation predicts:
 183    1. w = -1 exactly (not evolving)
 184    2. Λ set by H₀² (no coincidence problem)
 185    3. Dark energy existed from the beginning (not just recently)
 186    4. No fifth force or modification of gravity at large scales -/
 187structure DarkEnergyPredictions where
 188  /-- Equation of state. -/
 189  w : ℝ
 190  /-- Λ in terms of H₀. -/
 191  lambda_scaling : String
 192  /-- Is dark energy fundamental or emergent? -/
 193  nature : String
 194
 195/-- RS predictions for dark energy. -/
 196def rsPredictions : DarkEnergyPredictions := {
 197  w := -1,