generationWeylStateCount_eq_16
plain-language theorem explainer
One Standard Model generation, counted in left-handed Weyl multiplets with the sterile neutrino included, has exactly 16 states. Anyone checking the cube-completion hypercharge layer or the anomaly bookkeeping cites this equality. The proof is a one-step native decision of the finite sum 6+3+3+2+1+1.
Claim. The total number of Weyl states in one left-handed generation equals $16$, where the count is the sum of the multiplet multiplicities: quark doublet ($6$), up conjugate ($3$), down conjugate ($3$), lepton doublet ($2$), electron conjugate ($1$), and sterile neutrino conjugate ($1$).
background
The module places the Standard Model fermion content and hypercharges in the same cube-completion units used for the compact gauge skeleton $SU(3)\times SU(2)\times U(1)$. Hypercharges are written as integers $Y_6=6Y$ with canonical denominator $6$.
A generation is packaged as six left-handed Weyl multiplets (including the sterile/right-handed neutrino as the hypercharge-zero slot): quark doublet multiplicity $6$, up and down conjugates $3$ each, lepton doublet $2$, electron conjugate $1$, sterile conjugate $1$. The generation state count is defined as the sum of those multiplicities.
Upstream, that sum is the definition of the generation Weyl-state count; the module doc records the arithmetic $6+3+3+2+1+1=16$ and notes that the same accounting cancels the usual gauge and mixed anomalies in integer arithmetic.
proof idea
Term-mode proof by native_decide. After unfolding the generation count to the sum of the six fixed multiplet multiplicities, the goal is the closed natural-number equality $6+3+3+2+1+1=16$, which the kernel decides by evaluation. No intermediate lemmas are required.
why it matters
Feeds the certificate smHyperchargeCert as the field that one generation has $16$ Weyl states, alongside the three-generation count $48=|B_3|$ and the vanishing anomaly sums. That certificate is the concrete SM hypercharge layer in cube-completion $1/6$ units after the gauge-factor skeleton from GaugeLieCompletionFromCube.
In the Recognition punchlist this is part of P0-S2-01: express SM multiplets and hypercharges in the same units as the forced $SU(3)\times SU(2)\times U(1)$ skeleton. It does not claim uniqueness of the hypercharge assignment; it locks the standard anomaly-free $16$-state generation into the formal ledger so later uniqueness or forcing arguments have a fixed target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.