WeylMultiplet
plain-language theorem explainer
Enumerates the six left-handed Weyl multiplet species of one Standard Model generation: the quark weak doublet, up and down conjugates, the lepton weak doublet, the electron conjugate, and the sterile neutrino conjugate. Anyone assigning hypercharges, electric charges, or anomaly sums in the cube-completion units cites this finite type. It is a plain inductive enumeration with decidable equality and a Fintype instance.
Claim. There is a finite type of left-handed Standard Model Weyl multiplet labels for one generation, with exactly six constructors: quark weak doublet $Q_L$, up-type conjugate $u^c_L$, down-type conjugate $d^c_L$, lepton weak doublet $L_L$, electron conjugate $e^c_L$, and neutrino conjugate $\nu^c_L$ (the hypercharge-zero sterile completion).
background
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 open question is whether SM fermion multiplets and hypercharges can be written in the same units, using the canonical denominator $6$ so every hypercharge is the integer $Y_6=6Y$.
Upstream weak-force bookkeeping already fixes the weak doublets as two-component objects: the lepton doublet $(\nu_e,e^-)$ and the quark doublet $(u,d)$. This inductive type lifts those doublets into a single finite label set that also includes the three conjugate singlets and the sterile neutrino, matching the module's one-generation roster.
The intended multiplicities are $Q_L:6$ ($Y_6=1$), $u^c_L:3$ ($Y_6=-4$), $d^c_L:3$ ($Y_6=2$), $L_L:2$ ($Y_6=-3$), $e^c_L:1$ ($Y_6=6$), $\nu^c_L:1$ ($Y_6=0$), giving 16 Weyl states per generation.
proof idea
No proof body: this is an inductive definition. Six nullary constructors name the multiplet species; the deriving clause supplies decidable equality, printing, Boolean equality, and a Fintype instance so cardinality and exhaustive case analysis are available by decide and pattern matching.
why it matters
This type is the domain for the entire SM hypercharge layer in cube units. Downstream, hypercharge in sixths is defined by cases on it ($Y_6\in{1,-4,2,-3,6,0}$), multiplicity counts color and weak components, and electric charge is $Q_6=T_{3,6}+Y_6$. The certificate structure packages Fintype.card = 6, one-generation state count 16, three-generation count matching the signed-permutation cube, and vanishing $SU(3)^2U(1)$ anomaly.
It therefore anchors the exact anomaly-free SM hypercharge layer expressed in the cube completion's $1/6$ unit. The module is explicit that this is representation, not uniqueness: hypercharges are not yet forced from the forcing chain (T0–T8). It closes the bookkeeping half of punchlist item P0-S2-01 with zero sorry and zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.