Raised force tensor: $F^{\alpha\beta}=\partial^\alpha A^\beta-\partial^\beta A^\alpha+G^{\alpha\beta\gamma}A_\gamma$

Proved

RelPartMech.forceTensorUp_eq

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

mathematical-physicsrelativity

For a smooth metric $g$ and smooth covector field $A_\alpha$ with $A^\alpha=g^{\alpha\beta}A_\beta$ , let $F_{\alpha\beta}=\partial_\alpha A_\beta-\partial_\beta A_\alpha$ and $F^{\alpha\beta}=g^{\alpha\gamma}g^{\beta\delta}F_{\gamma\delta}$ . Then

F^{\alpha\beta} = \partial^\alpha A^\beta-\partial^\beta A^\alpha+G^{\alpha\beta\gamma}A_\gamma .

Unlike the covariant version, the raised force tensor is not the antisymmetrized raised derivative; $G$ measures the difference.

Preamble

import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff

Formal statement

namespace RelPartMech

theorem forceTensorUp_eq {n : ℕ} (g : MetricField n) (hg : IsSmoothMetric g)
    (A : CovectorField n) (hA : ∀ α, ContDiff ℝ ∞ (A α)) (α β : Fin n) (x : Coord n) :
    forceTensorUp g A α β x =
      pdUp g α (raise g A β) x - pdUp g β (raise g A α) x
        + ∑ γ, gSymbolUp g α β γ x * A γ x := by sorry

end RelPartMech

Source

G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 5, eq. (11), second 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 force tensor: Fαβ=∂αAβ−∂βAα+GαβγAγF^{\alpha\beta}=\partial^\alpha A^\beta-\partial^\beta A^\alpha+G^{\alpha\beta\gamma}A_\gammaFαβ=∂αAβ−∂βAα+GαβγAγ​

Raised force tensor: $F^{\alpha\beta}=\partial^\alpha A^\beta-\partial^\beta A^\alpha+G^{\alpha\beta\gamma}A_\gamma$