theorem
proved
hyper_gen_count
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.SMGaugeAlgebra on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
44
45theorem strong_gen_count : factorGenCount .strong = 8 := by decide
46theorem weak_gen_count : factorGenCount .weak = 3 := by decide
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