anomalyProofs
plain-language theorem explainer
This definition constructs the summary record that packages four independent theorems on anomalies arising from 8-tick phase quantization. A researcher examining chiral anomalies or QCD beta functions would cite the assembled record to reference the neutral-pion lifetime bound and the sign of the one-loop coefficient. The construction is a direct record literal that populates each field from an existing theorem without additional reasoning steps.
Claim. The summary record asserts the four statements $8 q = 2π$ where $q$ is the phase quantum, the rational relative error in the predicted $π^0$ lifetime satisfies $ε < 2/100$, the QCD beta coefficient for three colors and six flavors is positive, and the cubic anomaly coefficient satisfies $A(-Q) = -A(Q)$ for every rational charge $Q$.
background
The module derives quantum anomalies from mismatches between continuous classical phases and the discrete 8-tick cycle forced by three spatial dimensions. AnomalyProofSummary is the structure whose four fields collect the key claims: eight_tick requires that eight phase quanta close a full rotation, pi0_accurate bounds the lifetime error, qcd_af asserts a positive beta coefficient, and anomaly_antisym encodes charge-reversal antisymmetry of the cubic coefficient. Upstream, eight_tick is defined as the integer 8 both in DimensionForcing (from the D=3 gap integral) and in Gap45 (from ledger coverage of 2^D). The theorem eight_quanta_full_rotation proves the rotation identity by direct unfolding and ring simplification; pi0_prediction_within_2_percent reduces the error bound to a norm_num computation; anomaly_antisymmetric follows from the ring property of the cubic coefficient.
proof idea
The definition is a one-line record constructor that directly assigns the four upstream theorems to the corresponding fields of AnomalyProofSummary: eight_quanta_full_rotation supplies the eight_tick equation, pi0_prediction_within_2_percent supplies the accuracy bound, qcd_asymptotic_freedom_nf6 supplies the beta sign, and anomaly_antisymmetric supplies the antisymmetry property.
why it matters
The record closes the QFT.Anomalies module by exhibiting a single object that witnesses all listed anomaly derivations, thereby linking the eight-tick octave (T7) to concrete predictions such as the sub-2% π⁰ error and the positive QCD beta coefficient. It supplies the concrete content for the paper proposition on anomalies from discrete time structure and makes the four claims available for citation without re-proving each step. No downstream use sites are recorded, so the object functions as a terminal summary rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.