Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

The canonical Hamiltonian bracket satisfies the Lie algebra laws

Proved
SymplecticFreeModules.canonicalHamiltonianLieBracket

by Wenqian · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

lie-algebras

For every natural number lll, the bilinear extension of the canonical Hamiltonian basis brackets is a complex Lie bracket. Write h0=0h_0=0h0​=0, let nonzero exponent vectors index the remaining hrh_rhr​, and let did_idi​ denote the degree generators. The brackets are

[hr,hs]=⟨r~,s⟩hr+s,[di,hr]=rihr,[di,dj]=0,[h_r,h_s]=\langle\widetilde r,s\rangle h_{r+s},\qquad [d_i,h_r]=r_i h_r,\qquad [d_i,d_j]=0,[hr​,hs​]=⟨r,s⟩hr+s​,[di​,hr​]=ri​hr​,[di​,dj​]=0,

with [hr,di]=−rihr[h_r,d_i]=-r_i h_r[hr​,di​]=−ri​hr​. Here r~\widetilde rr exchanges the two coordinate blocks and negates the second block. The assertion is precisely additivity and complex homogeneity in both variables, alternation, and the cyclic Jacobi identity for the explicitly defined bracket on the finitely supported vector-space carrier. It supplies the bracket-law clause needed by the canonical Hamiltonian application.

Preamble
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces

open scoped TensorProduct
Formal statement
namespace SymplecticFreeModules

theorem canonicalHamiltonianLieBracket (l : ℕ) :
    IsCanonicalHamiltonianLieBracket l := by sorry

end SymplecticFreeModules
Source
Canonical basis bracket and IsCanonicalHamiltonianLieBracket in https://prove2.me/theorems/11f584f1-dcb8-4e17-8e63-99c778b2b7c0 ; Chen--Tan, Journal of Algebra 697 (2026), Section 5, Theorem 5.2, https://doi.org/10.1016/j.jalgebra.2026.02.022 .

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me