cubicU1Anomaly6_eq_zero
plain-language theorem explainer
The cubic U(1)^3 anomaly coefficient, written in sixth-units of hypercharge, vanishes for one left-handed SM generation including the sterile neutrino. Anyone checking anomaly freedom of the cube-completion hypercharge assignment cites this. The proof is a one-line native integer evaluation of the weighted sum of Y6 cubes.
Claim. The cubic $U(1)^3$ anomaly in sixth-units is zero: $6\,Y_{Q_L}^3 + 3\,Y_{u^c}^3 + 3\,Y_{d^c}^3 + 2\,Y_L^3 + Y_{e^c}^3 + Y_{\nu^c}^3 = 0$, where each $Y$ is the integer $6Y$ of the corresponding Weyl multiplet ($Y_{Q_L}=1$, $Y_{u^c}=-4$, $Y_{d^c}=2$, $Y_L=-3$, $Y_{e^c}=6$, $Y_{\nu^c}=0$).
background
This module sits on top of the gauge-factor skeleton from GaugeLieCompletionFromCube: compact factors $SU(3)\times SU(2)\times U(1)$ with recognition-axis counts $(3,2,1)$. Hypercharges are written in the canonical sixth-unit $Y_6=6Y$, so every multiplet carries an integer charge.
One left-handed generation, completed by a sterile right-handed neutrino at $Y_6=0$, is: quark doublet multiplicity 6 at $Y_6=1$; up conjugate 3 at $-4$; down conjugate 3 at $2$; lepton doublet 2 at $-3$; electron conjugate 1 at $6$; sterile 1 at $0$. That yields 16 Weyl states per generation.
The cubic anomaly is the integer $6 Y_{Q}^3 + 3 Y_{u^c}^3 + 3 Y_{d^c}^3 + 2 Y_L^3 + Y_{e^c}^3 + Y_{\nu^c}^3$ (the overall $6^3$ scaling is absorbed into the sixth-unit convention). Exact vanishing of this sum, together with the mixed $SU(3)^2U(1)$ and $SU(2)^2U(1)$ anomalies, is the arithmetic content of anomaly freedom in these units.
proof idea
Term-mode proof by native_decide. The anomaly is a closed integer expression built from the fixed sixth-unit hypercharges of the six Weyl multiplets; Lean evaluates the arithmetic and confirms the sum is identically zero. No lemmas beyond the definition of the cubic anomaly itself are required.
why it matters
anomaly cancellation is the first nontrivial consistency check that the SM hypercharge layer can live inside the cube-completion units. This theorem is packaged into the hypercharge certificate (alongside the mixed $SU(3)^2U(1)$ and $SU(2)^2U(1)$ zeros, the 16-state generation count, and the 48-state three-generation count). That certificate is then consumed by the T8-to-gauge-Standard-Model bridge, which routes the D=3 cube/spinor skeleton into the SM gauge surfaces.
In the forcing chain this is not a uniqueness claim: the module explicitly states that the hypercharges are not yet forced, only that the classical anomaly-free SM assignment embeds exactly in $1/6$ units. It closes the arithmetic half of P0-S2-01 on the punchlist while leaving the forcing question open for later steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.