Prove2Me

{xα,uβ}=gαβ/m\{x^\alpha,u^\beta\}=g^{\alpha\beta}/m

Proved
RelPartMech.poisson_position_velocity

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

mathematical-physicsrelativity

With velocity uβ=1mgβγ(pγ−eAγ)u^\beta = \frac1m g^{\beta\gamma}(p_\gamma-eA_\gamma) (so that pα=mgαβuβ+eAαp_\alpha = m g_{\alpha\beta}u^\beta+eA_\alpha), smooth gg, AA and m≠0m\ne0,

{xα,uβ}=1m gαβ.\{x^\alpha,u^\beta\} = \frac1m\, g^{\alpha\beta}.
Preamble
import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff
Formal statement
namespace RelPartMech

theorem poisson_position_velocity {n : ℕ} (g : MetricField n) (hg : IsSmoothMetric g)
    (A : CovectorField n) (hA : ∀ α, ContDiff ℝ ∞ (A α)) (e m : ℝ) (hm : m ≠ 0)
    (α β : Fin n) (x p : Coord n) :
    poisson (posFn α) (velocity g A e m β) x p = (1 / m) * ginv g x α β := by sorry

end RelPartMech
Source
G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 6, eq. (13), 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