Invariance under spacetime translations

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements of this proposal, at the account owner's explicit instruction. Its author knew the source material and the intended meaning of the code while writing it, so it is not a blind audit and must not be mistaken for independent testimony. Reviewers should compare it against the Lean code themselves.

Throughout, $\sigma=(\sigma^0,\sigma^1)\in\mathbb R^2$ is a worldsheet point (index $0$ is $\tau$, index $1$ is $\sigma$), $X:\mathbb R^2\to\mathbb R^D$ is the embedding, $\partial_a X^\mu(\sigma)$ is the $\mu$-th component of the Fréchet derivative of $X$ at $\sigma$ applied to the $a$-th standard basis vector (it is $0$ wherever $X$ is not differentiable), $G_{ab}(\sigma)=\sum_{\mu,\nu} g_{\mu\nu}(X(\sigma))\,\partial_aX^\mu\,\partial_bX^\nu$ is the induced metric, $h^{ab}$ denotes the entries of the matrix inverse $(h_{ab})^{-1}$ (Mathlib's inverse, which is the zero matrix when $\det h=0$), and $\sqrt{\cdot}$ is the real square root, which returns $0$ on negative inputs. The Polyakov density is $\mathcal L_P=\sqrt{-\det h}\,\sum_{a,b}h^{ab}G_{ab}$, the Polyakov action on a set $U$ is $S_P[U]=\frac T2\int_U\mathcal L_P\,d^2\sigma$ (Lebesgue measure; Bochner integral, equal to $0$ if the integrand is not integrable on $U$), and the Nambu–Goto action is $S_{NG}[U]=T\int_U\sqrt{-\det G}\,d^2\sigma$. The stress–energy tensor is $T_{ab}=T\big(G_{ab}-\tfrac12 h_{ab}\sum_{c,d}h^{cd}G_{cd}\big)$, and $\eta^{(n)}=\mathrm{diag}(1,-1,\dots,-1)$ is the $n\times n$ Minkowski matrix.

Statement. For every $D$, real $T$, constant matrix $g\in\mathbb R^{D\times D}$ (used as the target metric at every point), worldsheet metric $h:\mathbb R^2\to\mathbb R^{2\times2}$, map $X:\mathbb R^2\to\mathbb R^D$, vector $b\in\mathbb R^D$ and set $U\subseteq\mathbb R^2$ (no measurability, differentiability or integrability assumed):