Lattice Noether theorem: $\sum_x \delta_x S = 0$ for a $U(1)$-invariant action

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 function $S:\mathbb C^N\to\mathbb R$ that is real-differentiable at every point of $\mathbb C^N$ and satisfies $S(R_\theta\varphi)=S(\varphi)$ for all $\theta\in\mathbb R$ and all $\varphi$ (where $(R_\theta\varphi)_y=e^{i\theta}\varphi_y$), and every configuration $\varphi\in\mathbb C^N$:

where $g_x\varphi$ is the vector equal to $i\varphi_x$ at site $x$ and $0$ at every other site, and $DS(\varphi)$ is the real Fréchet derivative (a real linear map $\mathbb C^N\to\mathbb R$). For $N=0$ the sum is empty.