p. 16 — exact one-forms are Hamiltonian

Proved

CatSymplectic.Hemistrict.exact_forms

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

hamiltonian-one-formsmultisymplectic-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

For every smooth real function $f$ on a 2-plectic space, its exact form is Hamiltonian and

v_{df}=0.

This gives the differential from smooth functions to Hamiltonian one-forms in the two-term complex.

Formalization Note The space is a finite-dimensional real normed space. The differential $df$ is ContWeatherall.grad, and the three-form $\omega$ is named Ω in Lean.

Preamble

import Mathlib
import Definitions.Def_CatSymplectic_Hemistrict_Basic

Formal statement

namespace CatSymplectic.Hemistrict

theorem exact_forms {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (Ω : Form E 3) (hΩ : IsNPlectic 2 Ω)
    (f : E → ℝ) (hf : ContDiff ℝ smooth f) :
    ContWeatherall.grad f ∈ hamSubmodule Ω ∧
      hamVF Ω (ContWeatherall.grad f) = 0 := by sorry

end CatSymplectic.Hemistrict

Source

Baez, Hoffnung, Rogers, Categorified Symplectic Geometry and the Classical String, arXiv:0808.0246v1, p. 16, paragraph after the two-term complex

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