smTotalGenCount
plain-language theorem explainer
The total SM gauge generator count is defined by summing the individual factor contributions from the strong, weak, and hypercharge sectors. A physicist verifying the discrete origin of the Standard Model gauge group would reference this sum when checking consistency with the observed twelve gauge bosons. The construction is a direct arithmetic combination of the per-factor generator numbers supplied by the upstream factor mapping.
Claim. The total generator count in the Standard Model gauge algebra is defined as the sum of the generator counts for the strong factor, the weak factor, and the hypercharge factor.
background
The SM Gauge Algebra module supplies the canonical generator counts for the Standard Model gauge group SU(3) × SU(2) × U(1). It follows the cube-automorphism decomposition that matches the ranks (3,2,1) to the three factors. The module states that the total of twelve generators matches the empirical count and that any deviation would falsify the identification.
proof idea
This definition is a one-line wrapper that invokes factorGenCount on the strong, weak, and hypercharge factors and adds the three natural numbers.
why it matters
The definition is referenced by the SMGaugeAlgebraCert structure, which records the individual counts together with the total equaling twelve. It thereby supports the claim that the gauge algebra has exactly twelve generators, matching the Standard Model. Within the Recognition framework this completes the Lie-algebra layer of the gauge-group-from-cube construction, consistent with the rank decomposition B₃ = (ℤ/2)³ ⋊ S₃. The downstream theorem sm_total_gen_count then proves the numerical value by direct computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.