Poisson bracket of a position function with kinetic momentum

Proved

RelPartMech.poisson_position_fn_kinetic_momentum

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

mathematical-physicsrelativity

For any smooth function $f(x^\alpha)$ of position only, and kinetic momentum $\Pi_\beta=p_\beta-eA_\beta(x)$ ,

\{f(x^\alpha),\Pi_\beta\} = \partial_\beta f .

In particular $\{x^\alpha,\Pi_\beta\}=\delta^\alpha_\beta$ : kinetic momentum still generates translations of the position variables.

Preamble

import Mathlib
import Definitions.Def_RelPartMech_coordinates

open scoped ContDiff

Formal statement

namespace RelPartMech

theorem poisson_position_fn_kinetic_momentum {n : ℕ} (A : CovectorField n) (e : ℝ)
    (f : Coord n → ℝ) (hf : ContDiff ℝ ∞ f) (β : Fin n) (x p : Coord n) :
    poisson (fun y _ => f y) (kineticMomentum A e β) x p = pd β f x := by sorry

end RelPartMech

Source

G. Carcassi, C. A. Aidala, "Relativity and Particle Mechanics" (note, uploaded PDF), p. 3, eq. (8), third line

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