WeakComponent
plain-language theorem explainer
Two-valued label for the weak-isospin third component in sixth-units, carrying $T_{3,6}=\pm 3$. Anyone wiring SM electric charge as $Q_6=T_{3,6}+Y_6$ on cube-completion Weyl multiplets cites it. The body is a plain finite inductive type with decidable equality and a Fintype instance; no proof obligations.
Claim. A two-element type whose inhabitants are the upper and lower weak-isospin slots. In sixth-units one has $T_{3,6}=6T_3$, with the upper slot mapped to $+3$ and the lower slot to $-3$.
background
The module continues the cube-completion gauge skeleton $SU(3)\times SU(2)\times U(1)$ by asking whether Standard Model fermion multiplets and hypercharges fit the same integer units. Every hypercharge is stored as $Y_6=6Y$, and one left-handed generation (including a sterile neutrino) is listed with multiplicities that total 16 Weyl states and cancel the usual gauge anomalies in integer arithmetic.
Weak isospin third component is likewise scaled: $T_{3,6}=6T_3$. For an $SU(2)$ doublet the physical values are $T_3=\pm 1/2$, so the sixth-unit values are exactly $\pm 3$. This inductive type is the discrete tag that distinguishes those two slots before any integer assignment is written down.
Downstream, electric charge in the same units is the sum $Q_6=T_{3,6}+Y_6$, matching the Gell-Mann–Nishijima relation after clearing the common denominator 6.
proof idea
No proof. The declaration is an inductive enumeration with constructors upper and lower, deriving DecidableEq, Repr, BEq, and Fintype. The integer map $T_{3,6}$ is a separate definition that pattern-matches on these constructors.
why it matters
Gives the discrete domain for weakT3_6 (upper $\mapsto 3$, lower $\mapsto -3$) and therefore for electricCharge6, which implements $Q_6=T_{3,6}+Y_6$ on each Weyl multiplet. That charge formula is the bookkeeping layer that lets the module state the anomaly-free SM hypercharge assignment in pure integer arithmetic inside the cube-completion units. It does not claim uniqueness of the hypercharges; the module doc is explicit that this is representation, not a forcing proof. Lands inside the Foundation track that attaches SM quantum numbers to the already-proved compact gauge-factor skeleton from GaugeLieCompletionFromCube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.