phi59_gt

formal source

  81
  82/-! ## Phi-Power Transfer Lemmas -/
  83
  84private lemma phi59_gt : (2138898000000 : ℝ) < Constants.phi ^ (59 : ℕ) := by
  85  rw [phi_eq_goldenRatio]; exact Numerics.phi_pow59_gt
  86private lemma phi59_lt : Constants.phi ^ (59 : ℕ) < (2139810000000 : ℝ) := by
  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