Polyakov action reduces to the Nambu–Goto action on-shell

Proved

PolyakovAction.polyakov_eq_nambuGoto

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

mathematical-physicsstring-theory

Let $T$ be the string tension, $g_{\mu\nu}$ a target metric, $X$ the embedding of the worldsheet, $h_{ab}$ the worldsheet metric, and $G_{ab}=g_{\mu\nu}(X)\partial_aX^\mu\partial_bX^\nu$ the induced metric. Suppose that on a measurable worldsheet region $U$ the metric equations of motion hold,

T_{ab}=T\Big(G_{ab}-\tfrac12h_{ab}h^{cd}G_{cd}\Big)=0,

and that $h^{cd}G_{cd}\ge0$ on $U$ . Then the Polyakov action equals the Nambu–Goto action:

\frac T2\int_U d^2\sigma\,\sqrt{-h}\,h^{ab}G_{ab}=T\int_U d^2\sigma\,\sqrt{-G}.

This is the classical equivalence of the two string actions ("Relation with Nambu–Goto action" in the source): solving the auxiliary metric's equation of motion, $\sqrt{-h}=2\sqrt{-G}/(h^{cd}G_{cd})$ , and substituting back gives the Nambu–Goto action.

Formalization Note. The positivity $h^{cd}G_{cd}\ge0$ is implicit in the source's formula $\sqrt{-h}=2\sqrt{-G}/(h^{cd}G_{cd})$ (both square roots are non-negative); without it the two actions differ by a sign. No signature condition on $h$ is needed for the identity.

Preamble

import Mathlib
import Definitions.Def_PolyakovAction_Defs

open MeasureTheory Filter Asymptotics
open scoped Matrix Topology

Formal statement

namespace PolyakovAction

theorem polyakov_eq_nambuGoto {D : ℕ} (T : ℝ) (g : Spacetime D → Matrix (Fin D) (Fin D) ℝ)
    (h : Worldsheet → Matrix (Fin 2) (Fin 2) ℝ) (X : Worldsheet → Spacetime D)
    (U : Set Worldsheet) (hU : MeasurableSet U)
    (heom : ∀ σ ∈ U, stressEnergyTensor T g h X σ = 0)
    (hpos : ∀ σ ∈ U, 0 ≤ ∑ c, ∑ d, (h σ)⁻¹ c d * inducedMetric g X σ c d) :
    polyakovAction T g h X U = nambuGotoAction T g X U := 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 natural number $D$ , real $T$ , target metric $g:\mathbb R^D\to\mathbb R^{D\times D}$ (arbitrary), worldsheet metric $h:\mathbb R^2\to\mathbb R^{2\times2}$ (arbitrary, no symmetry, invertibility or signature assumed), map $X:\mathbb R^2\to\mathbb R^D$ (no differentiability assumed) and set $U\subseteq\mathbb R^2$ , assume

$U$ is Lebesgue (Borel) measurable;
for every $\sigma\in U$ the matrix $T_{ab}(\sigma)$ is the zero matrix;
for every $\sigma\in U$ , $\sum_{c,d}h^{cd}(\sigma)G_{cd}(\sigma)\ge0$ .

Then

\frac T2\int_U\sqrt{-\det h}\,\sum_{a,b}h^{ab}G_{ab}\,d^2\sigma \;=\; T\int_U\sqrt{-\det G}\,d^2\sigma .

Edge cases: if $T=0$ , hypothesis 2 holds trivially and both sides are $0$ . Both integrals use the convention that a non-integrable integrand has integral $0$ ; no integrability is assumed.

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