Geometrization preserves Newtonian trajectories

Proved

NewtonCartan.sameTrajectories_geomGamma

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

malamentnewton-cartantrautmanweatherall

Let $\nabla$ be any torsion-free derivative operator on $\mathbb R^4$ and $\varphi$ any smooth scalar field. Writing $\widetilde{\nabla}$ for the Trautman geometrization $(\nabla,-t_b t_c\nabla^a\varphi)$ , a unit-timelike curve is a $\widetilde{\nabla}$ -geodesic if and only if it satisfies Newton's law $\xi^n\nabla_n\xi^a=-\nabla^a\varphi$ . Equivalently, $\mathrm{SameTrajectories}(\nabla,\varphi,\widetilde{\nabla})$ holds.

This is the empirical-content half of Weatherall's Prop. 2.1 / Malament Prop. 4.2.1 (G1), and is reused in the Trautman recovery (Prop. 2.2).

Preamble

import Definitions.Def_NewtonCartan_defs

open scoped ContDiff

Formal statement

namespace NewtonCartan

theorem sameTrajectories_geomGamma (Γ : Conn) (φ : E → ℝ) :
    SameTrajectories Γ φ (geomΓ Γ φ) := by sorry

end NewtonCartan

Source

J. O. Weatherall, arXiv:1411.5757, Prop. 2.1; D. B. Malament, Topics in the Foundations of GR and NGT (2012), Prop. 4.2.1 (G1)

View graph