Sufficiency for a charge-invariant code

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.charge_invariant_sufficient

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$ . Assume that $CWW^\dagger=WW^\dagger C$ . If one complex coefficient array satisfies

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

then the code is correctable. The hypothesis concerns the code projector, and permits a code containing multiple charge sectors.

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.6, following Corollary 6: the displayed code-PROJECTOR
commutation condition makes Eq.(21) sufficient. -/
theorem charge_invariant_sufficient [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)
    (hinvariant : sectorChargeObservable s * (W * Wᴴ) = (W * Wᴴ) * sectorChargeObservable s)
    (hcoeff : ChargeCoefficients s A W) :
    PhysicallyCorrectable (sectorProject s) (krausApply A) 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 B following Corollary 6: sufficiency for a charge-invariant code

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, mutually orthogonal and summing to $I$ , with pairwise distinct real values $v_i$ , and define $\mathcal P(X)=\sum_iP_iXP_i$ and $C=\sum_iv_iP_i$ . Let $A_n\in\operatorname{Mat}(H)$ , $n\in J$ , satisfy $\sum_nA_n^\dagger A_n=I$ , set $\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$ . Suppose $W$ is an $H\times L$ matrix with $W^\dagger W=I$ , that $CWW^\dagger=WW^\dagger C$ , and that complex coefficients $c_{ijnm}$ exist satisfying

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

Then there exists a channel $R(Y)=\sum_aV_aYV_a^\dagger$ , for a finite family with $\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$ . 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