`anomaly_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.Anomalies
domain: QFT
line: 150 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.Anomalies on GitHub at line 150.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 147  ring
 148
 149/-- **THEOREM**: Zero charge gives zero anomaly. -/
 150theorem anomaly_zero :
 151    u1CubeCoeff 0 = 0 := by
 152  unfold u1CubeCoeff
 153  ring
 154
 155/-! ## Chiral Anomaly Description -/
 156
 157/-- The chiral anomaly (Adler-Bell-Jackiw):
 158    The axial current is NOT conserved: ∂_μ J⁵^μ = (α/π) E·B -/
 159def chiralAnomalyEquation : String :=
 160  "∂_μ J⁵^μ = (α/π) E·B"
 161
 162/-- Physical consequences of chiral anomaly. -/
 163def chiralAnomalyConsequences : List String := [
 164  "π⁰ → γγ decay (lifetime 8.52 × 10⁻¹⁷ s)",
 165  "η → γγ decay",
 166  "Chiral magnetic effect",
 167  "Axion physics"
 168]
 169
 170/-! ## 8-Tick Connection to Anomalies -/
 171
 172/-- In RS, anomalies arise from phase mismatch between:
 173    - Continuous classical evolution
 174    - Discrete 8-tick quantum evolution
 175
 176    The "extra" phase from discretization creates the anomaly. -/
 177structure PhaseEvolution where
 178  /-- Number of discrete ticks. -/
 179  ticks : ℕ
 180  /-- Corresponding continuous phase. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.