gravitationalU1Anomaly6_eq_zero
plain-language theorem explainer
The gravitational mixed U(1) anomaly for one left-handed SM generation vanishes when hypercharges are written as integers Y6 = 6Y. Anyone checking anomaly cancellation of the cube-completion hypercharge layer cites this. The proof is a one-line native integer evaluation of the weighted multiplet sum.
Claim. With the canonical integer hypercharges $Y_6 = 6Y$ for one left-handed generation (including a sterile neutrino), the gravitational-$U(1)$ anomaly coefficient $$6\,Y_6(Q_L)+3\,Y_6(u^c_L)+3\,Y_6(d^c_L)+2\,Y_6(L_L)+Y_6(e^c_L)+Y_6(\nu^c_L)$$ equals zero.
background
The module continues the cube-completion gauge skeleton of GaugeLieCompletionFromCube (compact factors $SU(3)\times SU(2)\times U(1)$, recognition-axis counts $(3,2,1)$). Hypercharges are represented in the denominator-$6$ unit $Y_6=6Y$, so every anomaly polynomial becomes an integer linear form.
One left-handed generation is the six Weyl multiplets $Q_L$ (mult.\ 6, $Y_6=1$), $u^c_L$ (3, $-4$), $d^c_L$ (3, $2$), $L_L$ (2, $-3$), $e^c_L$ (1, $6$), $\nu^c_L$ (1, $0$). That package has 16 Weyl states and is the standard anomaly-free SM layer written in cube units.
The gravitational-$U(1)$ coefficient is the multiplicity-weighted sum of the $Y_6$ values (the pure-gravity mixed anomaly $\mathrm{Tr},Y$). The definition packages exactly that integer sum; the theorem asserts it is zero.
proof idea
Pure decision procedure on a closed integer expression. After unfolding the multiplet hypercharges, the sum is the concrete arithmetic $6\cdot 1 + 3\cdot(-4) + 3\cdot 2 + 2\cdot(-3) + 6 + 0 = 0$. native_decide evaluates that $\mathbb{Z}$-equality; no lemmas beyond the definition of the scaled anomaly are required.
why it matters
Exact vanishing of the gravitational-$U(1)$ anomaly is one of the four integer anomaly checks that certify the SM hypercharge layer in cube units (alongside $SU(3)^2U(1)$, $SU(2)^2U(1)$, and $U(1)^3$). It is packaged into the hypercharge certificate and is consumed by the T8-to-gauge/Standard-Model bridge in the unified forcing chain, which routes $D=3$ cube/spinor structure into the SM gauge surface.
The module is explicit that this is representation, not uniqueness: the hypercharges are shown to be anomaly-free in the $1/6$ unit, not forced as the only solution. That distinction matters for later forcing steps beyond T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.