su2SquaredU1Anomaly6_eq_zero
plain-language theorem explainer
The SU(2)^2 U(1) mixed anomaly for one left-handed SM generation vanishes when hypercharges are written as integers Y6 = 6Y. The sum is 3 Y6(Q) + Y6(L) = 0 in Z. Anyone checking anomaly cancellation of the cube-completion hypercharge layer cites this. The proof is a one-line native_decide on the fixed integer values.
Claim. With hypercharges scaled as $Y_6 = 6Y$, the mixed $SU(2)^2 U(1)$ anomaly coefficient $3 Y_6(Q_L) + Y_6(L_L)$ equals zero in $\mathbb{Z}$.
background
The module attaches the Standard Model hypercharge layer to the cube-completion gauge skeleton $SU(3)\times SU(2)\times U(1)$ already obtained in GaugeLieCompletionFromCube. Hypercharges are represented by the integer denominator-6 units $Y_6 = 6Y$, so every anomaly sum is pure integer arithmetic.
One left-handed generation (including a sterile $\nu^c_L$ with $Y_6=0$) is packaged as six Weyl multiplets: quark doublet $Q_L$ with $Y_6=1$, lepton doublet $L_L$ with $Y_6=-3$, and the usual singlets. The $SU(2)^2 U(1)$ anomaly reduces to the classical combination $3Y_Q + Y_L$, written here as the integer $3\cdot\mathrm{hypercharge}_6(Q)+\mathrm{hypercharge}_6(L)$.
Sibling facts already record that one generation has 16 Weyl states and three generations have 48; the parallel $SU(3)^2 U(1)$ sum is likewise zero.
proof idea
The definition expands to the fixed integers $3\cdot 1 + (-3)$. The proof is a single native_decide that evaluates this closed integer expression to $0$. No lemmas are invoked beyond the definition of the anomaly sum and the tabulated $Y_6$ values for the quark and lepton doublets.
why it matters
Exact vanishing of the mixed weak-hypercharge anomaly is one of the four integer cancellation identities that certify the SM hypercharge layer in cube units. It is wired directly into smHyperchargeCert as the su2_anomaly_zero field, alongside the $SU(3)^2 U(1)$, gravitational-$U(1)$, and $U(1)^3$ zeros and the 16/48 Weyl-state counts.
That certificate is consumed by the T8 bridge theorem t8_to_gauge_standard_model_bridge_holds in the unified forcing chain, which routes the D=3 cube/spinor skeleton into the gauge and Standard Model surfaces. The module is explicit that this is representation of the anomaly-free SM layer, not a uniqueness proof that these hypercharges are forced; uniqueness remains open beyond the present exact-cancellation statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.