quark_doublet_charges
plain-language theorem explainer
In sixth-units of electric charge, the upper and lower components of the left-handed quark doublet carry charges 4 and −2 (i.e. ordinary Q = 2/3 and Q = −1/3). Anyone auditing the cube-completion encoding of SM fermion charges cites this identity. The proof is a one-line native decision on the integer definition Q₆ = T_{3,6} + Y₆.
Claim. Electric charge in units of $1/6$ on the left-handed quark isospin doublet equals $4$ on the upper weak component and $-2$ on the lower weak component: $Q_6(Q_L,\uparrow)=4$ and $Q_6(Q_L,\downarrow)=-2$.
background
The module continues the cube-completion program after the compact gauge skeleton $SU(3)\times SU(2)\times U(1)$ is already in hand. Hypercharges are stored as integers $Y_6=6Y$, so every charge identity is pure integer arithmetic in the canonical denominator-6 convention.
Electric charge in these units is defined by $Q_6=T_{3,6}+Y_6$: the sum of the weak-isospin third component scaled by six and the multiplet hypercharge. For the quark doublet the module assigns $Y_6=1$ (ordinary $Y=1/6$), while the upper and lower weak components carry $T_{3,6}=\pm 3$.
The local setting is one left-handed generation completed by a sterile neutrino: sixteen Weyl states whose $SU(3)^2U(1)$, $SU(2)^2U(1)$, gravitational-$U(1)$, and $U(1)^3$ anomaly sums cancel exactly in $\mathbb{Z}$.
proof idea
One-line wrapper that applies native_decide. Electric charge in sixth-units is definitionally the sum of the scaled weak $T_3$ for the chosen component and the multiplet hypercharge. Both summands are concrete integers on the quark doublet, so the two equalities collapse to closed integer arithmetic that the kernel decides immediately.
why it matters
Feeds the SM hypercharge certificate, which packages multiplet count, the 16-state one-generation census, the 48-state three-generation census, and vanishing of the $SU(3)^2U(1)$ and $SU(2)^2U(1)$ anomalies. That certificate is the Lean-side closure of punchlist item P0-S2-01: the anomaly-free SM hypercharge layer written in cube-completion $1/6$ units.
The module is explicit that uniqueness of these hypercharges is not claimed; only exact match to the textbook SM layer once the denominator-6 convention is fixed. The result sits downstream of the already-proved gauge-factor skeleton (recognition-axis counts $(3,2,1)$, carrier counts $(8,3,1)$) and supplies the charge labels needed for later mass-ladder and coupling work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.