muon_ratio_undershoot

formal source

 226    mul_lt_mul h16_hi (le_of_lt hφ_hi) hφ_pos (by norm_num)
 227  linarith [show (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) < (3574 : ℝ) from by norm_num]
 228
 229theorem muon_ratio_undershoot :
 230    Constants.phi ^ (11 : ℕ) < ratio_mu_e_exp := by
 231  linarith [phi11_lt, ratio_mu_e_exp_bounds.1]
 232
 233theorem tau_ratio_overshoot :
 234    ratio_tau_e_exp < Constants.phi ^ (17 : ℕ) := by
 235  linarith [phi17_gt, ratio_tau_e_exp_bounds.2]
 236
 237theorem muon_electron_ratio_error :
 238    |Constants.phi ^ (11 : ℕ) - ratio_mu_e_exp| / ratio_mu_e_exp < 0.04 := by
 239  have hr := ratio_mu_e_exp_bounds
 240  have hexp_pos : (0 : ℝ) < ratio_mu_e_exp := by linarith [hr.1]
 241  rw [div_lt_iff₀ hexp_pos, abs_lt]
 242  constructor <;> nlinarith [phi11_gt, phi11_lt, hr.1, hr.2]
 243
 244theorem tau_electron_ratio_error :
 245    |Constants.phi ^ (17 : ℕ) - ratio_tau_e_exp| / ratio_tau_e_exp < 0.03 := by
 246  have hr := ratio_tau_e_exp_bounds
 247  have hexp_pos : (0 : ℝ) < ratio_tau_e_exp := by linarith [hr.1]
 248  rw [div_lt_iff₀ hexp_pos, abs_lt]
 249  constructor <;> nlinarith [phi17_gt, phi17_lt, hr.1, hr.2]
 250
 251/-! ## Summary Certificate -/
 252
 253structure MassVerificationCert where
 254  electron_in_range : (0.5098 : ℝ) < electron_pred ∧ electron_pred < 0.5102
 255  muon_in_range : (101.49 : ℝ) < muon_pred ∧ muon_pred < 101.57
 256  tau_in_range : (1821 : ℝ) < tau_pred ∧ tau_pred < 1823
 257  electron_pct : |rs_mass_MeV .Lepton 2 - m_e_exp| / m_e_exp < 0.003
 258  muon_pct : |rs_mass_MeV .Lepton 13 - m_mu_exp| / m_mu_exp < 0.04
 259  tau_pct : |rs_mass_MeV .Lepton 19 - m_tau_exp| / m_tau_exp < 0.03