uGenCount
plain-language theorem explainer
uGenCount supplies the generator count for the Lie algebra u(N) as N squared. It is cited when building the total dimension of the Standard Model gauge algebra from its three factors. The implementation is the direct multiplication N * N.
Claim. The dimension of the Lie algebra of the group U(N) is $N^2$.
background
The SM Gauge Algebra module supplies the Lie-algebra generator counts for the factors of SU(3) × SU(2) × U(1). It records the canonical counts (8, 3, 1) for (su(3), su(2), u(1)), matching the dimensions (N²-1, N²-1, 1) for N = 3, 2, 1. The module states that the 8 + 3 + 1 = 12 total gauge generators match the empirical SM count and the structural prediction from the cube-automorphism rank decomposition B₃ = (ℤ/2)³ ⋊ S₃.
proof idea
The definition is the direct assignment of the product N * N.
why it matters
This definition is invoked by factorGenCount to assign the hypercharge generator count. It thereby contributes to the total of 12 generators that the module identifies with the empirical SM count and the cube-automorphism rank decomposition. In the Recognition Science framework the result supplies the Lie-algebra level structure consistent with the gauge group derived from the cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.