Phase-space setting: $\gamma_0$ , Hamiltonian, skew-Hamiltonian and symplectic matrices

Definition

UnQM_phase_space

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

hamiltonian-mechanicslinear-algebramathematical-physics

This definition file fixes the linear-algebraic setting of Sections IV–VI of Baumgarten's paper. Throughout, $n \ge 0$ is the number of degrees of freedom and phase-space vectors are $\psi = (q_1, p_1, q_2, p_2, \dots, q_n, p_n)^T \in \mathbb R^{2n}$ .

The $2\times 2$ symplectic unit matrix is

\eta_0 = \begin{pmatrix} 0 & 1 \\ -1 & 0 \end{pmatrix}.

The symplectic unit matrix (SUM) for $n$ degrees of freedom is the Kronecker product $\gamma_0 = \mathbf 1_n \otimes \eta_0$ , a real $2n \times 2n$ matrix.
A real $2n\times 2n$ matrix $M$ is Hamiltonian if $M = \gamma_0 A$ for some symmetric matrix $A$ .
A real $2n\times 2n$ matrix $C$ is skew-Hamiltonian if $C = \gamma_0 B$ for some skew-symmetric matrix $B$ ( $B^T = -B$ ).
A real $2n\times 2n$ matrix $M$ is symplectic if $M\gamma_0 M^T = \gamma_0$ .
For a matrix of second moments $\Sigma$ , the autocorrelation matrix is $S = \Sigma\,\gamma_0^T$ .

These notions are shared by every statement of the mission.

Formalization Note Indices of $2n\times 2n$ matrices are pairs $(i, b)$ with $i \in \{0,\dots,n-1\}$ and $b \in \{0, 1\}$ ( $b = 0$ for $q_i$ , $b=1$ for $p_i$ ), so $\gamma_0$ is literally the Kronecker product $\mathbf 1_n \otimes \eta_0$ . For $n = 0$ all matrices are empty.

Definition code

import Mathlib

namespace UnQuantumMechanics

open Matrix

/-- Phase-space coordinate indices for `n` degrees of freedom: the pair `(i, 0)` is the
coordinate `qᵢ` and `(i, 1)` is the conjugate momentum `pᵢ`, so a phase-space vector is
`ψ = (q₁, p₁, q₂, p₂, …, qₙ, pₙ)ᵀ` (Baumgarten, Sec. IV, after Eq. 33). -/
abbrev PhaseIdx (n : ℕ) : Type := Fin n × Fin 2

/-- The `2 × 2` symplectic unit matrix `η₀ = [[0, 1], [-1, 0]]` (Eq. 32). -/
def eta0 : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; -1, 0]

/-- The symplectic unit matrix (SUM) `γ₀ = 1ₙ ⊗ η₀` for `n` degrees of freedom (Eq. 33),
built as a Kronecker product. -/
def gamma0 (n : ℕ) : Matrix (PhaseIdx n) (PhaseIdx n) ℝ :=
  Matrix.kroneckerMap (· * ·) (1 : Matrix (Fin n) (Fin n) ℝ) eta0

/-- A real `2n × 2n` matrix `M` is *Hamiltonian* if it can be written `M = γ₀ A` with `A`
symmetric (Sec. IV, text before Eq. 36). -/
def IsHamiltonianMatrix (n : ℕ) (M : Matrix (PhaseIdx n) (PhaseIdx n) ℝ) : Prop :=
  ∃ A : Matrix (PhaseIdx n) (PhaseIdx n) ℝ, A.IsSymm ∧ M = gamma0 n * A

/-- A real `2n × 2n` matrix `C` is *skew-Hamiltonian* if it can be written `C = γ₀ B` with
`B` skew-symmetric, `Bᵀ = -B` (Eq. 53). -/
def IsSkewHamiltonianMatrix (n : ℕ) (C : Matrix (PhaseIdx n) (PhaseIdx n) ℝ) : Prop :=
  ∃ B : Matrix (PhaseIdx n) (PhaseIdx n) ℝ, Bᵀ = -B ∧ C = gamma0 n * B

/-- A real `2n × 2n` matrix `M` is *symplectic* if `M γ₀ Mᵀ = γ₀` (Eq. 50). -/
def IsSymplecticMatrix (n : ℕ) (M : Matrix (PhaseIdx n) (PhaseIdx n) ℝ) : Prop :=
  M * gamma0 n * Mᵀ = gamma0 n

/-- The "autocorrelation matrix" `S = Σ γ₀ᵀ` attached to a matrix of second moments `Σ`
(Sec. V, text before Eq. 42). -/
def autocorr (n : ℕ) (Sig : Matrix (PhaseIdx n) (PhaseIdx n) ℝ) :
    Matrix (PhaseIdx n) (PhaseIdx n) ℝ :=
  Sig * (gamma0 n)ᵀ

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 pp. 13–14 (Eqs. 32, 33, text before Eq. 36), Sec. V p. 15 (text before Eq. 42), Sec. VI p. 17 (Eqs. 50, 53)

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.

The file introduces, inside the namespace UnQuantumMechanics, the following objects over the real numbers, for a natural number $n$ (including $n = 0$ ).

The index type for $n$ degrees of freedom is the set of pairs $(i, b)$ with $i \in \{0, \dots, n-1\}$ and $b \in \{0, 1\}$ ; it has $2n$ elements, and all matrices below are indexed by it.
$\eta_0$ is the real $2 \times 2$ matrix with rows $(0, 1)$ and $(-1, 0)$ .
$\gamma_0$ (for a given $n$ ) is the Kronecker product of the $n\times n$ identity with $\eta_0$ : its $((i,b),(j,c))$ entry is $\delta_{ij}\,(\eta_0)_{bc}$ .
A matrix $M$ is called Hamiltonian iff there exists a symmetric matrix $A$ ( $A^T = A$ ) with $M = \gamma_0 A$ .
A matrix $C$ is called skew-Hamiltonian iff there exists $B$ with $B^T = -B$ and $C = \gamma_0 B$ .
A matrix $M$ is called symplectic iff $M\,\gamma_0\,M^T = \gamma_0$ .
For any matrix $\Sigma$ , the matrix $\operatorname{autocorr}(\Sigma)$ is $\Sigma\,\gamma_0^T$ .

No positivity, invertibility or symmetry is required of $A$ beyond what is stated; in particular $A$ need not be positive definite. When $n = 0$ all these matrices are the empty matrix and every predicate is trivially satisfied.

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

Phase-space setting: γ0\gamma_0γ0​, Hamiltonian, skew-Hamiltonian and symplectic matrices

Phase-space setting: $\gamma_0$ , Hamiltonian, skew-Hamiltonian and symplectic matrices