factorGenCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numbers 8, 3, 1 from the Recognition forcing chain or phi-ladder.
- Does not prove that the gauge group is exactly SU(3) × SU(2) × U(1).
- Does not address the cube-automorphism rank decomposition or full group structure.
Lean usage
factorGenCount .strongformal statement (Lean)
40def factorGenCount : SMGaugeFactor → ℕ
41 | .strong => suGenCount 3
42 | .weak => suGenCount 2
43 | .hyperY => uGenCount 1
44