gravitationalU1Anomaly6
plain-language theorem explainer
Integer gravitational-U(1) anomaly coefficient for one left-handed SM generation, written in sixths of hypercharge. It is the multiplicity-weighted sum of Y6 over the six Weyl multiplets (quark doublet, up/down conjugates, lepton doublet, electron and sterile neutrino conjugates). Anomaly certificates and the T8-to-gauge bridge cite it to record exact cancellation. The body is a direct linear combination of the hypercharge table with the multiplet state counts.
Claim. Let $Y_6=6Y$ be the integer hypercharge of each left-handed Weyl multiplet in one Standard Model generation (including a sterile neutrino). The gravitational-$U(1)$ anomaly coefficient, scaled by 6, is the integer $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)$.
background
This module sits on the cube-completion gauge skeleton SU(3)×SU(2)×U(1) and asks whether SM fermion multiplets and hypercharges fit the same units. Hypercharges are stored as integers $Y_6=6Y$ so every anomaly sum is exact integer arithmetic.
One left-handed generation (with sterile $\nu^c$) has six Weyl multiplets: $Q_L$ (multiplicity 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 is 16 Weyl states per generation. The gravitational-$U(1)$ anomaly is the sum of hypercharges over all Weyl fermions; here it is packaged with those multiplicities already inserted.
Upstream, hypercharge6 is the lookup table $Y_6$ on the multiplet enum. The doublet sizes 2 for quarks and leptons come from the weak-force emergence layer and match the multiplicity factors 6 (=3 colors × 2) and 2 in the sum.
proof idea
Definition only: no tactic proof. The value is the explicit $\mathbb{Z}$-linear form that multiplies each multiplet's $Y_6$ by its Weyl-state count (6 for the colored quark doublet, 3 for each quark conjugate, 2 for the lepton doublet, 1 for each lepton conjugate) and adds the six terms. Downstream equality-to-zero is discharged by native_decide on this closed integer expression.
why it matters
Exact vanishing of the gravitational-$U(1)$ anomaly is one of the four integer anomaly cancellations the module records for the SM hypercharge layer (together with $SU(3)^2U(1)$, $SU(2)^2U(1)$, and $U(1)^3$). The immediate consumer is gravitationalU1Anomaly6_eq_zero, which asserts the sum is 0; that fact is bundled into SMHyperchargeCert and routed through T8_To_GaugeStandardModel_Bridge in the unified forcing chain.
In the Recognition framework this is the anomaly-free SM hypercharge layer expressed in the cube completion's $1/6$ unit after T8 forces $D=3$ and the gauge skeleton. The module is explicit that the assignment is not yet uniquely forced: it is the exact anomaly-free layer in cube units, not a uniqueness theorem for $Y$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.