Symmetric connection difference vanishing on unit timelike vectors is zero

Proved

NewtonCartan.conn_eq_of_unitTimelike_quad

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

malamentnewton-cartanweatherall

Let $C^a{}_{bc}$ be symmetric in $b,c$ . Suppose that for every unit-timelike vector $\xi^a$ (i.e. $t_a\xi^a=1$ ),

C^a{}_{bc}\xi^b\xi^c=0.

Then $C^a{}_{bc}=0$ identically.

This is the standard polarization of a quadratic form on the Newton–Cartan unit-timelike cone in a global chart on $\mathbb{R}^4$ : expanding in spatial velocity $(p,q,r)$ yields a quadratic polynomial that vanishes for all $(p,q,r)$ , hence all coefficients vanish.

Preamble

import Definitions.Def_NewtonCartan_defs

open scoped ContDiff

Formal statement

namespace NewtonCartan

theorem conn_eq_of_unitTimelike_quad (C : Fin 4 → Fin 4 → Fin 4 → ℝ)
    (hsym : ∀ a b c, C a b c = C a c b)
    (hquad : ∀ a (ξ : Fin 4 → ℝ), ξ 0 = 1 →
      (∑ b : Fin 4, ∑ c : Fin 4, C a b c * ξ b * ξ c) = 0) :
    ∀ a b c, C a b c = 0 := by sorry

end NewtonCartan

View graph