Prove2Me

Lax pair: Tr⁡(Sk)\operatorname{Tr}(S^k) is a constant of motion

Proved
UnQuantumMechanics.lax_trace_power_conserved

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let τ↦H(τ)\tau\mapsto H(\tau) and τ↦S(τ)\tau\mapsto S(\tau) be real m×mm\times m matrix-valued functions such that SS is differentiable at every time and obeys the Lax equation

S˙(τ)=H(τ)S(τ)−S(τ)H(τ)for all τ.\dot S(\tau) = H(\tau)S(\tau) - S(\tau)H(\tau)\qquad\text{for all } \tau .

Then for every k∈Nk\in\mathbb N the trace of SkS^k is a constant of motion:

Tr⁡(S(τ)k)=Tr⁡(S(0)k)for all τ.\operatorname{Tr}\big(S(\tau)^k\big) = \operatorname{Tr}\big(S(0)^k\big)\qquad\text{for all }\tau .

Formalization Note HH is allowed to depend on time (the paper remarks the statement holds beyond the linear case); derivatives are entrywise; mm is an arbitrary finite index set, and k=0k = 0 is included.

Preamble
import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix
Formal statement
namespace UnQuantumMechanics

theorem lax_trace_power_conserved {m : Type} [Fintype m] [DecidableEq m]
    (H S : ℝ → Matrix m m ℝ)
    (hS : ∀ τ i j, HasDerivAt (fun t => S t i j) ((H τ * S τ - S τ * H τ) i j) τ)
    (k : ℕ) (τ : ℝ) :
    (S τ ^ k).trace = (S 0 ^ k).trace := 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. 16–17, Eq. (47)
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 finite index type mm (with decidable equality), all functions H,S:R→Rm×mH, S:\mathbb R\to\mathbb R^{m\times m} such that for every τ\tau and all indices i,ji,j the function t↦S(t)ijt\mapsto S(t)_{ij} is differentiable at τ\tau with derivative (H(τ)S(τ)−S(τ)H(τ))ij\big(H(\tau)S(\tau)-S(\tau)H(\tau)\big)_{ij}, every natural number kk (including 00) and every real τ\tau: Tr⁡(S(τ)k)=Tr⁡(S(0)k)\operatorname{Tr}\big(S(\tau)^k\big) = \operatorname{Tr}\big(S(0)^k\big). No regularity of HH (continuity, boundedness) 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