Prove2Me

The flow ψ˙=J∇H\dot\psi = J\nabla H with JJ skew-symmetric conserves HH

Proved
UnQuantumMechanics.skew_flow_conserves_hamiltonian

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let JJ be a real ν×ν\nu\times\nu skew-symmetric matrix and let H:Rν→RH:\mathbb R^\nu\to\mathbb R be differentiable (with no explicit time dependence). Let ψ:R→Rν\psi:\mathbb R\to\mathbb R^\nu be a differentiable curve satisfying

ψ˙(τ)=J ∇ψH(ψ(τ))for all τ.\dot\psi(\tau) = J\,\nabla_\psi H(\psi(\tau)) \quad\text{for all } \tau .

Then HH is a constant of motion:

ddτH(ψ(τ))=0for all τ.\frac{d}{d\tau} H(\psi(\tau)) = 0 \quad \text{for all }\tau.

This is the paper's derivation of the general form of an equation of motion that conserves a given quantity HH.

Formalization Note The kk-th component of ∇ψH(x)\nabla_\psi H(x) is written as the derivative of HH at xx applied to the kk-th standard basis vector.

Preamble
import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix
Formal statement
namespace UnQuantumMechanics

theorem skew_flow_conserves_hamiltonian {ν : ℕ} (J : Matrix (Fin ν) (Fin ν) ℝ) (hJ : Jᵀ = -J)
    (Hf : (Fin ν → ℝ) → ℝ) (hHf : Differentiable ℝ Hf) (ψ : ℝ → Fin ν → ℝ)
    (hψ : ∀ τ, HasDerivAt ψ (J *ᵥ (fun k => fderiv ℝ Hf (ψ τ) (Pi.single k 1))) τ) :
    ∀ τ, HasDerivAt (fun t => Hf (ψ t)) 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. IV, p. 13, Eqs. (26)–(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, every real ν×ν\nu\times\nu matrix JJ with JT=−JJ^T = -J, every function H:Rν→RH:\mathbb R^\nu\to\mathbb R that is (Fréchet) differentiable at every point, and every curve ψ:R→Rν\psi:\mathbb R\to\mathbb R^\nu such that for every τ∈R\tau\in\mathbb R the curve ψ\psi is differentiable at τ\tau with derivative

ψ˙(τ)=J g(ψ(τ)),g(x)k=DH(x)[ek]  (k=1,…,ν),\dot\psi(\tau) = J\,g(\psi(\tau)),\qquad g(x)_k = DH(x)[e_k]\ \ (k = 1,\dots,\nu),

where DH(x)DH(x) is the derivative of HH at xx and eke_k is the kk-th standard basis vector: for every τ\tau, the real function t↦H(ψ(t))t\mapsto H(\psi(t)) has derivative 00 at τ\tau. Rν\mathbb R^\nu carries its standard (sup-norm) topology; for ν=0\nu=0 the statement is trivial.

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