suGenCount
plain-language theorem explainer
The definition computes the dimension of the Lie algebra su(N) as N squared minus one. Gauge theorists assembling the Standard Model factors inside Recognition Science cite it to obtain the canonical counts 8, 3 and 1. The implementation is a direct arithmetic expression requiring no lemmas or upstream results.
Claim. The dimension of the Lie algebra of the special unitary group SU(N) is given by $N^2 - 1$.
background
The SM Gauge Algebra module supplies Lie-algebra dimensions for the factors SU(3) × SU(2) × U(1). The cube-automorphism cert shows that the rank decomposition B₃ = (ℤ/2)³ ⋊ S₃ reproduces the SM ranks (3, 2, 1). This definition supplies the standard formula for the dimension of su(N) so that the total generator count becomes 8 + 3 + 1 = 12, matching the empirical SM count.
proof idea
The definition is a direct arithmetic expression N * N - 1. No lemmas are invoked; it is a one-line definition.
why it matters
This definition is instantiated by factorGenCount to produce the per-factor generator counts for the strong, weak and hypercharge sectors. It completes the Lie-algebra dimension part of the gauge-group-from-cube identification stated in the module documentation. The resulting total of 12 generators is consistent with the Recognition Science prediction that any gauge group sharing the same cube-automorphism rank decomposition must have exactly 12 generators; deviation would falsify the identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.