u1CubeCoeff
plain-language theorem explainer
The cubic anomaly coefficient for a U(1) charge Q equals Q cubed. Researchers deriving chiral anomalies from eight-tick phase quantization cite it when establishing cancellation for opposite charges and vanishing at zero charge. The implementation is a direct algebraic assignment with no lemmas or tactics required.
Claim. The U(1)^3 anomaly coefficient for a fermion of charge $Q$ equals $Q^3$.
background
Recognition Science derives quantum anomalies from eight-tick phase mismatches between continuous classical symmetries and discrete time. The module QFT.Anomalies targets the chiral anomaly, such as neutral pion decay to two photons, arising when phase quantization over eight ticks breaks axial current conservation. Related definitions include phaseQuantum satisfying eight times phaseQuantum equals two pi, and eight_quanta_full_rotation enforcing the discrete rotation period.
proof idea
This is a direct definition that sets the coefficient equal to the cube of the input rational charge. No tactics or lemmas are applied; the body consists of a single power expression.
why it matters
The definition supplies the core expression used in anomaly_cubes, anomaly_antisymmetric, anomaly_zero, and the AnomalyProofSummary structure that collects the eight-tick phase identity together with the pi0 lifetime prediction. It fills the charge-cubing step in the paper proposition on quantum anomalies from discrete time structure and connects to the T7 eight-tick octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.