Prove2Me

SameTrajectories forces the spray of Γ' to match geomΓ on unit timelike vectors

Proved
NewtonCartan.sameTrajectories_diff_quad

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

malamentnewton-cartanweatherall

Let (∇,φ)(\nabla,\varphi) be a flat classical spacetime with potential (an object of NG), and let ∇′\nabla' be any torsion-free derivative operator whose unit-timelike geodesics are exactly the Newtonian trajectories of (∇,φ)(\nabla,\varphi). Writing ∇~\widetilde{\nabla} for the Trautman geometrization of (∇,φ)(\nabla,\varphi), one has

(Γ′abc−Γ~abc) ξbξc=0(\Gamma'^a{}_{bc}-\widetilde{\Gamma}^a{}_{bc})\,\xi^b\xi^c=0

at every point, for every unit-timelike ξ\xi (taξa=1t_a\xi^a=1).

The argument compares geodesic sprays: SameTrajectories\mathrm{SameTrajectories} identifies the unit-timelike geodesics of ∇′\nabla' with those of ∇~\widetilde{\nabla}, and existence of a unit-timelike ∇~\widetilde{\nabla}-geodesic with arbitrary initial velocity forces the quadratic forms of the Christoffel symbols to agree on that cone.

Preamble
import Definitions.Def_NewtonCartan_defs

open scoped ContDiff
Formal statement
namespace NewtonCartan

theorem sameTrajectories_diff_quad (Γ : Conn) (φ : E → ℝ) (hNG : IsNG Γ φ)
    (Γ' : Conn) (_hD : IsDerivOp Γ') (hS : SameTrajectories Γ φ Γ')
    (x : E) (a : Fin 4) (ξ : Fin 4 → ℝ) (hξ : ξ 0 = 1) :
    (∑ b : Fin 4, ∑ c : Fin 4,
        (Γ' x a b c - geomΓ Γ φ x a b c) * ξ b * ξ c) = 0 := by sorry

end NewtonCartan

View graph