phi5_eq

formal source

  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