structure
definition
SMVerificationCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.SMVerification on GitHub at line 162.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
159
160/-! ## Certificate: The SM Mass Verification Bundle -/
161
162structure SMVerificationCert where
163 all_positive : ∀ f : Fermion, 0 < fermionMass f
164 phi_scaling : ∀ (s : Sector) (r : ℤ) (z : ℤ),
165 predict_mass s (r + 1) z = phi * predict_mass s r z
166 nine_fermions : Fintype.card Fermion = 9
167
168def sm_verification_cert : SMVerificationCert where
169 all_positive := all_fermion_masses_pos
170 phi_scaling := mass_rung_scaling
171 nine_fermions := fermion_count
172
173end
174
175end SMVerification
176end Masses
177end IndisputableMonolith