structure
definition
SMGroupCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.StandardModelGroupStructure on GitHub at line 48.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
45def totalCarriers : ℕ := gluonCount + wBosonCount + rankU1
46theorem total_carriers_eq : totalCarriers = 12 := by decide
47
48structure SMGroupCert where
49 five_types : Fintype.card SMGaugeBosonType = 5
50 rank_decomp : rankSU3 + rankSU2 + rankU1 = 6
51 gluon_8 : gluonCount = 8
52 total_12 : totalCarriers = 12
53
54def smGroupCert : SMGroupCert where
55 five_types := smGaugeBosonCount
56 rank_decomp := totalRank
57 gluon_8 := gluon_count
58 total_12 := total_carriers_eq
59
60end IndisputableMonolith.Physics.StandardModelGroupStructure