Light-cone form of the general solution
ProvedPolyakovAction.wave_equation_lightcone_solutionLet be and satisfy everywhere (equivalently in light-cone coordinates ). Then there are functions with
This is the source's statement "the solution can be written as ".
Formalization Note. Stated on the whole plane ; boundary conditions for closed/open strings are not part of this statement.
import Mathlib import Definitions.Def_PolyakovAction_Defs open MeasureTheory Filter Asymptotics open scoped Matrix Topology
namespace PolyakovAction
theorem wave_equation_lightcone_solution {D : ℕ} (X : Worldsheet → Spacetime D)
(hX : ContDiff ℝ 2 X)
(hwave : ∀ σ : Worldsheet, ∀ μ : Fin D,
secondPartialDeriv X 0 0 μ σ - secondPartialDeriv X 1 1 μ σ = 0) :
∃ XL XR : ℝ → Spacetime D, ContDiff ℝ 2 XL ∧ ContDiff ℝ 2 XR ∧
∀ τ s : ℝ, X ![τ, s] = XL (τ + s) + XR (τ - s) := by sorry
end PolyakovActionRead-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, is a worldsheet point (index is , index is ), is the embedding, is the -th component of the Fréchet derivative of at applied to the -th standard basis vector (it is wherever is not differentiable), is the induced metric, denotes the entries of the matrix inverse (Mathlib's inverse, which is the zero matrix when ), and is the real square root, which returns on negative inputs. The Polyakov density is , the Polyakov action on a set is (Lebesgue measure; Bochner integral, equal to if the integrand is not integrable on ), and the Nambu–Goto action is . The stress–energy tensor is , and is the Minkowski matrix.
Statement. For every and map that is and satisfies for every and every , there exist , both , such that for all real :
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.