electricCharge6
plain-language theorem explainer
Electric charge in sixth-units is the integer sum of weak isospin third component and hypercharge, both scaled by six: Q6 = T3_6 + Y6. Anyone checking SM fermion charges or anomaly cancellation in the cube-completion layer cites this. The body is a one-line definitional sum of the two sixth-unit maps.
Claim. For a left-handed SM Weyl multiplet $m$ and a weak isospin component $c\in\{\mathrm{upper},\mathrm{lower}\}$, the electric charge in sixth-units is the integer $Q_6(m,c) := T_{3,6}(c) + Y_6(m)$, so that $Q_6 = 6Q$.
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 $1/6$ units. Every hypercharge is stored as the integer $Y_6=6Y$; every weak $T_3$ as $T_{3,6}=6T_3=\pm 3$.
WeylMultiplet enumerates one left-handed generation (quark doublet, up/down conjugates, lepton doublet, electron and sterile-neutrino conjugates). WeakComponent is the upper/lower isospin slot. Upstream, hypercharge6 assigns the classical SM values ($1,-4,2,-3,6,0$), and weakT3_6 sends upper to $+3$ and lower to $-3$.
The Gell-Mann–Nishijima relation $Q=T_3+Y$ then becomes exact integer arithmetic $Q_6=T_{3,6}+Y_6$, which is what this definition records.
proof idea
Definitional one-liner: evaluate weak $T_3$ in sixth-units on the component, evaluate hypercharge in sixth-units on the multiplet, and add the two integers. No lemmas or tactics; the body is literally weakT3_6 c + hypercharge6 m.
why it matters
This is the charge map used by the immediate charge theorems: quark doublet charges become $(Q_6=4,-2)$ (i.e. $2/3$ and $-1/3$), and lepton doublet charges become $(0,-6)$ (neutrino and electron). Those facts feed the certificate structure SMHyperchargeCert, which packages six multiplets, 16 Weyl states per generation, the three-generation count match, and vanishing $SU(3)^2U(1)$ anomaly in integer sixth-units.
In the Recognition foundation layer this is the exact anomaly-free SM hypercharge layer expressed in cube-completion $1/6$ units (planning item P0-S2-01). It does not claim the hypercharges are uniquely forced by the cube; it only embeds the classical assignment so later forcing or uniqueness arguments have a clean integer target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.