Prove2Me

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

Open
NewtonCartan.gauge_NG_poisson_of_hessF

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

newton-cartanpoissontrautman

Let ∇~\widetilde{\nabla} be a classical Newton–Cartan connection on (R4,ta,hab)(\mathbb{R}^4,t_a,h^{ab}) satisfying CurvConds for a smooth density ρ\rho, and suppose its Riemann tensor has 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}.

Let φ\varphi be a smooth potential whose raised gradient reproduces this field:

∂d(∇aφ)=Ra00d.\partial_d(\nabla^a\varphi)=R^a{}_{00d}.

Then the gauge-transformed connection

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

is flat and compatible (hence an object of NG), and φ\varphi obeys Poisson's equation ∇a∇aφ=4πρ\nabla^a\nabla_a\varphi=4\pi\rho with respect to ∇\nabla.

The flatness computation uses the classical Christoffel reduction Γ0bc=Γijk=0\Gamma^0{}_{bc}=\Gamma^i{}_{jk}=0 together with the Hessian identity to cancel all components of Rabcd(∇)R^a{}_{bcd}(\nabla); Poisson follows by tracing CurvConds (1) against the same identity.

Formalization Note. gaugeΓ, IsNG, Poisson, and CurvConds are as in Def_NewtonCartan_defs.

DEPRECATED: required ∂_d(∇^a φ) = R^a_00d for temporal d as well, which is stronger than needed for gauge flatness. Replaced by NewtonCartan.gauge_NG_poisson_of_spatial_hess.

Preamble
import Definitions.Def_NewtonCartan_defs

open scoped ContDiff
Formal statement
namespace NewtonCartan

/-- If $\partial_d(\nabla^a\varphi)=R^a{}_{00d}$ and $\Gamma t$ is classical with Trautman $t_b$-form curvature and CurvConds, then `gaugeΓ Γt φ` is NG and satisfies Poisson. -/
theorem gauge_NG_poisson_of_hessF (Γ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 a d, pd (fun y => gradUp φ y a) d x = riem Γt x a 0 0 d) :
    IsNG (gaugeΓ Γt φ) φ ∧ Poisson (gaugeΓ Γt φ) φ ρ := by sorry

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

View graph