def
definition
m_tau_exp
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.Verification on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
35
36def m_e_exp : ℝ := 0.51099895069
37def m_mu_exp : ℝ := 105.6583755
38def m_tau_exp : ℝ := 1776.86
39
40/-! ## Integer-Rung Mass Formula -/
41
42noncomputable def rs_mass_MeV (s : Anchor.Sector) (r : ℤ) : ℝ :=
43 (2 : ℝ) ^ (B_pow s) * Constants.phi ^ (-(5 : ℤ)) *
44 Constants.phi ^ (r0 s) * Constants.phi ^ r / 1000000
45
46/-! ## npow prediction helpers -/
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