Identities of the symplectic unit matrix $\gamma_0$

Proved

UnQuantumMechanics.gamma0_identities

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let $\gamma_0 = \mathbf 1_n\otimes\eta_0$ be the symplectic unit matrix for $n$ degrees of freedom. Then

$\gamma_0^T = -\gamma_0$ ,
$\gamma_0^2 = -\mathbf 1$ ,
$\gamma_0^T\gamma_0 = \mathbf 1$ .

These identities are used throughout the paper to move $\gamma_0$ across products of Hamiltonian matrices.

Preamble

import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix

Formal statement

namespace UnQuantumMechanics

theorem gamma0_identities (n : ℕ) :
    (gamma0 n)ᵀ = -gamma0 n ∧ gamma0 n * gamma0 n = -1 ∧ (gamma0 n)ᵀ * gamma0 n = 1 := 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. IV, p. 14, Eq. (33) and the text after it; text before Eq. (37); Sec. V, p. 15, text before Eq. (42)

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$ (including $n=0$ ), with $\gamma_0$ the $2n\times 2n$ real matrix $\mathbf 1_n\otimes\eta_0$ , $\eta_0 = \begin{pmatrix}0&1\\-1&0\end{pmatrix}$ , all three of the following hold:

\gamma_0^T = -\gamma_0,\qquad \gamma_0\gamma_0 = -\mathbf 1,\qquad \gamma_0^T\gamma_0 = \mathbf 1,

where $\mathbf 1$ is the $2n\times 2n$ identity matrix.

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

Identities of the symplectic unit matrix γ0\gamma_0γ0​

Identities of the symplectic unit matrix $\gamma_0$