p. 11 — uniqueness of the Hamiltonian vector field

Proved

CatSymplectic.Hemistrict.unique_hamVF

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

hamiltonian-vector-fieldsmultisymplectic-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\omega$ be 2-plectic and $F$ a one-form. If vector fields $v,w$ both satisfy the Hamiltonian equation for $F$ , then

v=w=v_F.

Thus every Hamiltonian one-form has a unique associated vector field.

Formalization Note The manifold is restricted to a finite-dimensional real normed space, and the witnesses are smooth. The paper's $\omega$ is named Ω in Lean.

Preamble

import Mathlib
import Definitions.Def_CatSymplectic_Hemistrict_Basic

Formal statement

namespace CatSymplectic.Hemistrict

theorem unique_hamVF {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (Ω : Form E 3) (hΩ : IsNPlectic 2 Ω)
    (F : Form E 1) (v w : E → E)
    (hv : IsHamVF Ω F v) (hw : IsHamVF Ω F w) :
    v = w ∧ hamVF Ω F = v := by sorry

end CatSymplectic.Hemistrict

Source

Baez, Hoffnung, Rogers, Categorified Symplectic Geometry and the Classical String, arXiv:0808.0246v1, p. 11, paragraph after Definition 3.1

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph