Exact strong-local correction for fermionic site regions

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.fermionic_site_exact_criteria

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 $\omega$ be a set of fermionic sites, possibly empty, and $\mathcal A_\omega$ its even local CAR algebra on the full Fock space. Let $C_\omega$ be regional parity, $P_\pm=(I\pm C_\omega)/2$ , and $\mathcal N(X)=\sum_iE_iXE_i^\dagger$ a normalized channel with $E_i\in\mathcal A_\omega$ . Let $W$ be any isometric code. Strong locality means the adjoint preserves $\mathcal A_\omega$ and fixes its full ambient commutant $\mathcal A_\omega'$ pointwise. The target projection onto $\mathcal A_\omega\vee\mathcal A_\omega'$ is regional parity dephasing. Exact strong-local correction to this physical target is equivalent to each condition:

There are normalized environment densities $\rho_+,\rho_-$ such that for every $B\in\mathcal A_\omega'$ and environment matrix $X$ ,

\sum_{ij}X_{ij}W^\dagger E_i^\dagger BE_jW=\sum_{s\in\{+,-\}}\operatorname{Tr}(\rho_sX)W^\dagger P_sBP_sW.

One complex array $\lambda_{ijs}$ , uniform in $B$ , satisfies, with $B_s=P_sBP_s$ ,

W^\dagger E_i^\dagger E_jB_sW=\lambda_{ijs}W^\dagger B_sW\quad\text{for all }i,j,s,\ B\in\mathcal A_\omega'.

The $B_s$ commute with the noise operators. For $\omega=\varnothing$ , $C_\omega=I$ and $P_-=0$ ; no nonzero-sector assumption is added.

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.10, Eqs.(53)--(54): exact strong-local correction for fermionic
SITE regions. The empty region is allowed; its unused minus sector is zero. 
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 fermionic_site_exact_criteria {n : ℕ} [Nonempty L] [Nonempty J]
    (f : Fermions n) (omega : Finset (Fin n))
    (noise : J → Mat (Fin (2 ^ n))) (hnoise : IsKrausFamily noise)
    (hlocal : ∀ i, noise i ∈ evenRegion f (siteModes omega))
    (W : Matrix (Fin (2 ^ n)) L ℂ) (hW : Wᴴ * W = 1) :
    (StrongCorrectable (evenRegion f (siteModes omega) : Set _) (regionParity f omega)
        (krausApply noise) W ↔
      RegionalStateCondition (evenRegion f (siteModes omega) : Set _)
        (regionParity f omega) noise W) ∧
    (StrongCorrectable (evenRegion f (siteModes omega) : Set _) (regionParity f omega)
        (krausApply noise) W ↔
      RegionalCoefficients (evenRegion f (siteModes omega) : Set _)
        (regionParity f omega) noise 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 E, Eqs.(53)–(54): exact strong local correction for fermionic site regions

Read-back

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

For every natural number $n$ , nonempty finite index types $L,J$ with decidable equality, a family $(w_j)_{0\le j<2n}$ of Hermitian complex $2^n\times2^n$ matrices satisfying $w_iw_j+w_jw_i=2I$ for $i=j$ and $0$ otherwise, and every finite set $\omega\subseteq\{0,\ldots,n-1\}$ , put $S=\{j<2n:\exists s\in\omega,\ \lfloor j/2\rfloor=s\}$ , let $\mathcal A$ be the complex linear span of all products $w_{j_1}\cdots w_{j_{2t}}$ with every $j_a\in S$ , including the empty product $I$ , and put $C=\mathrm{i}^{|\omega|}\prod_{j\in S}^{\text{in increasing order}}w_j$ and $P_{\mathrm{false}}=(I+C)/2,\ P_{\mathrm{true}}=(I-C)/2$ . For every family $(N_i)_{i\in J}$ belonging to $\mathcal A$ and satisfying $\sum_iN_i^\dagger N_i=I$ , and every matrix $W\in\mathbb C^{2^n\times L}$ satisfying $W^\dagger W=I$ , the theorem asserts both $\mathcal C\iff\mathcal S$ and $\mathcal C\iff\mathcal L$ , where $\mathcal C$ means that there exists a channel $R(Z)=\sum_aE_aZE_a^\dagger$ , with a finite Kraus family satisfying $\sum_aE_a^\dagger E_a=I$ , whose trace dual $[R^\vee(Y)]_{ab}=\operatorname{tr}(R(E_{ba})Y)$ maps $\mathcal A$ into itself and fixes every matrix commuting with $\mathcal A$ , and which satisfies

R\!\left(\sum_iN_iWXW^\dagger N_i^\dagger\right) =\frac12\left(WXW^\dagger+C\,WXW^\dagger C\right) \quad\text{for every }X\in\mathbb C^{L\times L};

$\mathcal S$ means that there exist positive semidefinite $J\times J$ matrices $\rho_{\mathrm{false}},\rho_{\mathrm{true}}$ , each of trace $1$ , such that

\sum_{i,j}X_{ij}W^\dagger N_i^\dagger YN_jW =\sum_k\operatorname{tr}(\rho_kX)\,W^\dagger P_kYP_kW

for every complex $J\times J$ matrix $X$ and every $Y$ commuting with $\mathcal A$ ; and $\mathcal L$ means that there exist complex scalars $\lambda_{ijk}$ such that

W^\dagger N_i^\dagger N_j(P_kYP_k)W =\lambda_{ijk}W^\dagger(P_kYP_k)W

for every $i,j\in J$ , Boolean $k$ , and every $Y$ commuting with $\mathcal A$ . No nonemptiness assumption on $\omega$ or positivity assumption on $n$ is made: for $\omega=\varnothing$ , one has $\mathcal A=\mathbb CI$ and $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