Hamilton's equation for position: $m g_{\alpha\beta}\, d_s x^\beta = \Pi_\alpha$

Proved

RelPartMech.position_evolution

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

mathematical-physicsrelativity

Let $H=\frac1{2m}\Pi_\alpha g^{\alpha\beta}\Pi_\beta$ with $\Pi_\alpha=p_\alpha-eA_\alpha(x)$ , a smooth metric $g$ and smooth potential $A$ , and mass $m\neq0$ . Then the evolution of the position along the affine parameter $s$ generated by $H$ is

d_s x^\alpha = \{x^\alpha,H\} = \frac1m\, g^{\alpha\beta}\Pi_\beta ,

equivalently $m\,g_{\alpha\beta}\,d_s x^\beta = \Pi_\alpha$ : the metric is the linear relation between kinetic momentum and velocity.

Preamble

import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff

Formal statement

namespace RelPartMech

theorem position_evolution {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 α) (hamiltonian g A e m) x p =
      (1 / m) * ∑ β, ginv g x α β * kineticMomentum A e β x p := by sorry

end RelPartMech

Source

G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 4, eq. (9), first two lines

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

Hamilton's equation for position: mgαβ dsxβ=Παm g_{\alpha\beta}\, d_s x^\beta = \Pi_\alphamgαβ​ds​xβ=Πα​

Hamilton's equation for position: $m g_{\alpha\beta}\, d_s x^\beta = \Pi_\alpha$