lepton_doublet_charges
plain-language theorem explainer
The lepton weak doublet carries sixth-unit electric charges 0 (upper/neutrino) and -6 (lower/electron), recovering ordinary Q=0 and Q=-1. Anyone auditing the cube-completion SM hypercharge layer against Gell-Mann–Nishijima cites this. Proof is a one-line native_decide on the integer sum T3_6 + Y6.
Claim. For the left-handed lepton doublet, the sixth-unit electric charges are $Q_6(\text{upper})=0$ and $Q_6(\text{lower})=-6$, where $Q_6=T_{3,6}+Y_6$. Equivalently, ordinary charges are $Q(\nu)=0$ and $Q(e^-)=-1$.
background
This module continues the cube-completion program after the compact gauge skeleton SU(3)×SU(2)×U(1) is in place. Hypercharges are stored as integers Y6=6Y so that all anomaly sums stay in exact integer arithmetic. One left-handed generation (including a sterile neutrino) is packaged as six Weyl multiplets whose Y6 values are the familiar SM assignments: QL has Y6=1, L_L has Y6=-3, and so on, giving 16 Weyl states per generation.
Electric charge in the same units is the Gell-Mann–Nishijima sum Q6=T3_6+Y6. The weak isospin third component is likewise scaled by six, so the upper (T3=+1/2) and lower (T3=-1/2) slots of a doublet become T3_6=+3 and T3_6=-3. The lepton doublet is the multiplet (νe,e−) with hypercharge Y6=-3.
proof idea
One-line wrapper: native_decide evaluates the two integer equalities electricCharge6 leptonDoublet upper = 0 and electricCharge6 leptonDoublet lower = -6. Unfolding the definition, each side is weakT3_6(component)+hypercharge6(leptonDoublet), i.e. 3+(-3)=0 and (-3)+(-3)=-6, which decide immediately.
why it matters
Feeds the certificate smHyperchargeCert that packages the full anomaly-free SM hypercharge layer in cube units (16 Weyl states per generation, vanishing SU(3)²U(1) and SU(2)²U(1) anomalies, etc.). The module is explicit that these Y6 values are the standard SM layer expressed in the 1/6 unit, not yet a uniqueness proof that the cube forces them. Together with the gauge-factor skeleton from GaugeLieCompletionFromCube, it closes the P0-S2-01 punchlist item that fermion multiplets and hypercharges can sit in the same integer units as the recognition-axis counts (3,2,1).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.