hyper_gen_count
plain-language theorem explainer
The hypercharge factor in the Standard Model gauge algebra carries exactly one generator. Researchers assembling the total generator count from the cube-automorphism rank decomposition cite this result when confirming the observed total of twelve generators. The proof is a one-line decision procedure that evaluates the case definition of factorGenCount on the hyperY constructor.
Claim. The generator count assigned to the hypercharge factor satisfies $uGenCount(1) = 1$.
background
The SMGaugeAlgebra module records the Lie-algebra dimensions of the Standard Model gauge factors SU(3) × SU(2) × U(1) as the integers 8, 3 and 1. The definition factorGenCount maps each gauge factor to its generator count by sending the hypercharge case to uGenCount 1, the strong case to suGenCount 3, and the weak case to suGenCount 2. This assignment reproduces the empirical total 12 and follows the cube-automorphism cert that identifies the rank triple (3,2,1) with the decomposition B₃ = (ℤ/2)³ ⋊ S₃.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality. The tactic reduces factorGenCount .hyperY by the definition to uGenCount 1 and confirms the right-hand side equals 1.
why it matters
The theorem supplies the hyperY field of the SM gauge-algebra certificate smGaugeAlgebraCert, which assembles the complete set of generator counts. It thereby supports the Recognition Science claim that any gauge group obtained from the same cube-automorphism rank decomposition must have exactly twelve generators. The result closes the algebra-level verification step that follows the structural-rank cert in the foundation chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.