Polyakov action: worldsheet, induced metric, Polyakov and Nambu–Goto actions, stress–energy tensor

Definition

PolyakovAction_Defs

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

mathematical-physicsstring-theory

Shared definitions for the Polyakov-action mission (namespace PolyakovAction). Worldsheet points are $\sigma=(\sigma^0,\sigma^1)=(\tau,\sigma)\in\mathbb R^2$ and target points $X\in\mathbb R^D$ .

Partial derivatives. $\partial_a X^\mu(\sigma)$ and $\partial_a\partial_b X^\mu(\sigma)$ , computed from the Fréchet derivative of $X:\mathbb R^2\to\mathbb R^D$ .
Induced metric. $G_{ab}(\sigma)=g_{\mu\nu}(X(\sigma))\,\partial_aX^\mu(\sigma)\,\partial_bX^\nu(\sigma)$ for a target metric $g:\mathbb R^D\to\mathbb R^{D\times D}$ .
Polyakov action. For a worldsheet metric $h_{ab}(\sigma)$ with inverse $h^{ab}$ and determinant $h=\det(h_{ab})$ , and string tension $T$ ,

S=\frac T2\int_U d^2\sigma\,\sqrt{-h}\,h^{ab}g_{\mu\nu}(X)\,\partial_aX^\mu\,\partial_bX^\nu .

Nambu–Goto action. $S_{NG}=T\int_U d^2\sigma\,\sqrt{-G}$ , $G=\det(G_{ab})$ .
Stress–energy tensor. $T_{ab}=T\big(G_{ab}-\tfrac12h_{ab}h^{cd}G_{cd}\big)$ .
Minkowski metric. $\eta=\mathrm{diag}(+1,-1,\dots,-1)$ (timelike $+$ , spacelike $-$ , as in the source).

These are the objects in terms of which every statement of the mission is phrased.

Formalization Note. Indices are Fin 2 / Fin D; $h^{ab}$ is Mathlib's matrix inverse (zero for a singular matrix); $\sqrt{\cdot}$ is Real.sqrt (zero on negative inputs); integrals are Bochner integrals for Lebesgue measure on $\mathbb R^2$ restricted to $U$ .

Definition code

import Mathlib

namespace PolyakovAction

open MeasureTheory

/-- Worldsheet coordinates `σ = (σ 0, σ 1) = (τ, σ)`: index `0` is the timelike
coordinate `τ`, index `1` the spacelike coordinate `σ`. -/
abbrev Worldsheet := Fin 2 → ℝ

/-- The `D`-dimensional target manifold (coordinates `X^μ`). -/
abbrev Spacetime (D : ℕ) := Fin D → ℝ

/-- `∂_a X^μ (σ)`: partial derivative of the `μ`-th component of the embedding
`X` with respect to the worldsheet coordinate `σ^a`. -/
noncomputable def partialDeriv {D : ℕ} (X : Worldsheet → Spacetime D) (a : Fin 2)
    (μ : Fin D) (σ : Worldsheet) : ℝ :=
  fderiv ℝ X σ (Pi.single a 1) μ

/-- `∂_a ∂_b X^μ (σ)`: second partial derivative of the `μ`-th component of `X`. -/
noncomputable def secondPartialDeriv {D : ℕ} (X : Worldsheet → Spacetime D) (a b : Fin 2)
    (μ : Fin D) (σ : Worldsheet) : ℝ :=
  fderiv ℝ (fun σ' => fderiv ℝ X σ' (Pi.single b 1)) σ (Pi.single a 1) μ

/-- Induced (pull-back) metric `G_ab = g_μν(X) ∂_a X^μ ∂_b X^ν`. -/
noncomputable def inducedMetric {D : ℕ} (g : Spacetime D → Matrix (Fin D) (Fin D) ℝ)
    (X : Worldsheet → Spacetime D) (σ : Worldsheet) : Matrix (Fin 2) (Fin 2) ℝ :=
  Matrix.of fun a b => ∑ μ, ∑ ν, g (X σ) μ ν * partialDeriv X a μ σ * partialDeriv X b ν σ

/-- Polyakov Lagrangian density `√(-h) h^{ab} g_μν(X) ∂_a X^μ ∂_b X^ν`, where
`h = det (h_ab)` and `h^{ab}` is the inverse of the worldsheet metric `h_ab`. -/
noncomputable def polyakovLagrangian {D : ℕ} (g : Spacetime D → Matrix (Fin D) (Fin D) ℝ)
    (h : Worldsheet → Matrix (Fin 2) (Fin 2) ℝ) (X : Worldsheet → Spacetime D)
    (σ : Worldsheet) : ℝ :=
  Real.sqrt (-(h σ).det) * ∑ a, ∑ b, (h σ)⁻¹ a b * inducedMetric g X σ a b

/-- Polyakov action over a worldsheet region `U`:
`S = (T/2) ∫_U d²σ √(-h) h^{ab} g_μν(X) ∂_a X^μ ∂_b X^ν`. -/
noncomputable def polyakovAction {D : ℕ} (T : ℝ) (g : Spacetime D → Matrix (Fin D) (Fin D) ℝ)
    (h : Worldsheet → Matrix (Fin 2) (Fin 2) ℝ) (X : Worldsheet → Spacetime D)
    (U : Set Worldsheet) : ℝ :=
  T / 2 * ∫ σ in U, polyakovLagrangian g h X σ

/-- Nambu–Goto action over a worldsheet region `U`: `S = T ∫_U d²σ √(-G)`, `G = det G_ab`. -/
noncomputable def nambuGotoAction {D : ℕ} (T : ℝ) (g : Spacetime D → Matrix (Fin D) (Fin D) ℝ)
    (X : Worldsheet → Spacetime D) (U : Set Worldsheet) : ℝ :=
  T * ∫ σ in U, Real.sqrt (-(inducedMetric g X σ).det)

/-- Stress–energy tensor (lower indices) `T_ab = T (G_ab - ½ h_ab h^{cd} G_cd)`. -/
noncomputable def stressEnergyTensor {D : ℕ} (T : ℝ)
    (g : Spacetime D → Matrix (Fin D) (Fin D) ℝ) (h : Worldsheet → Matrix (Fin 2) (Fin 2) ℝ)
    (X : Worldsheet → Spacetime D) (σ : Worldsheet) : Matrix (Fin 2) (Fin 2) ℝ :=
  Matrix.of fun a b => T * (inducedMetric g X σ a b
    - 1 / 2 * h σ a b * ∑ c, ∑ d, (h σ)⁻¹ c d * inducedMetric g X σ c d)

/-- Minkowski metric `diag(+1, -1, …, -1)` on `ℝⁿ` (timelike `+`, spacelike `-`). -/
def minkowskiMetric (n : ℕ) : Matrix (Fin n) (Fin n) ℝ :=
  Matrix.diagonal fun i => if i.val = 0 then 1 else -1

end PolyakovAction

Source

Wikipedia, "Polyakov action", revision oldid=1292212311 (https://en.wikipedia.org/w/index.php?title=Polyakov_action&oldid=1292212311), lead section and sections "Relation with Nambu–Goto action", "Equations of motion"

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.

The file declares, inside the namespace PolyakovAction:

$\mathrm{Worldsheet}=\mathbb R^{2}$ (functions $\{0,1\}\to\mathbb R$ ) and $\mathrm{Spacetime}(D)=\mathbb R^{D}$ .
$\partial_aX^\mu(\sigma)$ : for $X:\mathbb R^2\to\mathbb R^D$ , the $\mu$ -th coordinate of $DX(\sigma)e_a$ , where $DX(\sigma)$ is the Fréchet derivative (defined to be the zero map if $X$ is not differentiable at $\sigma$ ) and $e_a$ the $a$ -th standard basis vector.
$\partial_a\partial_bX^\mu(\sigma)$ : the $\mu$ -th coordinate of the derivative at $\sigma$ , in direction $e_a$ , of the map $\sigma'\mapsto DX(\sigma')e_b$ (again with zero junk at non-differentiable points).
$G_{ab}(\sigma)=\sum_{\mu,\nu=1}^{D} g(X(\sigma))_{\mu\nu}\,\partial_aX^\mu(\sigma)\,\partial_bX^\nu(\sigma)$ for an arbitrary matrix-valued $g$ (no symmetry or signature is imposed).
$\mathcal L_P(\sigma)=\sqrt{-\det h(\sigma)}\;\sum_{a,b\in\{0,1\}}\big(h(\sigma)^{-1}\big)_{ab}\,G_{ab}(\sigma)$ for an arbitrary $2\times2$ -matrix-valued $h$ ; here $\sqrt{x}=0$ for $x<0$ and $h^{-1}=0$ when $\det h=0$ .
$S_P(T,g,h,X,U)=\dfrac T2\displaystyle\int_U \mathcal L_P(\sigma)\,d\sigma$ (Lebesgue measure on $\mathbb R^2$ ; value $0$ if the integrand is not integrable on $U$ ).
$S_{NG}(T,g,X,U)=T\displaystyle\int_U\sqrt{-\det G(\sigma)}\,d\sigma$ , same conventions.
$T_{ab}(\sigma)=T\Big(G_{ab}(\sigma)-\tfrac12\,h(\sigma)_{ab}\sum_{c,d}(h(\sigma)^{-1})_{cd}G_{cd}(\sigma)\Big)$ .
$\eta^{(n)}$ : the $n\times n$ diagonal matrix with entry $+1$ at index $0$ and $-1$ at every other index.

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