Equivalent exact tensor-local correction criteria

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.tensor_local_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 $\mathcal N_A(X)=\sum_iE_iXE_i^\dagger$ have a normalized finite Kraus family and let $W:H_L\to H_A\otimes H_B$ be an isometry. Define $W_m=(I\otimes\langle m|)W$ in a fixed basis of $H_B$ . Exact correction on this code by a CPTP recovery on $A$ is equivalent to each of the following:

A single normalized environment density $\sigma$ satisfies, for all environment matrices $X$ and all matrices $B$ on $H_B$ ,

\sum_{ij}X_{ij}W^\dagger(E_i^\dagger E_j\otimes B)W=\operatorname{Tr}(\sigma X)W^\dagger(I\otimes B)W.

A single complex array $\lambda_{ij}$ satisfies

W^\dagger(E_i^\dagger E_j\otimes B)W=\lambda_{ij}W^\dagger(I\otimes B)W\quad\text{for all }i,j,B.

A single complex array $\lambda_{ij}$ satisfies

W_m^\dagger E_i^\dagger E_jW_n=\lambda_{ij}W_m^\dagger W_n\quad\text{for all }i,j,m,n.

The coefficients are uniform in $B,m,n$ , and no product-code restriction is imposed.

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.9--10, Eqs.(49)--(51): all three equivalent exact criteria.
The state and each lambda_ij are chosen before B,m,n. -/
theorem tensor_local_exact_criteria [Nonempty H] [Nonempty B] [Nonempty L]
    (A : J → Mat H) (hA : IsKrausFamily A)
    (W : Matrix (H × B) L ℂ) (hW : Wᴴ * W = 1) :
    (TensorCorrectable (krausApply A) W ↔
      ∃ sigma : Mat J, IsDensityMatrix sigma ∧ ∀ (X : Mat J) (Y : Mat B),
        (∑ i, ∑ j, X i j •
          (Wᴴ * Matrix.kronecker ((A i)ᴴ * A j) Y * W)) =
        (sigma * X).trace • (Wᴴ * Matrix.kronecker (1 : Mat H) Y * W)) ∧
    (TensorCorrectable (krausApply A) W ↔
      ∃ lambda : J → J → ℂ, ∀ i j (Y : Mat B),
        Wᴴ * Matrix.kronecker ((A i)ᴴ * A j) Y * W =
        lambda i j • (Wᴴ * Matrix.kronecker (1 : Mat H) Y * W)) ∧
    (TensorCorrectable (krausApply A) W ↔
      ∃ lambda : J → J → ℂ, ∀ i j m n,
        (codeSlice W m)ᴴ * (A i)ᴴ * A j * codeSlice W n =
        lambda i j • ((codeSlice W m)ᴴ * codeSlice W n)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P44

end

Source

Approximate recovery with locality and symmetry constraints, arXiv:1806.10324v2, PDF p. 9, §IV D, Eqs.(49)–(51): exact tensor-local correction criterion

Read-back

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

Let $H,B,L,J$ be finite index types with decidable equality, with $H,B,L$ nonempty; let $A_i$ be complex matrices on $H$ , indexed by $i\in J$ , satisfying $\sum_iA_i^\dagger A_i=I_H$ ; and let $W:\mathbb C^L\to\mathbb C^H\otimes\mathbb C^B$ satisfy $W^\dagger W=I_L$ . Write $N(X)=\sum_iA_iXA_i^\dagger$ , and write $W_m$ for the matrix with entries $(W_m)_{a\ell}=W_{(a,m),\ell}$ . Define correctability to mean the existence of a channel $R$ on $H$ such that $((R\circ N)\otimes\mathrm{id}_B)(WXW^\dagger)=WXW^\dagger$ for every complex matrix $X$ on $L$ ; a channel has a finite Kraus representation with $\sum_jE_j^\dagger E_j=I$ . The theorem asserts all three equivalences

\begin{aligned} \text{correctability} &\iff \exists\,\sigma\geq0,\ \operatorname{tr}\sigma=1,\quad \forall X\in\mathbb C^{J\times J},\ \forall Y\in\mathbb C^{B\times B},\\[-2pt] &\hspace{15pt}\sum_{i,j}X_{ij}\, W^\dagger(A_i^\dagger A_j\otimes Y)W =\operatorname{tr}(\sigma X)\, W^\dagger(I_H\otimes Y)W;\\ \text{correctability} &\iff \exists\,\lambda:J\times J\to\mathbb C,\quad \forall i,j,Y,\quad W^\dagger(A_i^\dagger A_j\otimes Y)W =\lambda_{ij}W^\dagger(I_H\otimes Y)W;\\ \text{correctability} &\iff \exists\,\lambda:J\times J\to\mathbb C,\quad \forall i,j\in J,\ \forall m,n\in B,\quad W_m^\dagger A_i^\dagger A_jW_n=\lambda_{ij}W_m^\dagger W_n. \end{aligned}

The witnesses in these three equivalences are separately existentially quantified, and no positivity or normalization is explicitly required of either $\lambda$ . All matrix tests $X,Y$ are unrestricted. Although $J$ is not assumed nonempty, an empty $J$ cannot satisfy the Kraus normalization when $H$ is nonempty; likewise the isometry hypothesis requires $|L|\leq |H||B|$ .

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