theorem
proved
down_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 87.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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 -/
100
101theorem muon_rung_minus_electron_rung :
102 r_lepton "mu" - r_lepton "e" = 11 := by
103 simp only [r_lepton, tau, Anchor.E_passive, passive_field_edges,
104 cube_edges, active_edges_per_tick, D, wallpaper_groups]
105 norm_num
106
107theorem tauon_rung_minus_electron_rung :
108 r_lepton "tau" - r_lepton "e" = 17 := by
109 simp only [r_lepton, tau, Anchor.W, Anchor.E_passive, passive_field_edges,
110 cube_edges, active_edges_per_tick, D, wallpaper_groups]
111 norm_num
112
113/-! ## PDG Experimental Mass Values (MeV/c²)
114
115These are the PDG 2024 central values. RS predicts masses in units
116of E_coh (≈ 0.0901 eV), so comparison requires the calibration:
117