theorem
proved
electron_mass_pos
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.SMVerification on GitHub at line 69.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
66
67/-! ## All Fermion Masses Are Positive -/
68
69theorem electron_mass_pos : 0 < fermionMass .electron :=
70 predict_mass_pos _ _ _
71
72theorem muon_mass_pos : 0 < fermionMass .muon :=
73 predict_mass_pos _ _ _
74
75theorem tauon_mass_pos : 0 < fermionMass .tauon :=
76 predict_mass_pos _ _ _
77
78theorem up_mass_pos : 0 < fermionMass .up :=
79 predict_mass_pos _ _ _
80
81theorem charm_mass_pos : 0 < fermionMass .charm :=
82 predict_mass_pos _ _ _
83
84theorem top_mass_pos : 0 < fermionMass .top :=
85 predict_mass_pos _ _ _
86
87theorem down_mass_pos : 0 < fermionMass .down :=
88 predict_mass_pos _ _ _
89
90theorem strange_mass_pos : 0 < fermionMass .strange :=
91 predict_mass_pos _ _ _
92
93theorem bottom_mass_pos : 0 < fermionMass .bottom :=
94 predict_mass_pos _ _ _
95
96theorem all_fermion_masses_pos : ∀ f : Fermion, 0 < fermionMass f := by
97 intro f; cases f <;> exact predict_mass_pos _ _ _
98
99/-! ## Generation Structure: φ-Scaling Between Generations -/