Exact constrained recovery with positive conditional states

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.exact_constrained_recovery

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$ . The code is correctable if and only if there exist environment matrices $\sigma_{j|i}$ such that

\sigma_{j|i}\succeq0,\qquad\sum_j\operatorname{Tr}\sigma_{j|i}=1\quad\text{for each }i,

W^\dagger E_n^\dagger P_jE_mW=\sum_i\langle n|\sigma_{j|i}|m\rangle W^\dagger P_iW\quad\text{for all }j,n,m.

This is a positive, normalized classical–quantum conditional-output criterion; it does not normalize each block separately.

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, Eqs.(18),(20): necessary AND sufficient, including positivity
and total conditional normalization. -/
theorem exact_constrained_recovery [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) :
    PhysicallyCorrectable (sectorProject s) (krausApply A) W ↔
      ChargeStateCondition 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, §III B, Eqs.(18),(20): exact constrained recovery criterion

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. Suppose $P_i\in\operatorname{Mat}(H)$ , $i<r$ , are nonzero Hermitian projections, mutually orthogonal and summing to $I$ , with pairwise distinct real values $v_i$ . Put $\mathcal P(X)=\sum_iP_iXP_i$ . Let $A_n\in\operatorname{Mat}(H)$ , $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$ . Then there exists a channel $R$ , meaning $R(Y)=\sum_aV_aYV_a^\dagger$ for some finite family with $\sum_aV_a^\dagger V_a=I$ , satisfying

\mathcal P(R(\mathcal P(Y)))=\mathcal P(R(Y))\quad\text{for every }Y, \qquad R(\mathcal N(WXW^\dagger))=\mathcal P(WXW^\dagger)\quad\text{for every }X\in\operatorname{Mat}(L),

if and only if there exist positive semidefinite matrices $\sigma_{ij}\in\operatorname{Mat}(J)$ satisfying $\sum_j\operatorname{tr}(\sigma_{ij})=1$ for every $i<r$ and $W^\dagger A_n^\dagger P_jA_mW=\sum_i(\sigma_{ij})_{nm}W^\dagger P_iW$ for every $j<r$ and $n,m\in J$ . The assumptions 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