Qft Anomalies

Anomalies from Discrete Phase

In quantum field theory, an anomaly is a classical symmetry that quantum effects break. The chiral anomaly, for instance, makes the axial current non-conserved, which explains the decay of a neutral pion into two photons. The conformal anomaly breaks scale invariance, leading to running coupling constants. Gauge anomalies, by contrast, would break gauge invariance itself, so they must cancel for the theory to be consistent.

Recognition Science models these anomalies as arising from an eight-tick cycle, a discrete record of phase steps. The framework's library of formal theorems defines a quantum of phase as π/4, so eight steps complete a full rotation of 2π. This discreteness contrasts with classical symmetry, which assumes continuous phases. The mismatch between the discrete and continuous descriptions produces the anomaly.

The module proves several structural facts. It establishes that the phase at step k is kπ/4, and that phase aligns every eight ticks. It also proves that the anomaly coefficient for a U(1) gauge group is proportional to the cube of the charge, Q³, and that this coefficient is antisymmetric under charge reversal. For QCD, it shows the beta function coefficient is (11Nc - 2Nf)/3, which is positive for six flavors and negative for seventeen, proving asymptotic freedom in the former case.

As an empirical check, the module compares its predicted neutral pion lifetime of 8.4 × 10⁻¹⁷ seconds against the observed 8.52 × 10⁻¹⁷ seconds. The relative error is 12/852, which the library proves is less than 2 percent. This agreement is a measured check of the framework's discrete phase structure, not a derivation of the full quantum field theory.

The framework's contribution is a single, labeled turn: it offers a discrete-time origin for anomalies. The eight-tick cycle is not a claim about the fundamental nature of time, but a modeling choice that reproduces known results. The library proves the arithmetic of this model, not the physical reality of discrete time.

/-- **THEOREM**: 8 phase quanta make a full rotation. -/
theorem eight_quanta_full_rotation :
    (numDiscretePhases : ℝ) * phaseQuantum = 2 * π := by
  unfold numDiscretePhases phaseQuantum
  ring

/-- **THEOREM**: Anomaly coefficients cube with charge. -/
theorem anomaly_cubes (Q : ℚ) :
    u1CubeCoeff Q = Q * Q * Q := by
  unfold u1CubeCoeff
  ring

/-- **THEOREM**: Opposite charges give opposite anomaly contributions. -/
theorem anomaly_antisymmetric (Q : ℚ) :
    u1CubeCoeff (-Q) = -u1CubeCoeff Q := by
  unfold u1CubeCoeff
  ring

/-- **THEOREM**: Positive beta means asymptotically free. -/
theorem qcd_asymptotic_freedom_nf6 :
    qcdBetaCoeff 3 6 > 0 := by
  rw [qcd_beta_nf6]
  norm_num

/-- **THEOREM**: Negative beta means NOT asymptotically free. -/
theorem qcd_no_af_nf17 :
    qcdBetaCoeff 3 17 < 0 := by
  rw [qcd_beta_nf17]
  norm_num

/-- **THEOREM**: The π⁰ lifetime prediction matches experiment to < 2%. -/
theorem pi0_prediction_within_2_percent :
    pi0_relative_error_rational < 2/100 := by
  rw [pi0_error_computation]
  norm_num

What this page does not claim

The module does not derive the full Standard Model or all quantum anomalies. The eight-tick cycle is a modeling choice, not a proven physical fact. The neutral pion lifetime agreement is an empirical check, not a derivation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/QFT/Anomalies.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: