Equations of motion in conformal gauge: $\Box X^\mu=0$

Proved

PolyakovAction.conformal_gauge_wave_equation

by Lucas · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsstring-theory

Work in conformal gauge with a Minkowskian target, $h_{ab}=\eta_{ab}$ , $g_{\mu\nu}=\eta_{\mu\nu}=\mathrm{diag}(1,-1,\dots,-1)$ , and let $T\neq0$ . Let $X$ be $C^2$ . If the action is stationary under every smooth compactly supported variation $X^\mu\to X^\mu+\varepsilon\,\delta X^\mu$ , i.e.

\frac{d}{d\varepsilon}\Big|_{\varepsilon=0}\frac T2\int d^2\sigma\,\big(\mathcal L_P[X+\varepsilon\delta X]-\mathcal L_P[X]\big)=0,

then $X$ satisfies the wave equation

\Box X^\mu=\eta^{ab}\partial_a\partial_bX^\mu=\partial_\tau^2X^\mu-\partial_\sigma^2X^\mu=0.

This is the bulk equation of motion derived in the source's "Equations of motion" section.

Formalization Note. Variations are compactly supported, so the boundary terms of the source vanish and the variation is taken over the whole plane. The action difference is used so that the integral is finite even when $S[X]$ itself diverges.

Preamble

import Mathlib
import Definitions.Def_PolyakovAction_Defs

open MeasureTheory Filter Asymptotics
open scoped Matrix Topology

Formal statement

namespace PolyakovAction

theorem conformal_gauge_wave_equation {D : ℕ} (T : ℝ) (hT : T ≠ 0)
    (X : Worldsheet → Spacetime D) (hX : ContDiff ℝ 2 X)
    (hvar : ∀ δX : Worldsheet → Spacetime D, ContDiff ℝ (⊤ : ℕ∞) δX → HasCompactSupport δX →
      HasDerivAt
        (fun ε : ℝ => T / 2 * ∫ σ,
          (polyakovLagrangian (fun _ => minkowskiMetric D) (fun _ => minkowskiMetric 2)
              (fun σ' => X σ' + ε • δX σ') σ
            - polyakovLagrangian (fun _ => minkowskiMetric D) (fun _ => minkowskiMetric 2) X σ))
        0 0) :
    ∀ σ : Worldsheet, ∀ μ : Fin D,
      secondPartialDeriv X 0 0 μ σ - secondPartialDeriv X 1 1 μ σ = 0 := by sorry

end PolyakovAction

Source

Wikipedia, "Polyakov action", revision oldid=1292212311 (https://en.wikipedia.org/w/index.php?title=Polyakov_action&oldid=1292212311)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

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\neq0$ and map $X:\mathbb R^2\to\mathbb R^D$ that is $C^2$ , assume: for every $\delta X:\mathbb R^2\to\mathbb R^D$ that is $C^\infty$ (infinitely differentiable, not necessarily analytic) with compact support, the real function

\varepsilon\mapsto\frac T2\int_{\mathbb R^2}\Big(\mathcal L_P[\eta^{(D)},\eta^{(2)},X+\varepsilon\,\delta X](\sigma)-\mathcal L_P[\eta^{(D)},\eta^{(2)},X](\sigma)\Big)\,d^2\sigma

has derivative $0$ at $\varepsilon=0$ (target metric the constant $\eta^{(D)}$ , worldsheet metric the constant $\eta^{(2)}$ ). Then for every $\sigma\in\mathbb R^2$ and every $\mu$ :

\partial_0\partial_0X^\mu(\sigma)-\partial_1\partial_1X^\mu(\sigma)=0.

When $D=0$ the conclusion is vacuous.

Human review

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

View graph

Equations of motion in conformal gauge: □Xμ=0\Box X^\mu=0□Xμ=0

Equations of motion in conformal gauge: $\Box X^\mu=0$