sm_total_gen_count
plain-language theorem explainer
The theorem establishes that the total number of Standard Model gauge generators equals 12, obtained by summing the contributions from the strong, weak, and hypercharge sectors. A physicist deriving gauge groups from cube automorphisms would cite this to confirm the match with observed counts. The proof is a direct decision procedure that evaluates the sum definition to the constant 12.
Claim. Let $N$ denote the total number of generators in the Standard Model gauge algebra, defined as the sum of the generator counts over the strong, weak, and hypercharge factors. Then $N = 12$.
background
The SM Gauge Algebra module works in the setting where the cube-automorphism rank decomposition $B_3 = (ℤ/2)^3 ⋊ S_3$ reproduces the Standard Model gauge group ranks (3, 2, 1). The definition of the total generator count is the sum of the three sector contributions, each obtained from the factor generator count function. Upstream results supply the J-cost structure (strictly convex with minimum at unity) and the spectral emergence that forces the gauge content SU(3) × SU(2) × U(1) together with the 24 chiral fermion flavors.
proof idea
The proof is a one-line term that applies the decide tactic to the equality after the definition of the total count has been unfolded into the explicit sum of the three sector generator counts.
why it matters
This supplies the total generator count to the SM gauge algebra certificate, which packages the individual sector counts together with the total. It confirms the module's structural prediction that any RS-derived gauge group sharing the cube-automorphism decomposition must have exactly 12 generators; deviation would falsify the identification. The result sits inside the broader forcing chain that yields D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.