phi70_lt

formal source

  87  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow59_lt
  88private lemma phi70_gt : (425698000000000 : ℝ) < Constants.phi ^ (70 : ℕ) := by
  89  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow70_gt
  90private lemma phi70_lt : Constants.phi ^ (70 : ℕ) < (426011000000000 : ℝ) := by
  91  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow70_lt
  92private lemma phi76_gt : (7638724000000000 : ℝ) < Constants.phi ^ (76 : ℕ) := by
  93  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow76_gt
  94private lemma phi76_lt : Constants.phi ^ (76 : ℕ) < (7646046000000000 : ℝ) := by
  95  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow76_lt
  96
  97/-! ## Electron Mass Verification -/
  98
  99theorem electron_mass_bounds :
 100    (0.5098 : ℝ) < electron_pred ∧ electron_pred < (0.5102 : ℝ) := by
 101  unfold electron_pred
 102  constructor
 103  · rw [lt_div_iff₀ (by norm_num : (0 : ℝ) < 4194304000000)]
 104    calc (0.5098 : ℝ) * 4194304000000 < (2138898000000 : ℝ) := by norm_num
 105      _ < Constants.phi ^ 59 := phi59_gt
 106  · rw [div_lt_iff₀ (by norm_num : (0 : ℝ) < 4194304000000)]
 107    calc Constants.phi ^ 59 < (2139810000000 : ℝ) := phi59_lt
 108      _ < (0.5102 : ℝ) * 4194304000000 := by norm_num
 109
 110theorem electron_relative_error :
 111    |rs_mass_MeV .Lepton 2 - m_e_exp| / m_e_exp < 0.003 := by
 112  rw [electron_pred_eq]
 113  have hb := electron_mass_bounds
 114  have hexp_pos : (0 : ℝ) < m_e_exp := by unfold m_e_exp; norm_num
 115  rw [div_lt_iff₀ hexp_pos, abs_lt]
 116  unfold m_e_exp
 117  constructor <;> nlinarith [hb.1, hb.2]
 118
 119/-! ## Muon Mass Verification -/
 120