Physical inversion of definite-parity unitary noise

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.definite_parity_unitary_invertible

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

prove2quantum

All Hilbert spaces are finite dimensional and nonzero, and every channel is completely positive and trace preserving on the full matrix algebra. Let $C$ be total fermionic parity and $\mathcal P(X)=(X+CXC)/2$ . Let $U$ be unitary and have definite parity, $UC=CU$ or $UC=-CU$ . Then $\mathcal N=\operatorname{Ad}_U$ and $\mathcal R=\operatorname{Ad}_{U^\dagger}$ are physical CPTP channels and

\mathcal R\mathcal N(X)=X\quad\text{for every matrix }X.

In particular the inverse physically corrects the noise, including when $U$ flips total parity.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P44

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P44

open scoped Matrix ComplexConjugate ComplexOrder

open QAlgorithms.Papers.Independent.Information100.P60 (Mat)

open QAlgorithms.Papers.Independent.Information100.P67 (mapFirst)

open QAlgorithms.Papers.Independent.Claimed50.P48 (operatorTraceDual)

open QAlgorithms.Papers.Independent.Renew46.P43 (purification)

variable {H K L J E F B : Type*}

variable [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K]

variable [Fintype L] [DecidableEq L] [Fintype J] [DecidableEq J]

variable [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]

variable [Fintype B] [DecidableEq B]

/-- PDF p.6, Section III C: a definite-parity unitary and its inverse are
physical; parity-flipping unitaries are included. 
Parity correction, PDF p.2 Eq.(1): printed i^(|omega|-1) for Majorana labels;
changed to i^m on 2m ordered modes. Why: the printed four-mode value is
anti-Hermitian with square -I, whereas the source requires parity sectors of
a Hermitian involution. Only this normalization (up to sign) is corrected. -/
theorem definite_parity_unitary_invertible {n : ℕ} (f : Fermions n)
    (U : Mat (Fin (2 ^ n))) (hU : Uᴴ * U = 1) (hUU : U * Uᴴ = 1)
    (hparity : DefiniteParity (totalParity f) U) :
    IsChannel (conjSuperop U) ∧ IsChannel (conjSuperop Uᴴ) ∧
    IsPhysicalChannel (parityProject (totalParity f)) (parityProject (totalParity f))
      (conjSuperop U) ∧
    IsPhysicalChannel (parityProject (totalParity f)) (parityProject (totalParity f))
      (conjSuperop Uᴴ) ∧
    ∀ X, conjSuperop Uᴴ (conjSuperop U X) = X := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P44

end

Source

Approximate recovery with locality and symmetry constraints, arXiv:1806.10324v2, PDF p. 6, §III C: physical invertibility of definite-parity unitary noise

Read-back

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

For every natural number $n$ , let $w_0,\ldots,w_{2n-1}$ be Hermitian $2^n\times2^n$ matrices satisfying $w_iw_j+w_jw_i=2\delta_{ij}I$ , and put $C=\mathrm{i}^{\,n}w_0\cdots w_{2n-1}$ and $P(X)=\tfrac12(X+CXC)$ . For every matrix $U$ satisfying both $U^\dagger U=I$ and $UU^\dagger=I$ , and satisfying $UC=CU$ or $UC=-CU$ , the maps $\mathcal U(X)=UXU^\dagger$ and $\mathcal V(X)=U^\dagger XU$ are channels, both obey

P(\mathcal U(P(X)))=P(\mathcal U(X)), \qquad P(\mathcal V(P(X)))=P(\mathcal V(X)),

and $\mathcal V(\mathcal U(X))=X$ for every complex matrix $X$ . Here a channel means a finite Kraus sum with $\sum_jE_j^\dagger E_j=I$ . The case $n=0$ is included, with the empty product giving $C=I$ .

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