weak_gen_count
plain-language theorem explainer
The theorem asserts that the generator count for the weak gauge factor equals 3. Researchers assembling Recognition Science derivations of the Standard Model gauge algebra cite this when confirming the (8, 3, 1) decomposition. The proof is a one-line decision procedure that evaluates the factor generator count definition directly for the weak case.
Claim. The generator count for the weak factor satisfies $factorGenCount(weak) = 3$.
background
The SM Gauge Algebra module defines generator counts for the factors of SU(3) × SU(2) × U(1) via the mapping factorGenCount, which sends the strong factor to suGenCount 3, the weak factor to suGenCount 2, and the hypercharge factor to uGenCount 1. This produces the dimensions 8, 3, and 1. The module states that these sum to 12, matching the empirical Standard Model gauge boson count, and ties the structure to the cube-automorphism rank decomposition B₃ = (ℤ/2)³ ⋊ S₃.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate factorGenCount on the weak factor, which reduces immediately to the known value suGenCount 2 = 3.
why it matters
This populates the weak slot in the SM gauge algebra certificate, which collects the full set of counts (strong, weak, hyperY, total) to certify the 12-generator structure. It supports the Recognition Science prediction that any gauge group with the same cube-automorphism rank decomposition must have exactly 12 generators; deviation would falsify the identification. The module notes the structural prediction explicitly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.