weylMultiplet_count

The module continues the cube-completion program after the compact gauge skeleton $SU(3)\times SU(2)\times U(1)$ with recognition-axis counts $(3,2,1)$ and carrier counts $(8,3,1)$. The remaining layer is the SM fermion content and hypercharges, written in the canonical denominator-$6$ units $Y_6=6Y$.

WeylMultiplet is the inductive enumeration of one left-handed generation, including the sterile/right-handed neutrino as the hypercharge-zero completion: quark doublet, up conjugate, down conjugate, lepton doublet, electron conjugate, and neutrino conjugate. Multiplicities (color and weak components) are tracked separately; this declaration only counts the multiplet species themselves.

The module states that the full assignment yields $16$ Weyl states per generation and exact integer cancellation of the usual gauge and gravitational $U(1)$ anomalies. It does not claim the hypercharges are uniquely forced, only that the anomaly-free SM layer sits cleanly in the cube's $1/6$ unit.

The inductive type derives Fintype (and DecidableEq). The goal is Fintype.card WeylMultiplet = 6. A single decide closes it by exhaustive evaluation of the finite enumeration: six constructors, six elements. No algebraic lemmas are required.

This is the first field of the package certificate smHyperchargeCert, bound as six_multiplets. That certificate also records one-generation state count $16$, three-generation count $48$, and vanishing of the $SU(3)^2U(1)$ and $SU(2)^2U(1)$ anomaly sums in $Y_6$ arithmetic.

In the punchlist this is P0-S2-01: after GaugeLieCompletionFromCube supplies the gauge factors, the hypercharge layer must be expressible in the same cube units. Counting the six multiplet species is the discrete skeleton on which multiplicities and $Y_6$ values are hung. It does not yet force uniqueness of hypercharge; it locks the enumeration that later anomaly identities use.