theorem
proved
totalRank
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.StandardModelGroupStructure on GitHub at line 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
31def rankSU2 : ℕ := 2
32def rankU1 : ℕ := 1
33
34theorem totalRank : rankSU3 + rankSU2 + rankU1 = 6 := by decide
35
36/-- gluon count = N² - 1 = 3² - 1 = 8 for SU(3). -/
37def gluonCount : ℕ := rankSU3 ^ 2 - 1
38theorem gluon_count : gluonCount = 8 := by decide
39
40/-- W boson count = N² - 1 = 2² - 1 = 3 for SU(2). -/
41def wBosonCount : ℕ := rankSU2 ^ 2 - 1
42theorem w_boson_count : wBosonCount = 3 := by decide
43
44/-- Total force carriers: 8 + 3 + 1 = 12 (before EWSB). -/
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