Trautman $F^a{}_d=R^a{}_{00d}$ is a closed spatial Hessian

Open

NewtonCartan.riem00_is_closed_F

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

curvaturenewton-cartantrautman

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

R^a{}_{bcd}=t_b(t_c F^a{}_d-t_d F^a{}_c),\qquad F^a{}_d=R^a{}_{00d}.

Then the field $F^a{}_d$ is smooth and satisfies

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

together with the trace identity $\sum_i F^i{}_i=4\pi\rho$ coming from CurvConds (1).

These are precisely the hypotheses of the Poincaré lemma that produces the recovering potential. Symmetry of $F$ is CurvConds (2) on the indices $(i,0,j,0)$ ; vanishing of temporal components uses $\Gamma^0{}_{bc}=0$ and antisymmetry of Riemann; closedness of the spatial Hessian follows from the Bianchi identity / equality of mixed partials of the Christoffel symbols under ContDiff; the trace is Ricci.

Formalization Note. Uses riem, CurvConds, and pd from Def_NewtonCartan_defs.

DEPRECATED: the universal closed-Hessian condition ∀ i j k, ∂_k F^i_j = ∂_j F^i_k (including temporal indices) is false for Trautman F. Counterexample: Γ^i_00 = x^i f(t) gives F^i_j = δ^i_j f(t) with ∂_0 F ≠ 0 while F^i_0 = 0. Replaced by NewtonCartan.riem00_spatial_closed_F (spatial indices only).

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 spatial Hessian; its trace is $4\pi\rho$. -/
theorem riem00_is_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, 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

Trautman Fad=Ra00dF^a{}_d=R^a{}_{00d}Fad​=Ra00d​ is a closed spatial Hessian

Trautman $F^a{}_d=R^a{}_{00d}$ is a closed spatial Hessian