suGenCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the specific values N = 3, 2, 1 from Recognition Science axioms.
- Does not prove that the gauge group must be SU(3) × SU(2) × U(1).
- Does not address fermion representations or chirality.
- Does not connect the generator count to the phi-ladder or mass formula.
formal statement (Lean)
27def suGenCount (N : ℕ) : ℕ := N * N - 1
proof body
Definition body.
28
29/-- Number of generators of `u(N)` is `N²`. -/