anomaly_antisymmetric
plain-language theorem explainer
The theorem establishes that the U(1)^3 anomaly coefficient for charge -Q equals the negative of the coefficient for Q. Gauge theorists verifying consistency of chiral spectra under charge conjugation would cite this property. The proof is a direct algebraic reduction that unfolds the cubic definition and applies ring simplification.
Claim. Let $a(Q) := Q^3$ be the U(1)^3 anomaly coefficient for rational charge $Q$. Then $a(-Q) = -a(Q)$.
background
The QFT module derives quantum anomalies from 8-tick phase mismatches between discrete time structure and continuous classical symmetries. The central definition is the U(1)^3 anomaly coefficient $a(Q) := Q^3$, which measures the chiral anomaly contribution from a fermion of charge Q. This rests on the upstream fact that anomaly coefficients scale as the cube of the charge.
proof idea
The proof unfolds the definition of the coefficient as the cube of the charge and applies the ring tactic to confirm the sign flip under negation.
why it matters
This antisymmetry feeds directly into the anomalyProofs summary that assembles theorems on eight-tick rotations and pion lifetime predictions. It supports the framework's account of anomalies arising from the eight-tick octave and phase quantization in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.