Prove2Me

Matrix Euler formulas eηφe^{\eta\varphi} for η2=∓1\eta^2 = \mp 1

Proved
UnQuantumMechanics.real_pauli_exp_euler

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

hamiltonian-mechanicslinear-algebramathematical-physics

Let η\eta be a real 2×22\times 2 matrix and φ∈R\varphi\in\mathbb R.

  1. If η2=−1\eta^2 = -\mathbf 1, then exp⁡(φη)=cos⁡φ 1+sin⁡φ η\exp(\varphi\eta) = \cos\varphi\,\mathbf 1 + \sin\varphi\,\eta.
  2. If η2=1\eta^2 = \mathbf 1, then exp⁡(φη)=cosh⁡φ 1+sinh⁡φ η\exp(\varphi\eta) = \cosh\varphi\,\mathbf 1 + \sinh\varphi\,\eta.

In the paper the first case yields rotations and the second boosts, generated by the real Pauli matrices η0,…,η3\eta_0,\dots,\eta_3 of Eq. (61).

Formalization Note The statement is made for every real 2×22\times 2 matrix with the given square, which covers each real Pauli matrix of Eq. (61); exp⁡\exp is the matrix exponential.

Preamble
import Mathlib
import Definitions.Def_UnQM_phase_space

open Matrix
Formal statement
namespace UnQuantumMechanics

theorem real_pauli_exp_euler (η : Matrix (Fin 2) (Fin 2) ℝ) (φ : ℝ) :
    (η * η = -1 → NormedSpace.exp (φ • η) = Real.cos φ • (1 : Matrix (Fin 2) (Fin 2) ℝ) + Real.sin φ • η) ∧
    (η * η = 1 → NormedSpace.exp (φ • η) = Real.cosh φ • (1 : Matrix (Fin 2) (Fin 2) ℝ) + Real.sinh φ • η) := 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.D, p. 20, Eq. (66)
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 real 2×22\times2 matrix η\eta and every real φ\varphi, both implications hold: (i) if ηη=−1\eta\eta = -\mathbf 1 then exp⁡(φη)=cos⁡(φ) 1+sin⁡(φ) η\exp(\varphi\eta) = \cos(\varphi)\,\mathbf 1 + \sin(\varphi)\,\eta; (ii) if ηη=1\eta\eta = \mathbf 1 then exp⁡(φη)=cosh⁡(φ) 1+sinh⁡(φ) η\exp(\varphi\eta) = \cosh(\varphi)\,\mathbf 1 + \sinh(\varphi)\,\eta. Here 1\mathbf 1 is the 2×22\times2 identity and exp⁡\exp the power-series matrix exponential. No other property of η\eta (e.g. being one of a specific list of matrices) 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