Odd powers of a Hamiltonian matrix are traceless

Proved

UnQuantumMechanics.hamiltonian_trace_odd_pow

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let $S = \gamma_0 A$ be a Hamiltonian $2n\times 2n$ matrix ( $A$ symmetric). Then every odd power of $S$ is traceless:

\operatorname{Tr}\big(S^{2k+1}\big) = 0\qquad (k = 0, 1, 2,\dots).

Consequently only the even powers in the Lax invariants (47) carry information.

Formalization Note The source phrases the hypothesis with $A$ symmetric positive definite; the statement here only assumes $A$ symmetric (the paper's definition of a Hamiltonian matrix). This is needed because the autocorrelation matrix $S = \Sigma\gamma_0^T$ equals $\gamma_0 A$ with $A = -\gamma_0^T\Sigma\gamma_0$ , which is negative (not positive) definite when $\Sigma$ is positive definite.

Preamble

import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix

Formal statement

namespace UnQuantumMechanics

theorem hamiltonian_trace_odd_pow (n : ℕ) (S : Matrix (PhaseIdx n) (PhaseIdx n) ℝ) (hS : IsHamiltonianMatrix n S) (k : ℕ) :
    (S ^ (2 * k + 1)).trace = 0 := 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, p. 17, Eq. (48)

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$ , every real $2n\times 2n$ matrix $S$ for which there exists a symmetric real matrix $A$ with $S = \gamma_0 A$ (no definiteness assumed), and every natural number $k$ (including $0$ ): $\operatorname{Tr}\big(S^{2k+1}\big) = 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