Ward–Takahashi identity for the two-point function of a $U(1)$ -invariant lattice field

Proved

WardTakahashi.ward_takahashi_two_point

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsquantum-field-theoryward-identity

Let $S:\mathbb C^N\to\mathbb R$ be a continuously (real-)differentiable action, invariant under global phase rotations $S(e^{i\theta}\varphi)=S(\varphi)$ , and satisfying the moment conditions

$\varphi\mapsto(1+\|\varphi\|^3)\,e^{-S(\varphi)}$ is integrable, and
$\varphi\mapsto\|\varphi\|^3\,\|DS(\varphi)\|\,e^{-S(\varphi)}$ is integrable.

Write $j_x(\varphi)=\delta_xS(\varphi)=DS(\varphi)[g_x\varphi]$ for the lattice divergence of the Noether current at site $x$ . Then

(current conservation) $\sum_x j_x(\varphi)=0$ for every configuration $\varphi$ , and
(Ward–Takahashi identity) for all sites $x,y,z$ ,

\int_{\mathbb C^N}j_x(\varphi)\,\varphi_y\overline{\varphi_z}\,e^{-S(\varphi)}\,d\varphi= i\,(\delta_{xy}-\delta_{xz})\int_{\mathbb C^N}\varphi_y\overline{\varphi_z}\,e^{-S(\varphi)}\,d\varphi .

The insertion of the current divergence into the charged two-point function produces only contact terms, one for each charged field, with opposite signs for $\varphi$ and $\overline\varphi$ . This is the position-space lattice analogue of the QED identity $k_\mu\mathcal M^{\mu}=-e\sum(\dots)$ of the source, whose right-hand side consists of amplitudes with shifted external momenta.

Formalization Note Euclidean weight $e^{-S}$ , unnormalised integrals, and sup norm $\|\varphi\|=\max_y|\varphi_y|$ .

Preamble

import Mathlib
import Definitions.Def_WardTakahashi_LatticeU1

open MeasureTheory Complex

Formal statement

namespace WardTakahashi

theorem ward_takahashi_two_point {N : ℕ} (S : FieldConfig N → ℝ)
    (hS : ContDiff ℝ 1 S) (hinv : IsU1Invariant S)
    (hm : Integrable (fun φ : FieldConfig N => (1 + ‖φ‖ ^ 3) * Real.exp (-S φ)))
    (hd : Integrable (fun φ : FieldConfig N => ‖φ‖ ^ 3 * ‖fderiv ℝ S φ‖ * Real.exp (-S φ)))
    (x y z : Fin N) :
    (∀ φ : FieldConfig N, ∑ x', localVar x' S φ = 0) ∧
    pathIntegral S (fun φ => ((localVar x S φ : ℝ) : ℂ) * (φ y * starRingEnd ℂ (φ z)))
      = I * ((if x = y then 1 else 0) - (if x = z then 1 else 0))
          * pathIntegral S (fun φ => φ y * starRingEnd ℂ (φ z)) := by sorry

end WardTakahashi

Source

Wikipedia, "Ward–Takahashi identity" (revision oldid=1374751657), https://en.wikipedia.org/w/index.php?title=Ward%E2%80%93Takahashi_identity&oldid=1374751657 ; section "Derivation in the path integral formulation" (finite-dimensional lattice model)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — NON-BLIND, same agent that drafted the statements

Note — NON-BLIND read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle by Harmonic), with full knowledge of the source material and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; an independent blind read-back is still recommended before submission.

Throughout: $\mathbb C^N$ is the space of functions $\varphi:\{0,\dots,N-1\}\to\mathbb C$ (with $N\ge 0$ arbitrary, so the case $N=0$ of a one-point space is included), regarded as a real vector space of dimension $2N$ with the sup norm $\|\varphi\|=\max_y|\varphi_y|$ and with Lebesgue (product) measure $d\varphi$ . All derivatives $D$ are real Fréchet derivatives. All integrals are Bochner integrals, which by convention equal $0$ when the integrand is not integrable. "Integrable" means Lebesgue integrable (including almost-everywhere strong measurability). $\delta_{ab}$ is $1$ if $a=b$ and $0$ otherwise.

For every $N$ and every action $S:\mathbb C^N\to\mathbb R$ such that

$S$ is continuously real-differentiable ( $C^1$ );
$S(R_\theta\varphi)=S(\varphi)$ for all real $\theta$ and all $\varphi$ , where $(R_\theta\varphi)_y=e^{i\theta}\varphi_y$ ;
$\varphi\mapsto(1+\|\varphi\|^3)\,e^{-S(\varphi)}$ is Lebesgue integrable on $\mathbb C^N$ ;
$\varphi\mapsto\|\varphi\|^3\cdot\|DS(\varphi)\|\cdot e^{-S(\varphi)}$ is Lebesgue integrable ( $\|DS(\varphi)\|$ the operator norm of the real derivative);

and for all sites $x,y,z$ (for $N=0$ there are none, and only part (a) has content), both of the following hold:

(a) for every $\varphi\in\mathbb C^N$ , $\displaystyle\sum_{x'=0}^{N-1}DS(\varphi)[g_{x'}\varphi]=0$ ;

(b) with $j_x(\varphi)=DS(\varphi)[g_x\varphi]$ (a real number, cast to $\mathbb C$ ),

\int_{\mathbb C^N}j_x(\varphi)\,\varphi_y\,\overline{\varphi_z}\;e^{-S(\varphi)}\,d\varphi=i\,\big(\delta_{xy}-\delta_{xz}\big)\int_{\mathbb C^N}\varphi_y\,\overline{\varphi_z}\;e^{-S(\varphi)}\,d\varphi .

Here $g_{x}\varphi$ is the vector equal to $i\varphi_{x}$ at site $x$ and $0$ elsewhere; integrals are Bochner integrals (value $0$ for non-integrable integrands). In particular when $x=y=z$ , or when $x\notin\{y,z\}$ , the right side is $0$ . Part (a) does not depend on $x,y,z$ or on the integrability hypotheses.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Ward–Takahashi identity for the two-point function of a U(1)U(1)U(1)-invariant lattice field

Ward–Takahashi identity for the two-point function of a $U(1)$ -invariant lattice field