Malament (4.2.8): Riemann tensor after Trautman geometrization

Proved

NewtonCartan.riem_geomGamma

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

curvaturenewton-cartantrautman-geometrization

Let $(\mathbb R^4,t_a,h^{ab},\nabla)$ be a flat classical spacetime with smooth potential $\varphi$ , and let $\tilde\nabla=(\nabla,-t_bt_c\nabla^a\varphi)$ be its Trautman geometrization. Then the Riemann curvature of $\tilde\nabla$ is

\tilde R^a{}_{bcd}=t_b\bigl(t_c\nabla_d\nabla^a\varphi-t_d\nabla_c\nabla^a\varphi\bigr).

Quadratic $C\cdot C$ terms vanish because $\nabla^a\varphi$ is spatial; mixed $C\Gamma$ terms vanish by $\nabla t=0$ .

Preamble

import Definitions.Def_NewtonCartan_defs

open scoped ContDiff

Formal statement

namespace NewtonCartan

theorem riem_geomGamma (Γ : Conn) (φ : E → ℝ) (hNG : IsNG Γ φ) (x : E) (a b c d : Fin 4) :
    riem (geomΓ Γ φ) x a b c d =
      tt b * (tt c * (pd (fun y => gradUp φ y a) d x +
          ∑ e : Fin 4, Γ x a d e * gradUp φ x e) -
        tt d * (pd (fun y => gradUp φ y a) c x +
          ∑ e : Fin 4, Γ x a c e * gradUp φ x e)) := by sorry

end NewtonCartan

Source

D. B. Malament, Topics… (2012), Prop. 4.2.1 proof, eq. (4.2.8) (p. 268); Weatherall arXiv:1411.5757 Prop. 2.1 (G3)

View graph