Prove2Me

Gauge by a spatial Hessian potential of Ra00dR^a{}_{00d} is NG and obeys Poisson

Proved
NewtonCartan.gauge_NG_poisson_of_spatial_hess

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

newton-cartanpoissontrautman

Let ∇~\widetilde{\nabla} be classical, satisfy CurvConds for ρ\rho, and have Trautman-form Riemann. Let φ\varphi be smooth with

∂j(∇iφ)=Ri00j(i,j spatial).\partial_j(\nabla^i\varphi)=R^i{}_{00j}\qquad(i,j\text{ spatial}).

Then ∇=(∇~,tbtc∇aφ)\nabla=(\widetilde{\nabla},t_b t_c\nabla^a\varphi) is flat and compatible, and ∇a∇aφ=4πρ\nabla^a\nabla_a\varphi=4\pi\rho.

Only spatial Hessian matching is required: the gauge modifies solely Γa00\Gamma^a{}_{00}, and flatness of the resulting Ri00jR^i{}_{00j} is exactly ∂j(gi−∂iφ)=0\partial_j(g^i-\partial^i\varphi)=0 after accounting for Coriolis/centrifugal terms already present in Ri00jR^i{}_{00j}.

Formalization Note. Corrects the retired gauge_NG_poisson_of_hessF.

Preamble
import Definitions.Def_NewtonCartan_defs

open scoped ContDiff
Formal statement
namespace NewtonCartan

/-- If $\partial_j(\nabla^i\varphi)=R^i{}_{00j}$ for spatial indices and $\Gamma t$ is classical with Trautman
form and CurvConds, then `gaugeΓ Γt φ` is NG and satisfies Poisson. -/
theorem gauge_NG_poisson_of_spatial_hess (Γt : Conn) (ρ : E → ℝ) (φ : E → ℝ)
    (hΓt : IsClassical Γt) (hρ : ContDiff ℝ ∞ ρ) (hcurv : CurvConds Γt ρ)
    (hφ : ContDiff ℝ ∞ φ)
    (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))
    (hhess : ∀ x i j, i ≠ 0 → j ≠ 0 →
      pd (fun y => gradUp φ y i) j x = riem Γt x i 0 0 j) :
    IsNG (gaugeΓ Γt φ) φ ∧ Poisson (gaugeΓ Γt φ) φ ρ := by sorry

end NewtonCartan
Source
Malament Prop. 4.2.5 / Weatherall Prop. 2.2

View graph