Prove2Me

Transpose of a skew-Hamiltonian matrix: CT=−γ0Cγ0C^T = -\gamma_0 C \gamma_0

Proved
UnQuantumMechanics.skew_hamiltonian_transpose

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let C=γ0BC = \gamma_0 B be a skew-Hamiltonian 2n×2n2n\times 2n matrix, BT=−BB^T = -B. Then

CT=−γ0Cγ0.C^T = -\gamma_0 C\gamma_0 .

Together with Eq. (36) this distinguishes the two classes of matrices that make up the phase-space algebra.

Preamble
import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix
Formal statement
namespace UnQuantumMechanics

theorem skew_hamiltonian_transpose (n : ℕ) (C : Matrix (PhaseIdx n) (PhaseIdx n) ℝ) (hC : IsSkewHamiltonianMatrix n C) :
    Cᵀ = -(gamma0 n * C * 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. VI.B, p. 17, Eqs. (53)–(54)
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 CC for which there exists a real matrix BB with BT=−BB^T = -B and C=γ0BC = \gamma_0 B (γ0=1n⊗η0\gamma_0 = \mathbf 1_n\otimes\eta_0), the transpose satisfies CT=−(γ0 C γ0)C^T = -(\gamma_0\, C\, \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