Skew-Hamiltonian $2n\times 2n$ matrices form a space of dimension $n(2n-1)$

Proved

UnQuantumMechanics.skew_hamiltonian_matrices_finrank

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

hamiltonian-mechanicslinear-algebramathematical-physics

The real $2n\times 2n$ skew-Hamiltonian matrices span a real vector space of dimension

\nu_c = n(2n-1).

Formalization Note As for Eq. (55), the count is the dimension of the real linear span of the set of skew-Hamiltonian matrices. The factor $2n-1$ is computed in natural numbers; for $n = 0$ both sides are $0$ , so truncated subtraction plays no role.

Preamble

import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix

Formal statement

namespace UnQuantumMechanics

theorem skew_hamiltonian_matrices_finrank (n : ℕ) :
    Module.finrank ℝ (Submodule.span ℝ {M | IsSkewHamiltonianMatrix n M}) = n * (2 * 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. VI.B, p. 17, Eq. (56)

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$ : the real linear span, inside the real $2n\times2n$ matrices, of the set of all matrices $C$ for which there is $B$ with $B^T=-B$ and $C=\gamma_0B$ , has dimension exactly $n\cdot(2n-1)$ , where $2n-1$ is natural-number subtraction (equal to $0$ when $n = 0$ , in which case the claimed dimension is $0$ ).

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

Skew-Hamiltonian 2n×2n2n\times 2n2n×2n matrices form a space of dimension n(2n−1)n(2n-1)n(2n−1)

Skew-Hamiltonian $2n\times 2n$ matrices form a space of dimension $n(2n-1)$