su3SquaredU1Anomaly6_eq_zero
plain-language theorem explainer
The SU(3)^2 U(1) mixed anomaly vanishes in sixth-units for one left-handed SM generation: 2 Y_Q + Y_{u^c} + Y_{d^c} = 0. Anyone checking the cube-completion hypercharge layer or the T8 gauge bridge cites this. The proof is pure integer evaluation of the fixed multiplet charges via native_decide.
Claim. With hypercharges written as integers $Y_6 = 6Y$, the mixed $SU(3)^2 U(1)$ anomaly sum $2 Y_{Q} + Y_{u^c} + Y_{d^c}$ equals zero for the canonical one-generation assignment $(Y_Q, Y_{u^c}, Y_{d^c}) = (1,-4,2)$.
background
The module sits on top of the cube-completion gauge skeleton $SU(3)\times SU(2)\times U(1)$ and asks whether SM fermion hypercharges fit the same $1/6$ unit. Every hypercharge is stored as the integer $Y_6=6Y$. For one left-handed generation (including a sterile $\nu^c$ at $Y_6=0$) the multiplet table is fixed: quark doublet $Y_6=1$, up conjugate $-4$, down conjugate $2$, lepton doublet $-3$, electron conjugate $6$, sterile $0$.
The quantity checked here is the integer $SU(3)^2 U(1)$ anomaly polynomial in those sixth-units: twice the quark-doublet charge plus the two conjugate singlets. Exact cancellation of this sum (together with the $SU(2)^2 U(1)$, gravitational-$U(1)$, and $U(1)^3$ sums) is the arithmetic content of an anomaly-free hypercharge layer. The module is explicit that this is representation, not uniqueness: the charges are the standard SM values written in cube units, not yet forced from first principles.
proof idea
One-line computational proof. Unfold the anomaly definition to the integer linear form $2\cdot Y_6(Q)+Y_6(u^c)+Y_6(d^c)$, substitute the fixed table values $1$, $-4$, $2$, and discharge equality to zero by native_decide on $\mathbb{Z}$. No lemmas beyond the definition of the anomaly sum and the hypercharge table are required.
why it matters
Feeds the local certificate smHyperchargeCert, which packages multiplet counts, the 16 Weyl states per generation, the 48-state three-generation total, and all four anomaly vanishings. That certificate is consumed by the forcing-chain bridge t8_to_gauge_standard_model_bridge_holds, which routes T8 (D=3 spatial dimensions forced by the cube/spinor skeleton) into the gauge and Standard Model theorem surfaces.
In the Recognition framework this is the arithmetic half of P0-S2-01: after GaugeLieCompletionFromCube supplies the compact factors and carrier counts, the hypercharge layer must sit in the same $1/6$ unit with exact anomaly cancellation. The result does not claim the charges are uniquely forced; it closes the integer-arithmetic check that the standard assignment is anomaly-free in cube units, so the T8 bridge can cite a proved zero rather than a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.