Prove2Me

Proposition 3.6(3), p. 12 — Jacobi identity of the hemi-bracket

Proved
CatSymplectic.Hemistrict.proposition_3_6_3

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

hemi-bracketjacobi-identitymultisymplectic-geometryp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

For Hamiltonian one-forms F,G,HF,G,H, the hemi-bracket satisfies

{F,{G,H}h}h={{F,G}h,H}h+{G,{F,H}h}h.\{F,\{G,H\}_h\}_h =\{\{F,G\}_h,H\}_h+\{G,\{F,H\}_h\}_h.

This is the degree-zero Jacobi identity used for the zero Jacobiator.

Formalization Note This is the paper's n=2n=2 case on a finite-dimensional real normed space. The paper's ω\omega is Ω in Lean.

Preamble
import Mathlib
import Definitions.Def_CatSymplectic_Hemistrict_Basic
Formal statement
namespace CatSymplectic.Hemistrict

theorem proposition_3_6_3 {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (Ω : Form E 3) (hΩ : IsNPlectic 2 Ω)
    (F G H : hamSubmodule Ω) :
    hemi Ω F (hemi Ω G H) =
      hemi Ω (hemi Ω F G) H + hemi Ω G (hemi Ω F H) := by sorry

end CatSymplectic.Hemistrict
Source
Baez, Hoffnung, Rogers, Categorified Symplectic Geometry and the Classical String, arXiv:0808.0246v1, p. 12, Proposition 3.6 part 3, equation (8)
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