anomaly_cubes
plain-language theorem explainer
Anomaly coefficients for U(1) gauge theories cube with the charge Q. Gauge theorists verifying anomaly cancellation in chiral models would cite this identity when assigning fermion charges to triangle diagrams. The proof is a one-line wrapper that unfolds the coefficient definition and applies the ring tactic to confirm the algebraic equality.
Claim. For any rational charge $Q$, the cubic anomaly coefficient of the U(1) gauge field satisfies $u(Q) = Q^3$.
background
Recognition Science derives quantum anomalies from 8-tick phase mismatches between discrete time and continuous symmetries. The module sets the local setting as chiral anomalies (such as π⁰ → γγ) and gauge anomalies that must cancel for consistency. The upstream definition states that the anomaly coefficient for U(1)³ with charge Q is proportional to Q³, given explicitly by u1CubeCoeff(Q) := Q^3.
proof idea
The proof is a term-mode one-line wrapper. It unfolds the definition of u1CubeCoeff and applies the ring tactic to verify the cubic identity.
why it matters
This supplies the basic algebraic identity for U(1) anomaly calculations inside the QFT-014 module on anomalies from 8-tick phase mismatch. It fills the charge-dependence step referenced in the paper proposition on quantum anomalies from discrete time structure and connects directly to the T7 eight-tick octave landmark. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.