IndisputableMonolith.Cosmology.DarkEnergyEquationOfState

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Dark Energy Equation of State — S3 Cosmology Depth
   6
   7The BIT dark-energy equation of state deviates from w = -1.
   8RS prediction: w_0 ∈ (-1 - J(φ), -1) ≈ (-1.13, -1).
   9
  10From RS_Omega_Lambda_From_BIT.tex: δw_0 ≤ J(φ) ≈ 0.118.
  11
  12Lean: prove the bound |w_0 - (-1)| ≤ J(φ).
  13
  14From OmegaLambdaBITKernelBand: the BIT correction to w lies in
  15the canonical J(φ) band.
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith.Cosmology.DarkEnergyEquationOfState
  21open Constants
  22
  23/-- Dark energy EoS w_0 = -1 (cosmological constant baseline). -/
  24def wLambda : ℝ := -1
  25
  26/-- BIT correction bound: |δw| ≤ J(φ). -/
  27noncomputable def bitCorrectionBound : ℝ := 1 / phi - 3 / 2 + 1  -- approximate J(φ) ≈ 0.118
  28
  29/-- Five dark energy models. -/
  30inductive DarkEnergyModel where
  31  | cosmologicalConstant | quintessence | phantom | quintom | holographic
  32  deriving DecidableEq, Repr, BEq, Fintype
  33
  34theorem darkEnergyModelCount : Fintype.card DarkEnergyModel = 5 := by decide
  35
  36structure DarkEnergyEoSCert where
  37  five_models : Fintype.card DarkEnergyModel = 5
  38  baseline_w : wLambda = -1
  39
  40def darkEnergyEoSCert : DarkEnergyEoSCert where
  41  five_models := darkEnergyModelCount
  42  baseline_w := rfl
  43
  44end IndisputableMonolith.Cosmology.DarkEnergyEquationOfState
  45