Raised form of $G$ : $G^{\alpha\beta\gamma}=\partial^\beta g^{\alpha\gamma}-\partial^\alpha g^{\beta\gamma}$

Proved

RelPartMech.gSymbolUp_eq

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

mathematical-physicsrelativity

For a smooth metric $g$ , raise all indices of $G$ : $G^{\alpha\beta\gamma}=g^{\alpha\delta}g^{\beta\epsilon}g^{\gamma\zeta}G_{\delta\epsilon\zeta}$ , and write $\partial^\alpha=g^{\alpha\beta}\partial_\beta$ . Then

G^{\alpha\beta\gamma} = \partial^\beta g^{\alpha\gamma}-\partial^\alpha g^{\beta\gamma}.

Preamble

import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff

Formal statement

namespace RelPartMech

theorem gSymbolUp_eq {n : ℕ} (g : MetricField n) (hg : IsSmoothMetric g)
    (α β γ : Fin n) (x : Coord n) :
    gSymbolUp g α β γ x =
      pdUp g β (fun y => ginv g y α γ) x - pdUp g α (fun y => ginv g y β γ) x := by sorry

end RelPartMech

Source

G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 5, eq. (11), first block

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

Raised form of GGG: Gαβγ=∂βgαγ−∂αgβγG^{\alpha\beta\gamma}=\partial^\beta g^{\alpha\gamma}-\partial^\alpha g^{\beta\gamma}Gαβγ=∂βgαγ−∂αgβγ

Raised form of $G$ : $G^{\alpha\beta\gamma}=\partial^\beta g^{\alpha\gamma}-\partial^\alpha g^{\beta\gamma}$