Necessary charge-resolved correction condition

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.charge_resolved_necessary

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 $P_1,\ldots,P_r$ be nonzero orthogonal Hermitian sector projectors summing to $I$ , let $C=\sum_i c_iP_i$ have pairwise distinct real eigenvalues, and put $\mathcal P(X)=\sum_iP_iXP_i$ . Let $\mathcal N(X)=\sum_nE_nXE_n^\dagger$ have a finite normalized Kraus family and satisfy $\mathcal P\mathcal N\mathcal P=\mathcal P\mathcal N$ . Let $W$ be an isometry from a nonzero logical space. Correctability means existence of a CPTP $\mathcal R$ with $\mathcal P\mathcal R\mathcal P=\mathcal P\mathcal R$ and $\mathcal R\mathcal N(WXW^\dagger)=\mathcal P(WXW^\dagger)$ for every logical matrix $X$ . If the code is correctable, then one complex array $(c_{ijnm})$ satisfies

W^\dagger E_n^\dagger P_jE_mW=\sum_i c_{ijnm}W^\dagger P_iW\quad\text{for all }j,n,m.

This necessary linear condition alone is not asserted sufficient for an arbitrary code.

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.5, Corollary 6, Eq.(21): necessity only, without code invariance. -/
theorem charge_resolved_necessary [Nonempty H] [Nonempty L] {r : ℕ}
    (s : Sectors H r) (A : J → Mat H) (hA : IsKrausFamily A)
    (hphys : IsPhysicalChannel (sectorProject s) (sectorProject s) (krausApply A))
    (W : Matrix H L ℂ) (hW : Wᴴ * W = 1)
    (hcorr : PhysicallyCorrectable (sectorProject s) (krausApply A) W) :
    ChargeCoefficients s A W := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P44

end

Source

Approximate recovery with locality and symmetry constraints, arXiv:1806.10324v2, PDF p. 5, Corollary 6, Eq.(21): necessary charge-resolved correction condition

Read-back

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

Let $H,L$ be nonempty finite index types with decidable equality, $J$ a finite index type, and $r$ a natural number. Let $P_i$ , $i<r$ , be nonzero Hermitian projections on $\mathbb C^H$ , mutually orthogonal and summing to $I$ , carrying pairwise distinct real values $v_i$ , and put $\mathcal P(X)=\sum_iP_iXP_i$ . Suppose matrices $A_n$ , $n\in J$ , satisfy $\sum_nA_n^\dagger A_n=I$ ; put $\mathcal N(X)=\sum_nA_nXA_n^\dagger$ , and assume $\mathcal P(\mathcal N(\mathcal P(X)))=\mathcal P(\mathcal N(X))$ for every $X$ . Let $W$ be an $H\times L$ matrix with $W^\dagger W=I$ . Assume there exists a channel $R(Y)=\sum_aV_aYV_a^\dagger$ , with a finite family satisfying $\sum_aV_a^\dagger V_a=I$ , such that $\mathcal P(R(\mathcal P(Y)))=\mathcal P(R(Y))$ for every $Y$ and $R(\mathcal N(WXW^\dagger))=\mathcal P(WXW^\dagger)$ for every complex matrix $X$ on $L$ . Then there exist complex coefficients $c_{ijnm}$ such that

W^\dagger A_n^\dagger P_jA_mW =\sum_{i=0}^{r-1}c_{ijnm}W^\dagger P_iW \quad\text{for every }j<r,\ n,m\in J.

No positivity or normalization of these coefficients is asserted. The hypotheses exclude $r=0$ and empty $J$ .

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