weakT3_6
plain-language theorem explainer
Maps the two weak-isospin doublet slots to integer third-component values in sixth-units: upper gets +3 and lower gets -3. Anyone assembling electric charge as Q6 = T3_6 + Y6 cites this table. The body is a two-clause pattern match on the WeakComponent inductive.
Claim. The weak-isospin third component in sixth-units is the function $T_{3,6}:\{\mathrm{upper},\mathrm{lower}\}\to\mathbb{Z}$ with $T_{3,6}(\mathrm{upper})=3$ and $T_{3,6}(\mathrm{lower})=-3$. Equivalently $T_{3,6}=6T_3$ takes the values $\pm 3$ on a weak doublet.
background
The module continues the cube-completion gauge skeleton $SU(3)\times SU(2)\times U(1)$ by writing Standard Model fermion hypercharges in the canonical denominator-6 units $Y_6=6Y$. Every multiplet charge is therefore an integer, so anomaly sums and the Gell-Mann–Nishijima relation can be checked in pure integer arithmetic.
Weak isospin is treated the same way. The inductive type with constructors upper and lower stands for the two slots of an $SU(2)$ doublet; its doc-comment fixes the convention $T_{3,6}=6T_3=\pm 3$. The present definition is exactly that assignment.
Together with the multiplet hypercharge table, these sixth-unit integers feed the electric-charge formula $Q_6=T_{3,6}+Y_6$ used throughout the anomaly-cancellation checks for one left-handed generation (16 Weyl states, including the sterile neutrino).
proof idea
Pure definition by cases: pattern-match on the two constructors of WeakComponent and return the constants 3 and -3. No lemmas, no tactics, no proof obligations.
why it matters
Electric charge in sixth-units is defined downstream as the sum of this table with the multiplet hypercharge: $Q_6=T_{3,6}+Y_6$. Without the $\pm 3$ assignment the integer Gell-Mann–Nishijima relation cannot even be stated inside the cube-completion units.
The surrounding module is the exact anomaly-free SM hypercharge layer (not a uniqueness proof) expressed in the $1/6$ unit forced by the gauge-factor skeleton. The definition therefore sits on the path from the compact gauge completion to the integer anomaly vanishings for $SU(3)^2U(1)$, $SU(2)^2U(1)$, gravitational $U(1)$, and $U(1)^3$. It does not itself touch the forcing chain T0–T8; it is bookkeeping that makes those later integer identities well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.