theorem
proved
tauon_mass_pos
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Masses.SMVerification on GitHub at line 75.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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 -/
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