Prove2Me

Transpose of a Hamiltonian matrix: HT=γ0Hγ0H^T = \gamma_0 H \gamma_0

Proved
UnQuantumMechanics.hamiltonian_transpose

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let H=γ0AH = \gamma_0 A be a Hamiltonian 2n×2n2n\times 2n matrix, AA symmetric. Then

HT=γ0Hγ0.H^T = \gamma_0 H \gamma_0 .

This identity is the algebraic characterization of Hamiltonian matrices used in the derivation of Heisenberg's equation (Eq. 42).

Preamble
import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix
Formal statement
namespace UnQuantumMechanics

theorem hamiltonian_transpose (n : ℕ) (H : Matrix (PhaseIdx n) (PhaseIdx n) ℝ) (hH : IsHamiltonianMatrix n H) :
    Hᵀ = gamma0 n * H * gamma0 n := 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. 14, Eq. (36)
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 nn and every real 2n×2n2n\times 2n matrix HH for which there exists a symmetric real matrix AA with H=γ0AH = \gamma_0 A (where γ0=1n⊗η0\gamma_0 = \mathbf 1_n\otimes\eta_0), the transpose satisfies HT=γ0 H γ0H^T = \gamma_0\, H\, \gamma_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