AnomalyProofSummary
plain-language theorem explainer
AnomalyProofSummary bundles four independent results on quantum anomalies generated by the discrete eight-tick phase structure of Recognition Science. A researcher working on discrete-time QFT models would cite the record to reference the pi0 lifetime accuracy and the sign-reversal property of the cubic anomaly coefficient. The declaration is a plain record definition that simply aggregates the four sibling theorems eight_quanta_full_rotation, pi0_prediction_within_2_percent, qcd_asymptotic_freedom_nf6 and anomaly_antisymmetric.
Claim. The structure asserts: $8$ times the phase quantum equals $2π$; the rational relative error in the predicted $π^0$ lifetime is less than $0.02$; the QCD beta-function coefficient for three colors and six flavors is positive; and the cubic U(1) anomaly coefficient satisfies $c(-Q)=-c(Q)$ for every charge $Q$.
background
Recognition Science derives quantum anomalies from phase mismatches between continuous symmetries and the discrete eight-tick evolution period. The eight-tick period is the fundamental octave (T7) whose phase advance per tick is the phase quantum; eight quanta therefore close a full $2π$ rotation. The module QFT.Anomalies treats chiral, conformal and gauge anomalies as direct consequences of this discreteness rather than of continuous field theory.
proof idea
The declaration is a structure definition containing no proof body. It is instantiated by direct field assignment in the sibling anomalyProofs, which supplies the four concrete theorems eight_quanta_full_rotation, pi0_prediction_within_2_percent, qcd_asymptotic_freedom_nf6 and anomaly_antisymmetric.
why it matters
The record supplies the compact reference object used by anomalyProofs and thereby supports the QFT-014 claim that anomalies arise from eight-tick phase mismatch. It directly instantiates the T7 eight-tick octave landmark and shows how the discrete phase structure produces both the observed pi0 lifetime and the sign of the QCD beta function. No open scaffolding questions are attached to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.