def
definition
fermionCharge
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.SMVerification on GitHub at line 57.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
54 | .strange => r_down "s"
55 | .bottom => r_down "b"
56
57def fermionCharge : Fermion → ℚ
58 | .electron | .muon | .tauon => -1
59 | .up | .charm | .top => 2/3
60 | .down | .strange | .bottom => -1/3
61
62def fermionZ (f : Fermion) : ℤ := Z (fermionSector f) (fermionCharge f)
63
64def fermionMass (f : Fermion) : ℝ :=
65 predict_mass (fermionSector f) (fermionRung f) (fermionZ f)
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 :=