theorem
proved
electron_pred_eq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.Verification on GitHub at line 73.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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)
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)]