Prove2Me

Poincaré recovery of φ\varphi from the Trautman curvature form

Proved
NewtonCartan.exists_potential_of_tt_riem

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

malamentnewton-cartanpoincare-lemmatrautman

Assume a classical connection ∇~\widetilde{\nabla} satisfies CurvConds for a smooth density ρ\rho, and that its Riemann tensor has already been reduced to the Trautman form

Rabcd=tb(tcFad−tdFac),Fad=Ra00d.R^a{}_{bcd}=t_b(t_c F^a{}_d-t_d F^a{}_c),\qquad F^a{}_d=R^a{}_{00d}.

Then there exists a smooth potential φ\varphi such that the gauge-transformed connection

∇=(∇~, tbtc∇aφ)\nabla=(\widetilde{\nabla},\,t_b t_c\nabla^a\varphi)

is flat and compatible and satisfies Poisson's equation ∇a∇aφ=4πρ\nabla^a\nabla_a\varphi=4\pi\rho.

This packages the Poincaré-lemma integrability of FadF^a{}_d (from CurvConds (2)) together with the verification that the resulting gauge is an object of NG obeying Poisson (from CurvConds (1)).

Preamble
import Definitions.Def_NewtonCartan_defs

open scoped ContDiff
Formal statement
namespace NewtonCartan

/-- Poincaré / integrability step of Trautman recovery: if the Riemann tensor of a classical
`Γt` has the Trautman $t_b$-form coming from CurvConds, then there is a smooth potential `φ`
whose covectorially differentiated raised gradient reproduces `R^a{}_{00d}`, and for which
the gauge `gaugeΓ Γt φ` is an NG object obeying Poisson. -/
theorem exists_potential_of_tt_riem (Γt : Conn) (ρ : E → ℝ)
    (hΓt : IsClassical Γt) (hρ : ContDiff ℝ ∞ ρ) (hcurv : CurvConds Γt ρ)
    (hform : ∀ x a b c d,
      riem Γt x a b c d =
        tt b * (tt c * riem Γt x a 0 0 d - tt d * riem Γt x a 0 0 c)) :
    ∃ φ : E → ℝ, IsNG (gaugeΓ Γt φ) φ ∧ Poisson (gaugeΓ Γt φ) φ ρ := by sorry

end NewtonCartan
Source
D. B. Malament, Topics in the Foundations of GR and NGT (2012), Prop. 4.2.5; Weatherall arXiv:1411.5757 Prop. 2.2

View graph