(Anti-)commutator table of Hamiltonian and skew-Hamiltonian matrices

Proved

UnQuantumMechanics.hamiltonian_skew_hamiltonian_algebra

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let $S_1, S_2$ be Hamiltonian and $C_1, C_2$ skew-Hamiltonian $2n\times 2n$ matrices, and let $k \in \mathbb N$ . Then

$S_1S_2 - S_2S_1$ , $\ C_1C_2 - C_2C_1$ , $\ C_1S_1 + S_1C_1$ and $S_1^{2k+1}$ are Hamiltonian;
$S_1S_2 + S_2S_1$ , $\ C_1C_2 + C_2C_1$ , $\ C_1S_1 - S_1C_1$ , $S_1^{2k}$ and $C_1^{k}$ are skew-Hamiltonian.

This is the "phase-space algebra" from which the paper later builds Clifford algebras.

Formalization Note In Eq. (57) the exponent letter $n$ is a generic natural number, not the number of degrees of freedom; it is written $k$ here. The case $k = 0$ is included, so in particular the identity matrix is skew-Hamiltonian.

Preamble

import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix

Formal statement

namespace UnQuantumMechanics

theorem hamiltonian_skew_hamiltonian_algebra (n : ℕ) (S₁ S₂ C₁ C₂ : Matrix (PhaseIdx n) (PhaseIdx n) ℝ)
    (hS₁ : IsHamiltonianMatrix n S₁) (hS₂ : IsHamiltonianMatrix n S₂)
    (hC₁ : IsSkewHamiltonianMatrix n C₁) (hC₂ : IsSkewHamiltonianMatrix n C₂) (k : ℕ) :
    (IsHamiltonianMatrix n (S₁ * S₂ - S₂ * S₁) ∧
      IsHamiltonianMatrix n (C₁ * C₂ - C₂ * C₁) ∧
      IsHamiltonianMatrix n (C₁ * S₁ + S₁ * C₁) ∧
      IsHamiltonianMatrix n (S₁ ^ (2 * k + 1))) ∧
    (IsSkewHamiltonianMatrix n (S₁ * S₂ + S₂ * S₁) ∧
      IsSkewHamiltonianMatrix n (C₁ * C₂ + C₂ * C₁) ∧
      IsSkewHamiltonianMatrix n (C₁ * S₁ - S₁ * C₁) ∧
      IsSkewHamiltonianMatrix n (S₁ ^ (2 * k)) ∧
      IsSkewHamiltonianMatrix n (C₁ ^ k)) := by sorry

end UnQuantumMechanics

Source

C. Baumgarten, How to (Un-) Quantum Mechanics, arXiv:1810.06981v2 [physics.gen-ph] (v2 dated June 10, 2025), https://arxiv.org/abs/1810.06981, Sec. VI.B, pp. 17–18, Eq. (57)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent that drafted the statements; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, at the explicit direction of the proposal owner. The author knew the intended meaning and the source text while writing it, so it must not be mistaken for a blind, independent audit. An independent blind read-back is still recommended before submission.

For every natural number $n$ , all real $2n\times2n$ matrices $S_1,S_2,C_1,C_2$ such that $S_1$ and $S_2$ are each of the form $\gamma_0A$ with $A$ symmetric and $C_1$ and $C_2$ are each of the form $\gamma_0B$ with $B^T=-B$ , and every natural number $k$ (including $0$ ), both of the following blocks hold:

each of $S_1S_2-S_2S_1$ , $C_1C_2-C_2C_1$ , $C_1S_1+S_1C_1$ , $S_1^{2k+1}$ is of the form $\gamma_0A'$ with $A'$ symmetric;
each of $S_1S_2+S_2S_1$ , $C_1C_2+C_2C_1$ , $C_1S_1-S_1C_1$ , $S_1^{2k}$ , $C_1^{k}$ is of the form $\gamma_0B'$ with $B'^T=-B'$ .

Only the mixed products of $C_1$ with $S_1$ (not $C_2$ or $S_2$ ) and only powers of $S_1$ and $C_1$ appear.

Human review

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

View graph