weylMultiplicity
plain-language theorem explainer
Assigns each left-handed SM Weyl multiplet its state count including color and weak factors: 6 for the quark doublet, 3 for each quark conjugate, 2 for the lepton doublet, and 1 for each lepton conjugate. Anyone counting generation Weyl states or checking anomaly cancellation in sixths of hypercharge cites this table. It is a pure pattern-match definition on the multiplet inductive.
Claim. For each left-handed Standard Model Weyl multiplet $M$, the multiplicity $n(M)\in\mathbb{N}$ is $n(Q_L)=6$, $n(u^c_L)=3$, $n(d^c_L)=3$, $n(L_L)=2$, $n(e^c_L)=1$, $n(\nu^c_L)=1$, counting color and weak components.
background
The module continues the cube-completion gauge skeleton $SU(3)\times SU(2)\times U(1)$ by asking whether SM fermion multiplets and hypercharges fit the same units. Hypercharges are stored as integers $Y_6=6Y$.
WeylMultiplet is the inductive type of one left-handed generation: quark doublet, up and down conjugates, lepton doublet, electron conjugate, and sterile/right-handed neutrino conjugate. Upstream weak-force constants already fix the bare isospin doublets at size 2; here color multiplies the quark sector (factor 3) so the quark doublet carries $3\times 2=6$ Weyl states.
The module states the target bookkeeping explicitly: multiplicities $(6,3,3,2,1,1)$ with $Y_6$ values $(1,-4,2,-3,6,0)$, giving 16 Weyl states per generation and integer anomaly cancellation.
proof idea
No proof obligations. The definition is an exhaustive pattern match on the six constructors of the multiplet inductive, returning the fixed natural numbers 6, 3, 3, 2, 1, 1. Those numbers encode color times weak dimension for quarks and weak dimension alone for leptons.
why it matters
This table is the multiplicity layer under the hypercharge-in-sixths story. Downstream, generationWeylStateCount sums the six values to obtain $6+3+3+2+1+1=16$ Weyl states per generation; three-generation counts and the integer anomaly identities ($SU(3)^2U(1)$, and siblings) build on that sum.
In the Recognition punchlist it is the concrete SM fermion content expressed in cube-completion units after the gauge-factor skeleton $(3,2,1)$ and carrier counts $(8,3,1)$. It does not claim the hypercharges are uniquely forced by the cube; it only locks the anomaly-free SM layer in the $1/6$ unit so later uniqueness or forcing arguments have a fixed target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.