Prove2Me

If G≡0G\equiv0 then the metric is a Hessian

Proved
RelPartMech.metric_hessian_of_gSymbol_zero

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

mathematical-physicsrelativity

Let gg be a smooth metric on the coordinate space Rn\mathbb R^n such that Gαβγ=∂αgβγ−∂βgαγG_{\alpha\beta\gamma}=\partial_\alpha g_{\beta\gamma}-\partial_\beta g_{\alpha\gamma} vanishes identically. Then there is a smooth scalar function SS with

gαβ=∂α∂βS.g_{\alpha\beta} = \partial_\alpha\partial_\beta S .

Formalization Note The source argues locally; here the chart is all of Rn\mathbb R^n, on which closed one-forms are exact.

Preamble
import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff
Formal statement
namespace RelPartMech

theorem metric_hessian_of_gSymbol_zero {n : ℕ} (g : MetricField n) (hg : IsSmoothMetric g)
    (hG : ∀ α β γ x, gSymbol g α β γ x = 0) :
    ∃ S : Coord n → ℝ, ContDiff ℝ ∞ S ∧ ∀ α β x, g x α β = pd α (pd β S) x := by sorry

end RelPartMech
Source
G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 9, eq. (16)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph