def
definition
equationOfState
show as:
view math explainer →
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
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,