chiralAnomalyEquation
plain-language theorem explainer
ChiralAnomalyEquation supplies the standard Adler-Bell-Jackiw expression for axial-current non-conservation as ∂_μ J⁵^μ = (α/π) E·B. Physicists embedding pion decay or discrete-time QFT models into Recognition Science would cite this as the native form of the anomaly. The declaration is a direct string assignment with no lemmas or reductions applied.
Claim. The chiral anomaly equation states that the divergence of the axial current satisfies $∂_μ J^{5μ} = (α/π) E · B$.
background
Recognition Science derives quantum anomalies from 8-tick phase mismatches between continuous classical symmetries and the discrete periodicity of the phi-ladder. The module QFT.Anomalies targets the chiral anomaly (axial current not conserved, realized as π⁰ → γγ), the conformal anomaly, and gauge anomalies that must cancel to preserve invariance. Upstream results include SpectralEmergence.of, which forces SU(3) × SU(2) × U(1) gauge content together with exactly 24 chiral fermion flavors (= D × 2^D for D = 3), and PhiForcingDerived.of, which calibrates the J-cost underlying the discrete phase structure.
proof idea
The declaration is a direct string assignment of the standard chiral anomaly formula with no tactic steps or lemma applications.
why it matters
This definition anchors the chiral anomaly inside the eight-tick phase mismatch mechanism that generates all quantum anomalies in Recognition Science. It supplies the concrete equation referenced by the module's target of deriving anomalies from discrete time structure and connects to the gauge-invariance consequences already established in GaugeInvariance.consequences. The placement prepares the ground for later anomaly-cancellation checks required by the spectral emergence of three generations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.