DarkEnergyModel

formal source

  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]