Local Ward–Takahashi identity: $\langle\delta_xF\rangle=\langle F\,\delta_xS\rangle$

Proved

WardTakahashi.local_ward_takahashi

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

mathematical-physicsquantum-field-theoryward-identity

Let $S:\mathbb C^N\to\mathbb R$ and $F:\mathbb C^N\to\mathbb C$ be continuously (real-)differentiable, let $x$ be a site, and assume

$\varphi\mapsto\|\varphi\|\,|F(\varphi)|\,e^{-S(\varphi)}$ is integrable, and
$\varphi\mapsto\|\varphi\|\,\big\|D\big(Fe^{-S}\big)(\varphi)\big\|$ is integrable.

Then

\int_{\mathbb C^N}\delta_xF(\varphi)\,e^{-S(\varphi)}\,d\varphi=\int_{\mathbb C^N}F(\varphi)\,\delta_xS(\varphi)\,e^{-S(\varphi)}\,d\varphi,

i.e. $Z_S[\delta_xF]=Z_S[F\,\delta_xS]$ .

When $S$ is $U(1)$ -invariant, $\delta_xS$ is the lattice divergence of the Noether current, and the identity says that the current divergence inserted into a correlation function equals the local variation of the observable: the Euclidean lattice form of the Ward–Takahashi identity.

Preamble

import Mathlib
import Definitions.Def_WardTakahashi_LatticeU1

open MeasureTheory Complex

Formal statement

namespace WardTakahashi

theorem local_ward_takahashi {N : ℕ} (S : FieldConfig N → ℝ) (F : FieldConfig N → ℂ)
    (hS : ContDiff ℝ 1 S) (hF : ContDiff ℝ 1 F) (x : Fin N)
    (h1 : Integrable (fun φ : FieldConfig N => ‖φ‖ * ‖F φ‖ * Real.exp (-S φ)))
    (h2 : Integrable (fun φ : FieldConfig N =>
      ‖φ‖ * ‖fderiv ℝ (fun ψ => F ψ * (Real.exp (-S ψ) : ℂ)) φ‖)) :
    pathIntegral S (localVar x F) = pathIntegral S (fun φ => F φ * ((localVar x S φ : ℝ) : ℂ)) := 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$ , every $C^1$ (over $\mathbb R$ ) action $S:\mathbb C^N\to\mathbb R$ , every $C^1$ observable $F:\mathbb C^N\to\mathbb C$ and every site $x$ , provided

$\varphi\mapsto\|\varphi\|\cdot|F(\varphi)|\cdot e^{-S(\varphi)}$ is Lebesgue integrable, and
$\varphi\mapsto\|\varphi\|\cdot\|DG(\varphi)\|$ is Lebesgue integrable, where $G(\psi)=F(\psi)e^{-S(\psi)}$ and $\|DG(\varphi)\|$ is the operator norm of its real derivative,

it holds that

\int_{\mathbb C^N}DF(\varphi)[g_x\varphi]\;e^{-S(\varphi)}\,d\varphi=\int_{\mathbb C^N}F(\varphi)\,DS(\varphi)[g_x\varphi]\;e^{-S(\varphi)}\,d\varphi,

with $g_x\varphi$ equal to $i\varphi_x$ at $x$ and $0$ elsewhere, and both sides Bochner integrals (each equal to $0$ if its integrand is not integrable; no separate integrability of either side is assumed). No invariance of $S$ is assumed.

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

Local Ward–Takahashi identity: ⟨δxF⟩=⟨F δxS⟩\langle\delta_xF\rangle=\langle F\,\delta_xS\rangle⟨δx​F⟩=⟨Fδx​S⟩

Local Ward–Takahashi identity: $\langle\delta_xF\rangle=\langle F\,\delta_xS\rangle$