Existence of a recovering potential for CurvConds

Proved

NewtonCartan.exists_recovery_potential

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

malamentnewton-cartanpoincare-lemmatrautmanweatherall

Let $(\mathbb R^4,t_a,h^{ab},\widetilde{\nabla})$ be a classical spacetime satisfying the Trautman–Malament curvature conditions (1)–(3) for a smooth mass density $\rho$ . Then there exists a smooth gravitational potential $\varphi$ such that the gauge-transformed connection

\nabla=(\widetilde{\nabla},\,t_b t_c\widetilde{\nabla}^a\varphi)

(i.e. $\Gamma^a{}_{bc}=\widetilde{\Gamma}^a{}_{bc}-t_b t_c\nabla^a\varphi$ ) is flat and compatible, and $(\nabla,\varphi)$ satisfies Poisson's equation $\nabla^a\nabla_a\varphi=4\pi\rho$ .

In the formalization, $\nabla$ is written gaugeΓ Γt φ. This is the existence/Poincaré-lemma content of Weatherall Prop. 2.2 / Malament Prop. 4.2.5; together with the identity $\mathrm{geom}\Gamma(\mathrm{gauge}\Gamma(\widetilde{\Gamma},\varphi),\varphi)=\widetilde{\Gamma}$ it yields Trautman recovery.

Preamble

import Definitions.Def_NewtonCartan_defs

open scoped ContDiff

Formal statement

namespace NewtonCartan

theorem exists_recovery_potential (Γt : Conn) (ρ : E → ℝ)
    (hΓt : IsClassical Γt) (hρ : ContDiff ℝ ∞ ρ) (hcurv : CurvConds Γt ρ) :
    ∃ φ : E → ℝ, IsNG (gaugeΓ Γt φ) φ ∧ Poisson (gaugeΓ Γt φ) φ ρ := by sorry

end NewtonCartan

Source

J. O. Weatherall, arXiv:1411.5757, Prop. 2.2 (pp. 4-5); D. B. Malament, Topics in the Foundations of GR and NGT (2012), Prop. 4.2.5

View graph