factorGenCount
plain-language theorem explainer
factorGenCount maps each Standard Model gauge factor to its Lie-algebra generator count: eight for strong, three for weak, and one for hyperY. Recognition Science gauge theorists cite it when confirming the total of twelve generators matches the observed SM algebra. The definition proceeds by pattern matching on the SMGaugeFactor inductive type and delegates arithmetic to suGenCount and uGenCount.
Claim. The function $f$ from gauge factors to natural numbers satisfies $f(strong)=3^2-1$, $f(weak)=2^2-1$, $f(hyperY)=1^2$.
background
The SM Gauge Algebra module records the generator dimensions of SU(3) × SU(2) × U(1). SMGaugeFactor is the inductive type with three constructors: strong for SU(3), weak for SU(2), and hyperY for U(1). Upstream, suGenCount N computes N²-1 for the dimension of su(N) while uGenCount N computes N² for the dimension of u(N).
proof idea
The definition is given directly by pattern matching on the three constructors of SMGaugeFactor, sending strong to suGenCount 3, weak to suGenCount 2, and hyperY to uGenCount 1.
why it matters
This definition supplies the concrete values required by SMGaugeAlgebraCert to assert the sector counts 8, 3, 1 and the total of 12. The module documentation states that this total matches the empirical SM count and that any deviation would falsify the gauge-group-from-cube identification. It completes the Lie-algebra layer of the structural-rank cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.