def
definition
smTotalGenCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.SMGaugeAlgebra on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
47theorem hyper_gen_count : factorGenCount .hyperY = 1 := by decide
48
49/-- Total SM gauge-generator count. -/
50def smTotalGenCount : ℕ :=
51 factorGenCount .strong + factorGenCount .weak + factorGenCount .hyperY
52
53theorem sm_total_gen_count : smTotalGenCount = 12 := by decide
54
55/-- Number of SM gauge factors = 3, matching the cube-automorphism
56three-layer decomposition. -/
57theorem factor_count : Fintype.card SMGaugeFactor = 3 := by decide
58
59structure SMGaugeAlgebraCert where
60 strong : factorGenCount .strong = 8
61 weak : factorGenCount .weak = 3
62 hyperY : factorGenCount .hyperY = 1
63 total : smTotalGenCount = 12
64 factor_count : Fintype.card SMGaugeFactor = 3
65
66/-- SM gauge-algebra certificate. -/
67def smGaugeAlgebraCert : SMGaugeAlgebraCert where
68 strong := strong_gen_count
69 weak := weak_gen_count
70 hyperY := hyper_gen_count
71 total := sm_total_gen_count
72 factor_count := factor_count
73
74end SMGaugeAlgebra
75end Foundation
76end IndisputableMonolith