Definite-parity Kraus representation

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.definite_parity_kraus

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 parity for a finite spinless-fermion Fock space, and put $\mathcal P=\mathcal Q:X\mapsto(X+CXC)/2$ . A channel $\mathcal N$ is physical if $\mathcal Q\mathcal N\mathcal P=\mathcal Q\mathcal N$ . A Kraus operator has definite parity when it commutes or anticommutes with $C$ . Then

\bigl[\mathcal N\text{ has a normalized definite-parity Kraus representation}\bigr]\Longrightarrow\mathcal N\text{ physical},

\mathcal N\text{ physical}\Longrightarrow\mathcal Q\mathcal N=\mathcal Q\mathcal N\mathcal P\text{ has such a representation}.

The projected channel has the same physical-observable action. Both parity-preserving and parity-flipping Kraus operators are allowed.

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.3, Proposition 1. The converse represents the PHYSICALLY
EQUIVALENT projected channel QN, not necessarily N on forbidden coherences. 
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_kraus {n : ℕ} (f : Fermions n)
    (N : Superop (Fin (2 ^ n)) (Fin (2 ^ n))) (hN : IsChannel N) :
    ((∃ (m : ℕ) (A : Fin m → Mat (Fin (2 ^ n))), IsKrausFamily A ∧
        N = krausApply A ∧ ∀ j, DefiniteParity (totalParity f) (A j)) →
      IsPhysicalChannel (parityProject (totalParity f)) (parityProject (totalParity f)) N) ∧
    (IsPhysicalChannel (parityProject (totalParity f)) (parityProject (totalParity f)) N →
      ∃ (m : ℕ) (A : Fin m → Mat (Fin (2 ^ n))), IsKrausFamily A ∧
        parityProject (totalParity f) ∘ N = krausApply A ∧
        ∀ j, DefiniteParity (totalParity f) (A j)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P44

end

Source

Approximate recovery with locality and symmetry constraints, arXiv:1806.10324v2, PDF p. 3, Proposition 1: definite-parity Kraus representation

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 matrices on $\mathbb C^{2^n}$ satisfying $w_iw_j+w_jw_i=2\delta_{ij}I$ , put $C=\mathrm{i}^{\,n}w_0\cdots w_{2n-1}$ , and define $P(X)=\tfrac12(X+CXC)$ . Let $N$ be a channel on this space, meaning that it has a finite Kraus representation with $\sum_jA_j^\dagger A_j=I$ . The theorem asserts two implications: if there exist $m\geq0$ and matrices $A_0,\ldots,A_{m-1}$ with that normalization, $N(X)=\sum_jA_jXA_j^\dagger$ for every $X$ , and each $A_jC=CA_j$ or $A_jC=-CA_j$ , then $P(N(P(X)))=P(N(X))$ for every matrix $X$ ; conversely, if this last identity holds for every $X$ , then there exist $m\geq0$ and normalized Kraus matrices of definite parity representing $P\circ N$ :

P(N(X))=\sum_{j=0}^{m-1}A_jXA_j^\dagger, \qquad A_jC=CA_j\ \text{or}\ A_jC=-CA_j.

The case $n=0$ is included, with $C=I$ , $P$ the identity map, and every matrix commuting with $C$ .

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