Spectral invariants of the second-moment matrix under linear Hamiltonian motion

Proved

UnQuantumMechanics.second_moment_spectrum_conserved

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let $H = \gamma_0 A$ be a Hamiltonian $2n\times 2n$ matrix ( $A$ symmetric), the driving matrix of linear Hamiltonian motion $\dot\psi = H\psi$ . Let $\tau\mapsto\Sigma(\tau)$ be a matrix of second moments: a real $2n\times 2n$ matrix-valued function, symmetric at every time, that is differentiable and obeys the second-moment equation (40)

\dot\Sigma = H\Sigma + \Sigma H^T .

Let $S(\tau) = \Sigma(\tau)\gamma_0^T$ be the autocorrelation matrix. Then for every time $\tau$ :

the eigenvalues of $S$ are constants of motion, in the strong form that the characteristic polynomial is conserved:

\chi_{S(\tau)}(x) = \chi_{S(0)}(x);

all odd powers of $S(\tau)$ are traceless: $\operatorname{Tr}\big(S(\tau)^{2k+1}\big) = 0$ for every $k\in\mathbb N$ .

This is the paper's conclusion (p. 17) that "the result of Hamiltonian evolution in time ... is a symplectic similarity transformation. And since similarity transformations do not change eigenvalues, the eigenvalues are COMs", together with Eq. (48).

Formalization Note Derivatives are entrywise. $\Sigma$ is any symmetric matrix-valued solution of Eq. (40); its interpretation as an ensemble average $\langle\psi\psi^T\rangle$ (and positive semidefiniteness, $\Sigma = KK^T$ ) is not assumed, because it is not needed. Conservation of the characteristic polynomial (with multiplicities) implies conservation of the whole spectrum and of all $\operatorname{Tr}(S^k)$ .

Preamble

import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix

Formal statement

namespace UnQuantumMechanics

theorem second_moment_spectrum_conserved (n : ℕ) (H : Matrix (PhaseIdx n) (PhaseIdx n) ℝ) (hH : IsHamiltonianMatrix n H)
    (Sig : ℝ → Matrix (PhaseIdx n) (PhaseIdx n) ℝ)
    (hSig : ∀ τ i j, HasDerivAt (fun t => Sig t i j) ((H * Sig τ + Sig τ * Hᵀ) i j) τ)
    (hSym : ∀ t, (Sig t).IsSymm) (τ : ℝ) :
    (autocorr n (Sig τ)).charpoly = (autocorr n (Sig 0)).charpoly ∧
      ∀ k : ℕ, (autocorr n (Sig τ) ^ (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. V–VI, pp. 15–17: Eqs. (40)–(42), (47), (48), (51) and the sentence after Eq. (51)

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\times2n$ matrix $H$ for which there is a symmetric real $A$ with $H=\gamma_0A$ ( $\gamma_0=\mathbf 1_n\otimes\eta_0$ ), every function $\Sigma:\mathbb R\to\mathbb R^{2n\times2n}$ such that

for every $t$ and all indices $i,j$ , the function $s\mapsto\Sigma(s)_{ij}$ is differentiable at $t$ with derivative $\big(H\Sigma(t)+\Sigma(t)H^T\big)_{ij}$ , and
$\Sigma(t)$ is symmetric for every $t$ ,

and every real $\tau$ , both of the following hold, where $S(t) = \Sigma(t)\gamma_0^T$ :

the characteristic polynomial of $S(\tau)$ (a real polynomial) equals the characteristic polynomial of $S(0)$ ;
for every natural number $k$ (including $0$ ), $\operatorname{Tr}\big(S(\tau)^{2k+1}\big)=0$ .

No positivity of $\Sigma$ or of $A$ is assumed; $H$ is constant in time.

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