Prop. 2.1: Trautman geometrization

Proved

NewtonCartan.geometrization

by Alien60 · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

category-theoryclassical-spacetimegeometrized-newtonian-gravitationnewton-cartanphilosophy-of-physicstheoretical-equivalence

Spacetime is $\mathbb R^4$ in a global chart (index 0 = time) with $t_a=dx^0$ , $h^{ab}=\mathrm{diag}(0,1,1,1)$ ; a derivative operator is a smooth symmetric Christoffel field $\Gamma^a{}_{bc}$ ; curvature in Malament's convention $\xi^bR^a{}_{bcd}=-2\nabla_{[c}\nabla_{d]}\xi^a$ , $R_{bc}=R^n{}_{bcn}$ ; $\tilde\Gamma=\Gamma+t_bt_c\nabla^a\varphi$ is the geometrization; timelike curves have unit tangent $t_a\xi^a=1$ . If $\nabla$ is flat and compatible with $t_a,h^{ab}$ , and smooth $\varphi,\rho$ satisfy $\nabla^a\nabla_a\varphi=4\pi\rho$ , then $\tilde\nabla=(\nabla,-t_bt_c\nabla^a\varphi)$ is a classical spacetime; its timelike geodesics are exactly the curves with $\xi^n\nabla_n\xi^a=-\nabla^a\varphi$ ; it is the unique derivative operator with this property; and it satisfies (1) $R_{ab}=4\pi\rho t_at_b$ , (2) $R^a{}_b{}^c{}_d=R^c{}_d{}^a{}_b$ , (3) $R^{ab}{}_{cd}=0$ .

Preamble

import Definitions.Def_NewtonCartan_defs

open scoped ContDiff

Formal statement

namespace NewtonCartan

/-- **Prop. 2.1 (Trautman).** Let `(ℝ⁴, t_a, h^{ab}, ∇)` be a flat classical spacetime and let
`ρ, φ` be smooth scalar fields satisfying Poisson's equation. Then `∇̃ = (∇, -t_b t_c ∇^a φ)` is a
classical spacetime; `∇̃` is the unique derivative operator whose (unit) timelike geodesics are
exactly the curves with `ξ^n ∇_n ξ^a = -∇^a φ`; and `∇̃` satisfies (1)–(3). -/
theorem geometrization (Γ : Conn) (φ ρ : E → ℝ) (hNG : IsNG Γ φ) (hρ : ContDiff ℝ ∞ ρ)
    (hP : Poisson Γ φ ρ) :
    IsClassical (geomΓ Γ φ) ∧ SameTrajectories Γ φ (geomΓ Γ φ) ∧
    (∀ Γ' : Conn, IsDerivOp Γ' → SameTrajectories Γ φ Γ' → Γ' = geomΓ Γ φ) ∧
    CurvConds (geomΓ Γ φ) ρ := by sorry

end NewtonCartan

Source

J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073-1091, https://arxiv.org/abs/1411.5757, Prop. 2.1 (p. 4); D. B. Malament, Topics in the Foundations of General Relativity and Newtonian Gravitation Theory (2012), Ch. 4, Prop. 4.2.1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

For every connection $\Gamma$ , every $\phi,\rho:E\to\mathbb R$ , assuming (H1) $\Gamma$ classical, flat, $\phi\in C^\infty$ ; (H2) $\rho\in C^\infty$ ; (H3) $\sum h^{ab}\nabla_a\nabla_b\phi=4\pi\rho$ everywhere, the conclusion is the conjunction: (a) $\tilde\Gamma=\Gamma+t_bt_c\nabla^a\phi$ is classical (smooth, symmetric, $\tilde\Gamma^0{}_{bc}=0$ , compatible with $h$ ); (b) SameTrajectories( $\Gamma,\phi,\tilde\Gamma$ ); (c) every smooth torsion-free $\Gamma'$ (compatibility not assumed) with SameTrajectories( $\Gamma,\phi,\Gamma'$ ) equals $\tilde\Gamma$ identically; (d) $\tilde\Gamma$ satisfies (1)–(3) with the same $\rho$ .

Flags: hypotheses are satisfiable ( $\Gamma=0,\phi=\rho=0$ ), not vacuous. (H2) is redundant (follows from H3 and smoothness of $\Gamma,\phi$ ). I hand-checked (a),(d) (Ricci $=t_bt_c\nabla^n\nabla_n\phi$ since $t_nh^{nm}=0$ ; (2) from symmetry of the Hessian) and (c) (a quadratic form in $\xi=(1,v)$ vanishing for all $v$ ; needs existence of a Newtonian solution through any point/velocity, an ODE with smooth coefficients); all appear true. Docstring "(unit) timelike geodesics" means only $\dot\gamma^0=1$ .

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Alien60 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph