def
definition
suGenCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.SMGaugeAlgebra on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
24namespace SMGaugeAlgebra
25
26/-- Number of generators of `su(N)` is `N² - 1`. -/
27def suGenCount (N : ℕ) : ℕ := N * N - 1
28
29/-- Number of generators of `u(N)` is `N²`. -/
30def uGenCount (N : ℕ) : ℕ := N * N
31
32/-- The three SM gauge factors. -/
33inductive SMGaugeFactor where
34 | strong -- SU(3): 8 generators
35 | weak -- SU(2): 3 generators
36 | hyperY -- U(1): 1 generator
37 deriving DecidableEq, Repr, BEq, Fintype
38
39/-- Generator count per gauge factor. -/
40def factorGenCount : SMGaugeFactor → ℕ
41 | .strong => suGenCount 3
42 | .weak => suGenCount 2
43 | .hyperY => uGenCount 1
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