hypercharge6
plain-language theorem explainer
Integer hypercharge assignment Y6 = 6Y on one left-handed SM Weyl generation, with the sterile neutrino as the Y = 0 completion. Anyone checking anomaly cancellation or electric charge in cube-completion units cites this table. It is a pure pattern-match definition: six constructors, six integers.
Claim. Define the sixth-unit hypercharge map $Y_6$ from one left-handed Standard Model Weyl multiplet to $\mathbb{Z}$ by $Y_6(Q_L)=1$, $Y_6(u^c_L)=-4$, $Y_6(d^c_L)=2$, $Y_6(L_L)=-3$, $Y_6(e^c_L)=6$, $Y_6(\nu^c_L)=0$. Equivalently $Y_6 = 6Y$ for the usual hypercharges $Y \in \{1/6,-2/3,1/3,-1/2,1,0\}$.
background
The module continues the cube-completion gauge skeleton of GaugeLieCompletionFromCube: compact factors $SU(3)\times SU(2)\times U(1)$ with recognition-axis counts $(3,2,1)$. The open question is whether SM fermion multiplets and hypercharges fit the same $1/6$ unit system.
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. Multiplicities are the usual color and weak factors (6, 3, 3, 2, 1, 1), totaling 16 Weyl states.
Canonical SM hypercharges are fractions with denominator 6. Clearing that denominator yields an integer table $Y_6=6Y$, so every anomaly polynomial becomes an exact $\mathbb{Z}$-linear combination with no rationals.
proof idea
No proof body: the declaration is a total function on the six constructors of WeylMultiplet, each mapped to a fixed integer. Comments record the corresponding ordinary $Y$ values. Downstream anomaly and charge definitions simply pattern-match on this table.
why it matters
This table is the integer substrate for the whole hypercharge layer. Downstream it feeds su3SquaredU1Anomaly6 ($2Y_Q+Y_{u^c}+Y_{d^c}$), su2SquaredU1Anomaly6 ($3Y_Q+Y_L$), gravitationalU1Anomaly6, cubicU1Anomaly6 (the $U(1)^3$ sum scaled by $6^3$), and electricCharge6 via $Q_6=T_{3,6}+Y_6$.
Module doc states the design goal: exact cancellation of those four anomaly sums in integer arithmetic for one generation of 16 Weyl states. It also records the explicit non-claim: the assignment is the anomaly-free SM layer in cube units, not a uniqueness proof that cube completion forces these $Y$ values.
In the broader Recognition chain this sits after the gauge-factor skeleton and before any claim that hypercharge is derived rather than matched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.