Eigenvalues of a real skew-symmetric matrix come in pairs ±λ

Proved

UnQuantumMechanics.skew_symm_eigenvalue_neg

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let $J$ be a real $\nu \times \nu$ skew-symmetric matrix, $J^T = -J$ . Regard $J$ as a complex matrix. If $\mu \in \mathbb C$ is an eigenvalue of $J$ , then so is $-\mu$ :

\mu \in \operatorname{spec}_{\mathbb C}(J) \implies -\mu \in \operatorname{spec}_{\mathbb C}(J).

The paper uses this pairing to argue that a skew-symmetric "structure matrix" of odd size must be singular, which forces an even number of dynamical variables.

Formalization Note Eigenvalues are taken over $\mathbb C$ for the complexified matrix, since a real skew-symmetric matrix generally has no real eigenvalues other than $0$ .

Preamble

import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix

Formal statement

namespace UnQuantumMechanics

theorem skew_symm_eigenvalue_neg {ν : ℕ} (J : Matrix (Fin ν) (Fin ν) ℝ) (hJ : Jᵀ = -J)
    (μ : ℂ) (hμ : Module.End.HasEigenvalue (Matrix.toLin' (J.map (algebraMap ℝ ℂ))) μ) :
    Module.End.HasEigenvalue (Matrix.toLin' (J.map (algebraMap ℝ ℂ))) (-μ) := 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. 13, paragraph after Eq. (28)

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 $\nu$ (including $\nu = 0$ ), every real $\nu\times\nu$ matrix $J$ with $J^T = -J$ , and every complex number $\mu$ : if $\mu$ is an eigenvalue of the complex matrix obtained from $J$ by viewing each real entry as a complex number (i.e. there is a nonzero vector $v \in \mathbb C^\nu$ with $Jv = \mu v$ ), then $-\mu$ is also an eigenvalue of that complex matrix. For $\nu = 0$ there are no eigenvalues, so the statement holds vacuously.

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