$G_{\alpha\beta\gamma}=\Gamma_{\beta\alpha\gamma}-\Gamma_{\alpha\beta\gamma}$

Proved

RelPartMech.gSymbol_eq_christoffel_diff

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsrelativity

For a smooth symmetric metric $g$ , define $G_{\alpha\beta\gamma}=\partial_\alpha g_{\beta\gamma}-\partial_\beta g_{\alpha\gamma}$ and the Christoffel symbols of the first kind $\Gamma_{\alpha\beta\gamma}=\frac12(\partial_\gamma g_{\alpha\beta}+\partial_\beta g_{\alpha\gamma}-\partial_\alpha g_{\beta\gamma})$ . Then

G_{\alpha\beta\gamma} = \Gamma_{\beta\alpha\gamma}-\Gamma_{\alpha\beta\gamma}.

So $G$ antisymmetrizes the first two indices of the Christoffel symbols (unlike torsion, which uses the last two).

Preamble

import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff

Formal statement

namespace RelPartMech

theorem gSymbol_eq_christoffel_diff {n : ℕ} (g : MetricField n) (hg : IsSmoothMetric g)
    (α β γ : Fin n) (x : Coord n) :
    gSymbol g α β γ x = christoffelFirst g β α γ x - christoffelFirst g α β γ x := by sorry

end RelPartMech

Source

G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 5, eq. (10), definition of G and the identity below it

Human review

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

View graph

Gαβγ=Γβαγ−ΓαβγG_{\alpha\beta\gamma}=\Gamma_{\beta\alpha\gamma}-\Gamma_{\alpha\beta\gamma}Gαβγ​=Γβαγ​−Γαβγ​

$G_{\alpha\beta\gamma}=\Gamma_{\beta\alpha\gamma}-\Gamma_{\alpha\beta\gamma}$