Second moments obey Heisenberg's equation $\dot S = [H, S]$

Proved

UnQuantumMechanics.second_moment_heisenberg_equation

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let $H$ be a Hamiltonian $2n\times 2n$ matrix and let $\tau\mapsto\Sigma(\tau)$ be a matrix-valued function that, at the time $\tau$ , is differentiable and satisfies the second-moment equation (40)

\dot\Sigma(\tau) = H\Sigma(\tau) + \Sigma(\tau)H^T .

Then the autocorrelation matrix $S(t) = \Sigma(t)\gamma_0^T$ is differentiable at $\tau$ and satisfies Heisenberg's equation (42)

\dot S(\tau) = H S(\tau) - S(\tau) H = [H, S(\tau)] .

Formalization Note Derivatives of matrix-valued functions are taken entrywise. $\Sigma$ is any matrix-valued function obeying Eq. (40); its interpretation as an ensemble average $\langle\psi\psi^T\rangle$ is not part of the statement.

Preamble

import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix

Formal statement

namespace UnQuantumMechanics

theorem second_moment_heisenberg_equation (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) τ) :
    ∀ i j, HasDerivAt (fun t => autocorr n (Sig t) i j)
      ((H * autocorr n (Sig τ) - autocorr n (Sig τ) * H) i j) τ := 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, p. 15, Eqs. (40)–(42)

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 $A$ with $H=\gamma_0A$ , every function $\Sigma:\mathbb R\to\mathbb R^{2n\times 2n}$ and every $\tau\in\mathbb R$ : if for all indices $i,j$ the scalar function $t\mapsto\Sigma(t)_{ij}$ is differentiable at $\tau$ with derivative $\big(H\Sigma(\tau)+\Sigma(\tau)H^T\big)_{ij}$ , then for all indices $i,j$ the scalar function $t\mapsto\big(\Sigma(t)\gamma_0^T\big)_{ij}$ is differentiable at $\tau$ with derivative $\big(HS-SH\big)_{ij}$ , where $S = \Sigma(\tau)\gamma_0^T$ . The hypothesis is only about the single time $\tau$ ; no symmetry of $\Sigma$ is assumed.

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

Second moments obey Heisenberg's equation S˙=[H,S]\dot S = [H, S]S˙=[H,S]

Second moments obey Heisenberg's equation $\dot S = [H, S]$