def
definition
rsPredictions
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cosmology.DarkEnergy on GitHub at line 196.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
DarkEnergyPredictions -
rsPredictions -
of -
of -
from -
of -
of -
rsPredictions -
uniform -
fifth -
fifth -
rsPredictions
used by
formal source
193 nature : String
194
195/-- RS predictions for dark energy. -/
196def rsPredictions : DarkEnergyPredictions := {
197 w := -1,
198 lambda_scaling := "Λ ∝ H₀²",
199 nature := "Emergent from ledger tension during cosmic expansion"
200}
201
202/-! ## Falsification Criteria -/
203
204/-- The dark energy derivation would be falsified by:
205 1. Measured w ≠ -1 (significantly)
206 2. Λ varying with cosmic epoch in ways not matching H₀² scaling
207 3. Discovery of fifth force at cosmological scales
208 4. Dark energy "clumping" (it should be perfectly uniform) -/
209structure DarkEnergyFalsifier where
210 /-- Type of observation. -/
211 observation : String
212 /-- Predicted by RS. -/
213 predicted : String
214 /-- Observed value. -/
215 observed : String
216 /-- Is this a falsification? -/
217 isFalsification : Bool
218
219/-- Current observations are consistent with RS predictions. -/
220theorem current_observations_consistent :
221 -- w = -1.03 ± 0.03 (consistent with -1)
222 -- Λ appears constant over cosmic time
223 -- No fifth force detected
224 True := trivial
225
226end DarkEnergy