Geometric support ensures exact Majorana-ring correction

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.majorana_ring_geometric_correction

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$ . Let $d=\min_j|I_j|$ . Let $\mathcal N(X)=\sum_iE_iXE_i^\dagger$ have a normalized finite Kraus family. Suppose each whole $E_i$ is an even Majorana polynomial supported on some cyclic interval of length $\ell_i$ with $2\ell_i\le d$ . The intervals may differ with $i$ . Then, writing $P_\pm=(I\pm C)/2$ , there is one complex array $\lambda_{ijs}$ such that

W^\dagger E_i^\dagger E_j(P_sBP_s)W=\lambda_{ijs}W^\dagger(P_sBP_s)W

for every $i,j,s$ and every $B$ commuting with the whole-chain even algebra. Moreover a CPTP recovery strongly local to that algebra exactly recovers $\mathcal P$ on the code. If $d=0$ , only scalar Kraus operators meet the support condition.

This is finite exact correction under geometric support, without a common support region for the channel or a standard full-code Knill–Laflamme assertion.

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.10--11, Section IV F: each even Kraus operator may have its OWN
geometric interval, of length at most half the shortest paired interval.
Conclusion is Eq.(54) and exact strong-local physical correction; the disputed
whole-code standard-KL reduction is not used or 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_ring_geometric_correction {n k : ℕ}
    (f : Fermions n) (r : RingLayout n k) (code : RingCode f r)
    (noise : J → Mat (Fin (2 ^ n))) (hnoise : IsKrausFamily noise)
    (hsupport : ∀ j, ∃ length : ℕ, 2 * length ≤ minimumGap r ∧
      HasIntervalSupport f (noise j) length) :
    RegionalCoefficients (evenRegion f Finset.univ : Set _) (totalParity f)
      noise code.W ∧
    StrongCorrectable (evenRegion f Finset.univ : Set _) (totalParity f)
      (krausApply noise) code.W := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P44

end

Source

Approximate recovery with locality and symmetry constraints, arXiv:1806.10324v2, PDF p. 10, §IV F: geometric support implies exact correction on the Majorana ring

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}$ with even cyclic gaps $g_j=(u_{(j+1)\bmod 2k}+2n-u_j-1)\bmod 2n$ . Let $W$ be a complex $2^n\times2^k$ matrix with $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),

ordered by increasing $j$ and then increasing $t$ , with empty products equal to $I$ . For a finite index type $J$ , let $A_j$ be complex $2^n\times2^n$ matrices satisfying $\sum_{j\in J}A_j^\dagger A_j=I$ . Suppose that for each $j\in J$ there exist a natural number $\ell_j$ and a starting index $s_j<2n$ such that $2\ell_j\le\min(2n,g_0,\ldots,g_{2k-1})$ and $A_j$ belongs to the complex linear span of even-length products of matrices $w_a$ whose indices satisfy $(a+2n-s_j)\bmod 2n<\ell_j$ ; repetitions, arbitrary ordering, and empty products are allowed. In particular, $\ell_j=0$ is permitted and then $A_j$ is a scalar multiple of $I$ ; an empty $J$ cannot satisfy the normalization above. Write $\mathcal A$ for the complex linear span of all even-length products of the $w_a$ , set $C=\mathrm i^n w_0\cdots w_{2n-1}$ , and put $P_b=\frac12(I+(-1)^bC)$ for $b\in\{0,1\}$ . The first conclusion is that there exist complex coefficients $\lambda_{ijb}$ such that, for every $i,j\in J$ , every $b\in\{0,1\}$ , and every matrix $Y$ commuting with every element of $\mathcal A$ ,

W^\dagger A_i^\dagger A_j(P_bYP_b)W =\lambda_{ijb}\,W^\dagger(P_bYP_b)W.

The second conclusion is that there exists a channel $\mathcal R$ , admitting a finite Kraus representation with Kraus operators $K_a$ satisfying $\sum_aK_a^\dagger K_a=I$ , whose trace dual $\mathcal R^\vee(Y)_{ab}=\operatorname{tr}(\mathcal R(E_{ba})Y)$ sends every element of $\mathcal A$ into $\mathcal A$ and fixes every matrix commuting with $\mathcal A$ , and such that

\mathcal R\left(\sum_{j\in J}A_jWZW^\dagger A_j^\dagger\right) =\frac12\left(WZW^\dagger+CWZW^\dagger C\right)

for every complex $2^k\times2^k$ 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