strong_gen_count
plain-language theorem explainer
The result confirms that the strong gauge factor contributes exactly 8 generators in the Standard Model algebra. A researcher verifying gauge group dimensions from cube automorphisms would cite this to match the su(3) Lie algebra dimension. The proof evaluates the generator count definition directly via a decision procedure.
Claim. The generator count for the strong gauge factor equals 8, where the strong factor maps to the dimension of the su(3) Lie algebra.
background
This module records the Lie-algebra generator counts for SU(3) × SU(2) × U(1). The function that assigns a generator number to each gauge factor returns the value 8 on the strong case by invoking the su(3) dimension function. The module document states that these counts (8, 3, 1) total 12 and match the empirical Standard Model.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the generator count definition on the strong factor.
why it matters
It supplies the strong entry to the SM gauge algebra certificate. This supports the structural prediction that any gauge group with the same cube-automorphism rank decomposition has exactly 12 generators and aligns with the framework match to dimensions N²-1 for N=3,2,1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.