tau_pred

formal source

  47
  48noncomputable def electron_pred : ℝ := Constants.phi ^ (59 : ℕ) / 4194304000000
  49noncomputable def muon_pred : ℝ := Constants.phi ^ (70 : ℕ) / 4194304000000
  50noncomputable def tau_pred : ℝ := Constants.phi ^ (76 : ℕ) / 4194304000000
  51
  52private lemma zpow_sum3 (x : ℝ) (a b c : ℤ) (hx : x ≠ 0) :
  53    x ^ a * x ^ b * x ^ c = x ^ (a + b + c) := by
  54  rw [← zpow_add₀ hx, ← zpow_add₀ hx]
  55
  56private lemma lepton_pred_eq_aux (n : ℕ) (r : ℤ) (h : (-5 : ℤ) + 62 + r = (n : ℤ)) :
  57    rs_mass_MeV .Lepton r = Constants.phi ^ n / 4194304000000 := by
  58  unfold rs_mass_MeV
  59  simp only [B_pow_Lepton_eq, r0_Lepton_eq]
  60  have hphi : Constants.phi ≠ 0 := ne_of_gt Constants.phi_pos
  61  have hphi_combine : Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (62 : ℤ) * Constants.phi ^ r =
  62      Constants.phi ^ ((n : ℕ) : ℤ) := by
  63    rw [← zpow_add₀ hphi, ← zpow_add₀ hphi]; congr 1
  64  conv_lhs =>
  65    rw [show (2 : ℝ) ^ (-22 : ℤ) * Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (62 : ℤ) * Constants.phi ^ r
  66      = (2 : ℝ) ^ (-22 : ℤ) * (Constants.phi ^ (-5 : ℤ) * Constants.phi ^ (62 : ℤ) * Constants.phi ^ r) from by ring]
  67    rw [hphi_combine, zpow_natCast]
  68  rw [show (2 : ℝ) ^ (-22 : ℤ) = ((4194304 : ℝ))⁻¹ from by
  69    have h22 : (-22 : ℤ) = -↑(22 : ℕ) := by norm_num
  70    rw [h22, zpow_neg_coe_of_pos (2 : ℝ) (by norm_num : 0 < (22 : ℕ))]; norm_num]
  71  field_simp; ring
  72
  73theorem electron_pred_eq : rs_mass_MeV .Lepton 2 = electron_pred :=
  74  lepton_pred_eq_aux 59 2 (by norm_num)
  75
  76theorem muon_pred_eq : rs_mass_MeV .Lepton 13 = muon_pred :=
  77  lepton_pred_eq_aux 70 13 (by norm_num)
  78
  79theorem tau_pred_eq : rs_mass_MeV .Lepton 19 = tau_pred :=
  80  lepton_pred_eq_aux 76 19 (by norm_num)