Poincaré lemma: spatial Hessian data integrate to a potential on $\mathbb{R}^4$

Open

NewtonCartan.exists_potential_of_closed_F

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

newton-cartanpoincare-lemmatrautman

Let $F^a{}_d$ be a smooth $(1,1)$ -tensor field on $\mathbb{R}^4$ (indices relative to the standard global chart) satisfying

F^0{}_d = 0,\qquad F^a{}_0 = 0,\qquad F^i{}_j = F^j{}_i,

and the closed-Hessian condition

\partial_k F^i{}_j = \partial_j F^i{}_k

for all spatial indices. Then there exists a smooth scalar potential $\varphi$ such that

\partial_d\bigl(h^{an}\partial_n\varphi\bigr) = F^a{}_d

everywhere. Equivalently, the spatial Hessian of $\varphi$ recovers $F$ on spatial indices, while the temporal component of the raised gradient vanishes identically.

This is the global Poincaré lemma on the contractible chart $\mathbb{R}^4$ for Hessian data; it is the analytic step in Trautman recovery once CurvConds have reduced the Riemann tensor to $R^a{}_{00d}=F^a{}_d$ .

Formalization Note. pd and gradUp are as in Def_NewtonCartan_defs; ContDiff ℝ ∞ F is ContDiff of the uncurried map E → Fin 4 → Fin 4 → ℝ.

DEPRECATED: required full closedness including time, which Trautman F need not satisfy. Replaced by NewtonCartan.exists_potential_of_spatial_F.

Preamble

import Definitions.Def_NewtonCartan_defs

open scoped ContDiff

Formal statement

namespace NewtonCartan

/-- If $F^a{}_d$ is smooth, vanishes whenever $a=0$ or $d=0$, is symmetric in its spatial indices, and is closed as a spatial Hessian ($\partial_k F^i{}_j = \partial_j F^i{}_k$), then there is a smooth $\varphi$ with $\partial_d(\nabla^a\varphi) = F^a{}_d$. -/
theorem exists_potential_of_closed_F (F : E → Fin 4 → Fin 4 → ℝ)
    (hF : ContDiff ℝ ∞ F)
    (hrow : ∀ x d, F x 0 d = 0) (hcol : ∀ x a, F x a 0 = 0)
    (hsym : ∀ x i j, F x i j = F x j i)
    (hclosed : ∀ x i j k,
      pd (fun y => F y i j) k x = pd (fun y => F y i k) j x) :
    ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧
      ∀ x a d, pd (fun y => gradUp φ y a) d x = F x a d := by sorry

end NewtonCartan

Source

Malament Prop. 4.2.5 / Weatherall Prop. 2.2 (Poincaré step); Schwartz, Newton–Cartan gravity, Thm. 2.29

View graph

Poincaré lemma: spatial Hessian data integrate to a potential on R4\mathbb{R}^4R4

Poincaré lemma: spatial Hessian data integrate to a potential on $\mathbb{R}^4$