su2SquaredU1Anomaly6
plain-language theorem explainer
Integer SU(2)^2 U(1) anomaly coefficient in sixths of hypercharge: three times the quark-doublet Y6 plus the lepton-doublet Y6. Anyone checking SM anomaly cancellation in the cube-completion hypercharge layer cites this sum. It is a two-term arithmetic definition, not a proved identity; vanishing is a separate native_decide theorem.
Claim. The scaled $SU(2)^2 U(1)$ anomaly coefficient is the integer $3 Y_{6}(Q_L) + Y_{6}(L_L)$, where $Y_6 = 6Y$ is hypercharge in sixths, $Y_6(Q_L)=1$ for the left-handed quark doublet, and $Y_6(L_L)=-3$ for the left-handed lepton doublet.
background
The module continues the cube-completion gauge skeleton $SU(3)\times SU(2)\times U(1)$ by writing one left-handed SM generation (plus sterile $\nu^c$) in units $Y_6=6Y$. Six Weyl multiplet species are assigned fixed integers: quark doublet $Y_6=1$, up conjugate $-4$, down conjugate $2$, lepton doublet $-3$, electron conjugate $6$, sterile $0$. Multiplicities give 16 Weyl states per generation.
The map hypercharge6 is that assignment. Upstream weak-sector counts fix the isospin doublets: quark doublet $(u,d)$ and lepton doublet $(\nu_e,e^-)$, each of cardinality 2 under $SU(2)$. The classical $SU(2)^2 U(1)$ mixed anomaly for one generation reduces to a color-weighted sum over those doublets only: three colors times $Y_Q$ plus $Y_L$.
All anomaly bookkeeping here is exact integer arithmetic in the $1/6$ unit; the module states this is the anomaly-free SM hypercharge layer expressed in cube units, not yet a uniqueness proof that the charges are forced.
proof idea
Pure definition: expand the scaled anomaly as the linear combination $3\cdot\mathrm{hypercharge6}(Q_L)+\mathrm{hypercharge6}(L_L)$. Substituting the table values yields $3\cdot 1+(-3)$. No lemmas or tactics; the companion theorem su2SquaredU1Anomaly6_eq_zero discharges equality to zero by native_decide.
why it matters
Feeds the certificate SMHyperchargeCert (anomaly-zero fields for the hypercharge layer) and the equality theorem that proves this coefficient vanishes. Downstream it sits on the path into T8_To_GaugeStandardModel_Bridge, the forcing-chain bridge from $D=3$ cube geometry to the SM gauge routing.
In the Recognition stack this is the $SU(2)^2 U(1)$ half of the integer anomaly cancellation that must hold once the cube supplies the $(3,2,1)$ recognition-axis counts and the $1/6$ hypercharge denominator. Together with the sibling $SU(3)^2 U(1)$, gravitational-$U(1)$, and $U(1)^3$ sums, it shows one generation is anomaly-free in cube units. The module is explicit that uniqueness of these hypercharges remains open; only exact cancellation is recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.