Prove2Me

Trautman Fad=Ra00dF^a{}_d=R^a{}_{00d} is spatially closed as a Hessian

Proved
NewtonCartan.riem00_spatial_closed_F

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

curvaturenewton-cartantrautman

Assume a classical connection ∇~\widetilde{\nabla} on (R4,ta,hab)(\mathbb{R}^4,t_a,h^{ab}) satisfies CurvConds for smooth ρ\rho and that 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}.

Then FF is smooth and satisfies F0d=0F^0{}_d=0, Fa0=0F^a{}_0=0, Fij=FjiF^i{}_j=F^j{}_i, the spatial closed-Hessian identity

∂kFij=∂jFik(i,j,k∈{1,2,3}),\partial_k F^i{}_j=\partial_j F^i{}_k\qquad(i,j,k\in\{1,2,3\}),

and ∑iFii=4πρ\sum_i F^i{}_i=4\pi\rho.

Temporal closedness need not hold: Γi00=xif(t)\Gamma^i{}_{00}=x^i f(t) yields Fij=δijf(t)F^i{}_j=\delta^i{}_j f(t) with ∂0F≠0\partial_0 F\neq 0. Spatial closedness is the integrability needed to recover φ\varphi slicewise.

Formalization Note. Corrects the retired riem00_is_closed_F. Uses classical_christoffel_form.

Preamble
import Definitions.Def_NewtonCartan_defs

open scoped ContDiff
Formal statement
namespace NewtonCartan

/-- Under CurvConds and the Trautman $t_b$-form, $F^a{}_d := R^a{}_{00d}$ is smooth, vanishes on
temporal indices, is symmetric, and is closed as a Hessian in the *spatial* indices; its trace is $4\pi\rho$.
(Temporal closedness $\partial_0 F^i{}_j = \partial_j F^i{}_0$ can fail, e.g. $\Gamma^i{}_{00}=x^i f(t)$.) -/
theorem riem00_spatial_closed_F (Γ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)) :
    let F : E → Fin 4 → Fin 4 → ℝ := fun x a d => riem Γt x a 0 0 d
    ContDiff ℝ ∞ F ∧
      (∀ x d, F x 0 d = 0) ∧ (∀ x a, F x a 0 = 0) ∧
      (∀ x i j, F x i j = F x j i) ∧
      (∀ x i j k, i ≠ 0 → j ≠ 0 → k ≠ 0 →
        pd (fun y => F y i j) k x = pd (fun y => F y i k) j x) ∧
      (∀ x, ∑ i : Fin 4, F x i i = 4 * Real.pi * ρ x) := by sorry

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

View graph