Two free-Majorana jumps obstruct physical recovery

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.majorana_poisoning_not_correctable

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. Consider $2n$ Majorana operators $w_a=w_a^\dagger$ on the $2^n$ -dimensional Fock space, satisfying $\{w_a,w_b\}=2\delta_{ab}I$ . There are $2k>0$ free modes in cyclic order, with even-length intervals $I_j$ of nearest-neighbor paired modes between consecutive free modes. The isometry $W$ encodes all $2^k$ free-mode states and initializes each paired fermion in its specified vacuum; its range projector is the product of the paired-mode vacuum projectors. Write $C$ for total parity and $\mathcal P(X)=(X+CXC)/2$ . Suppose $2k>2$ , and define

\mathcal N(X)=\tfrac12\bigl(w_{\omega_1}Xw_{\omega_1}+w_{\omega_2}Xw_{\omega_2}\bigr),\qquad M=iw_{\omega_2}w_{\omega_3}.

Then $\mathcal N$ is physical and CPTP, $\mathcal N^\dagger(M)=0$ , and $M$ commutes with $C$ and $WW^\dagger$ . Its logical compression $W^\dagger MW$ is not scalar. There is no physical CPTP recovery satisfying

\mathcal R\mathcal N(WXW^\dagger)=\mathcal P(WXW^\dagger)\quad\text{for every logical matrix }X.

Thus this poisoning noise destroys recoverable physical logical information; no numerical optimum is claimed.

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 pp.6--7, Section III C: physical but uncorrectable poisoning when
there are more than two free Majoranas; the stated physical logical witness
is annihilated. No numerical optimal-fidelity estimate is asserted. 
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 majorana_poisoning_not_correctable {n k : ℕ}
    (f : Fermions n) (r : RingLayout n k) (code : RingCode f r) (hk : 2 < 2 * k) :
    let a : Fin (2 * k) := ⟨1, by omega⟩
    let b : Fin (2 * k) := ⟨2, by omega⟩
    let M := Complex.I • (f.w (r.free a) * f.w (r.free b))
    IsChannel (poisoning f r) ∧
    IsPhysicalChannel (parityProject (totalParity f)) (parityProject (totalParity f))
      (poisoning f r) ∧
    operatorTraceDual (poisoning f r) M = 0 ∧
    M * totalParity f = totalParity f * M ∧
    M * (code.W * code.Wᴴ) = (code.W * code.Wᴴ) * M ∧
    (¬ ∃ z : ℂ, code.Wᴴ * M * code.W = z • (1 : Mat (Fin (2 ^ k)))) ∧
    ¬ PhysicallyCorrectable (parityProject (totalParity f)) (poisoning f r) code.W := 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: two unpaired-Majorana jumps prevent physical recovery

Read-back

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

For all natural numbers $n,k$ , let $w_0,\ldots,w_{2n-1}$ be Hermitian complex $2^n\times2^n$ matrices satisfying $w_iw_j+w_jw_i=2\delta_{ij}I$ , and let a ring layout specify $n,k>0$ and strictly increasing free indices $u_0,\ldots,u_{2k-1}$ whose cyclic gaps $g_j=(u_{(j+1)\bmod 2k}+2n-u_j-1)\bmod 2n$ are even. Let $W$ be a complex $2^n\times2^k$ matrix satisfying $W^\dagger W=I$ and

WW^\dagger= \prod_{j=0}^{2k-1}\ \prod_{t=0}^{g_j/2-1} \frac12\left(I-\mathrm i\, w_{(u_j+1+2t)\bmod 2n}\, w_{(u_j+2+2t)\bmod 2n}\right),

where products follow increasing $j$ and then increasing $t$ , and an empty product is $I$ . Assume also $2<2k$ . Define

C=\mathrm i^n w_0\cdots w_{2n-1},\qquad \mathcal P(X)=\tfrac12(X+CXC),\qquad \mathcal N(X)=\tfrac12(w_{u_0}Xw_{u_0}^\dagger+w_{u_1}Xw_{u_1}^\dagger), \qquad M=\mathrm i\,w_{u_1}w_{u_2}.

Then $\mathcal N$ is a channel, meaning that it admits a finite representation $\mathcal N(X)=\sum_a K_aXK_a^\dagger$ with $\sum_aK_a^\dagger K_a=I$ ; it satisfies $\mathcal P(\mathcal N(\mathcal P(X)))=\mathcal P(\mathcal N(X))$ for every matrix $X$ ; its trace dual annihilates $M$ ; $M$ commutes with both $C$ and $WW^\dagger$ ; and $W^\dagger MW$ is not $zI$ for any $z\in\mathbb C$ . Here the trace dual is defined entrywise by $\mathcal N^\vee(Y)_{ab}=\operatorname{tr}(\mathcal N(E_{ba})Y)$ , with $E_{ba}$ the matrix unit. Finally, there exists no channel $\mathcal R$ satisfying both

\mathcal P(\mathcal R(\mathcal P(X)))=\mathcal P(\mathcal R(X)) \quad\text{for every physical-space matrix }X, \qquad \mathcal R(\mathcal N(WZW^\dagger))=\mathcal P(WZW^\dagger) \quad\text{for every complex }2^k\times2^k\text{ matrix }Z.

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