def
definition
sm_verification_cert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.SMVerification on GitHub at line 168.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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