Quadratic Gaussian conjugation and all special orthogonal rotations

Open

QAlgorithms.Papers.Independent.Intakethird100.P77.gaussian_rotation

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $c_1,\ldots,c_{2n}$ be Hermitian operators on the full $n$ -qubit Hilbert space with $c_\mu c_\nu+c_\nu c_\mu=2\delta_{\mu\nu}I$ . For a real antisymmetric matrix $h$ , set $H=i\sum_{\mu\ne\nu}h_{\mu\nu}c_\mu c_\nu$ and $U=e^{iH}$ . Then

Uc_\mu U^\dagger=\sum_\nu(e^{4h})_{\mu\nu}c_\nu,\qquad U^\dagger c_\mu U=\sum_\nu(e^{-4h})_{\mu\nu}c_\nu.

Both real coefficient matrices are orthogonal with determinant one, and every matrix in $SO(2n)$ is $e^{4h}$ for such an $h$ and hence is induced by this conjugation. Both ordered off-diagonal terms are included and scalar Hamiltonian terms are omitted. This is the rotation interface underlying the simulation results.

Source correction. The printed displayed theorem puts $e^{4h}$ beside the opposite adjoint action. The statement follows the convention and differential equation in the source proof.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P77

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P77

open QAlgorithms

open QAlgorithms.Complexity (Str)

open QAlgorithms.Papers.Independent.Advance50.P19 (Major CARSystem)

open QAlgorithms.Papers.Independent.Information100.P32 (Op)

open scoped BigOperators Matrix ComplexConjugate

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.9 Theorem 3, corrected using its own proof: exp(4h) describes
U c U†, while exp(-4h) describes U† c U. The literal displayed theorem has the
adjoint sign reversed. Surjectivity is included, including the n=0 case. -/
theorem gaussian_rotation {n : ℕ} (c : CARSystem n) :
    (∀ h : Matrix (Major n) (Major n) ℝ, Skew h →
      IsMajoranaRotation (NormedSpace.exp ((4 : ℝ) • h)) ∧
      IsMajoranaRotation (NormedSpace.exp ((-4 : ℝ) • h)) ∧
      (∀ i, gaussianOperation c.majorana h * c.majorana i * star (gaussianOperation c.majorana h) =
        ∑ j, ((NormedSpace.exp ((4 : ℝ) • h)) i j : ℂ) • c.majorana j) ∧
      (∀ i, star (gaussianOperation c.majorana h) * c.majorana i * gaussianOperation c.majorana h =
        ∑ j, ((NormedSpace.exp ((-4 : ℝ) • h)) i j : ℂ) • c.majorana j)) ∧
    (∀ R : Matrix (Major n) (Major n) ℝ, IsMajoranaRotation R →
      ∃ h : Matrix (Major n) (Major n) ℝ, Skew h ∧
        NormedSpace.exp ((4 : ℝ) • h) = R ∧
        ∀ i, gaussianOperation c.majorana h * c.majorana i * star (gaussianOperation c.majorana h) =
          ∑ j, (R i j : ℂ) • c.majorana j) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P77

end

Source

Matchgates and classical simulation of quantum circuits, arXiv:0804.4050v2, PDF p. 9, Theorem 3: Gaussian conjugation induces every special orthogonal rotation

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number $n$ and every family $c_i$ , $0\le i<2n$ , of Hermitian complex matrices indexed by $Q_n=\{0,1\}^n$ satisfying

c_i c_j+c_j c_i= \begin{cases} 2I,&i=j,\\ 0,&i\ne j, \end{cases}

define $G_h=\exp(-\sum_{i\ne j}h_{ij}c_i c_j)$ for each real $2n\times2n$ matrix $h$ . The theorem asserts both of the following: for every $h$ satisfying $h_{ij}=-h_{ji}$ for all indices, the matrices $R_+=\exp(4h)$ and $R_-=\exp(-4h)$ each satisfy $R_\pm^{\mathsf T}R_\pm=I_{2n}$ and $\det R_\pm=1$ , and, for every index $i$ ,

G_hc_iG_h^\dagger=\sum_{j=0}^{2n-1}(R_+)_{ij}c_j, \qquad G_h^\dagger c_iG_h=\sum_{j=0}^{2n-1}(R_-)_{ij}c_j;

also, for every real matrix $R$ satisfying $R^{\mathsf T}R=I_{2n}$ and $\det R=1$ , there exists a real matrix $h$ satisfying $h_{ij}=-h_{ji}$ , $\exp(4h)=R$ , and

G_hc_iG_h^\dagger=\sum_{j=0}^{2n-1}R_{ij}c_j \quad\text{for every }i.

Here $\dagger$ denotes conjugate transpose. The existentially quantified $h$ is not asserted to be unique. The statement includes $n=0$ , when the conjugation assertions have no indices, $G_h=I$ , and the real rotation matrices are empty.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph