IndisputableMonolith.Cosmology.DarkEnergyEquationOfStateDepth

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Dark Energy Equation of State — S3 Depth
   6
   7w(z) on the φ-ladder: adjacent-redshift ratio corrections of order φ⁻ⁿ.
   8
   9Five canonical w-models (= configDim D = 5):
  10  ΛCDM (w = -1), wCDM (constant w), w0wa CPL, quintessence, phantom.
  11
  12Canonical BIT kernel: w_BIT(z) = -1 + δ with δ ≤ 1/φ⁵ ≈ 0.09.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith.Cosmology.DarkEnergyEquationOfStateDepth
  18open Constants
  19
  20inductive DarkEnergyModel where
  21  | lambdaCDM
  22  | wCDM
  23  | w0wa_CPL
  24  | quintessence
  25  | phantom
  26  deriving DecidableEq, Repr, BEq, Fintype
  27
  28theorem darkEnergyModel_count : Fintype.card DarkEnergyModel = 5 := by decide
  29
  30/-- δ bound = 1/φ⁵. Using φ⁵ = 5φ + 3. -/
  31noncomputable def deltaBound : ℝ := 1 / phi ^ 5
  32
  33theorem phi5_eq : phi ^ 5 = 5 * phi + 3 := by
  34  have h2 := phi_sq_eq
  35  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  36  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  37  nlinarith
  38
  39theorem deltaBound_pos : 0 < deltaBound := by
  40  unfold deltaBound
  41  exact div_pos one_pos (pow_pos phi_pos 5)
  42
  43theorem deltaBound_small : deltaBound < 0.1 := by
  44  unfold deltaBound
  45  have h5 : phi ^ 5 = 5 * phi + 3 := phi5_eq
  46  rw [h5]
  47  have h_phi_gt : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
  48  have h_denom : (11.05 : ℝ) < 5 * phi + 3 := by linarith
  49  have h_denom_pos : (0 : ℝ) < 5 * phi + 3 := by linarith
  50  rw [div_lt_iff₀ h_denom_pos]
  51  nlinarith
  52
  53structure DarkEnergyEoSDepthCert where
  54  five_models : Fintype.card DarkEnergyModel = 5
  55  phi5_fibonacci : phi ^ 5 = 5 * phi + 3
  56  delta_pos : 0 < deltaBound
  57  delta_bounded : deltaBound < 0.1
  58
  59noncomputable def darkEnergyEoSDepthCert : DarkEnergyEoSDepthCert where
  60  five_models := darkEnergyModel_count
  61  phi5_fibonacci := phi5_eq
  62  delta_pos := deltaBound_pos
  63  delta_bounded := deltaBound_small
  64
  65end IndisputableMonolith.Cosmology.DarkEnergyEquationOfStateDepth
  66