hyper_gen_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the generator counts from the forcing chain or phi-ladder.
- Does not prove the full gauge-group identification with the cube automorphism.
- Does not address coupling constants or particle representations.
- Does not extend the count to grand-unified or beyond-Standard-Model groups.
formal statement (Lean)
47theorem hyper_gen_count : factorGenCount .hyperY = 1 := by decide
proof body
Term-mode proof.
48
49/-- Total SM gauge-generator count. -/