Prop. 2.2: Trautman recovery

Proved

NewtonCartan.recovery

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 $\tilde\nabla$ is a classical spacetime satisfying (1)-(3) for some smooth $\rho$ , there are a smooth $\varphi$ and a flat compatible $\nabla$ such that the timelike geodesics of $\tilde\nabla$ are exactly the curves with $\xi^n\nabla_n\xi^a=-\nabla^a\varphi$ , and $\nabla^a\nabla_a\varphi=4\pi\rho$ .

Preamble

import Definitions.Def_NewtonCartan_defs

open scoped ContDiff

Formal statement

namespace NewtonCartan

/-- **Prop. 2.2 (Trautman).** Let `(ℝ⁴, t_a, h^{ab}, ∇̃)` be a classical spacetime satisfying
conditions (1)–(3) of Prop. 2.1 for some smooth `ρ`. Then there are a smooth `φ` and a flat derivative
operator `∇` such that `(ℝ⁴, t_a, h^{ab}, ∇)` is a classical spacetime, the timelike geodesics of `∇̃`
are exactly the curves with `ξ^n ∇_n ξ^a = -∇^a φ`, and `∇, φ` satisfy Poisson's equation. -/
theorem recovery (Γt : Conn) (ρ : E → ℝ) (hΓt : IsClassical Γt) (hρ : ContDiff ℝ ∞ ρ)
    (hcurv : CurvConds Γt ρ) :
    ∃ (Γ : Conn) (φ : E → ℝ), IsNG Γ φ ∧ SameTrajectories Γ φ Γt ∧ Poisson Γ φ ρ := 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.2 (pp. 4-5); D. B. Malament, Topics in the Foundations of General Relativity and Newtonian Gravitation Theory (2012), Ch. 4, Prop. 4.2.5

Read-back

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

For every classical $\Gamma_t$ and every $C^\infty$ $\rho$ with CurvConds( $\Gamma_t,\rho$ ), there exist a connection $\Gamma$ and function $\phi$ with $\Gamma$ classical and flat, $\phi\in C^\infty$ , SameTrajectories( $\Gamma,\phi,\Gamma_t$ ), and $\sum h^{ab}\nabla_a\nabla_b\phi=4\pi\rho$ everywhere.

Flags: hypotheses satisfiable ( $\Gamma_t=0,\rho=0$ ). $\rho$ -smoothness is redundant (follows from (1)). The true statement needs contractibility of $\mathbb R^4$ (Trautman/Malament 4.2.x); a genuinely hard existence theorem, no hypotheses appear missing. No uniqueness asserted.

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