Local information–disturbance duality

Open

QAlgorithms.Papers.Independent.Intakethird100.P44.local_information_disturbance

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. Here $F$ denotes either root entanglement fidelity $F_\rho$ for any normalized input density $\rho$ , with an identity reference retained, or worst-case root entanglement fidelity $F_W$ over all normalized logical densities for an arbitrary isometry $W$ . Let $\mathcal B$ be a unital complex dagger algebra, and let $\mathcal N,\mathcal M$ be channels on its ambient space whose trace-dual adjoints fix $\mathcal B$ pointwise. Choose arbitrary Stinespring isometries $V_N:H\to H\otimes E_N$ and $V_M:H\to H\otimes E_M$ . Their local complements are $\widehat{\mathcal N}^{\mathcal B}=(\mathcal P_{\mathcal B}\otimes\mathrm{id}_{E_N})\circ\mathrm{Ad}_{V_N}$ and similarly for $\mathcal M$ , where $\mathcal P_{\mathcal B}$ is the canonical Hilbert–Schmidt projection. Then both maxima are attained and

\max_{\mathcal R^\dagger|_{\mathcal B}=\mathrm{id}}F(\mathcal R\mathcal N,\mathcal M)=\max_{\mathcal S^\dagger(B\otimes I_{E_N})=B\otimes I_{E_M}}F(\widehat{\mathcal N}^{\mathcal B},\mathcal S\widehat{\mathcal M}^{\mathcal B}).

The dual channel acts from $H\otimes E_M$ to $H\otimes E_N$ . This is the local information–disturbance tradeoff.

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.8, Theorem 8, Eq.(35), proof completed p.9. Both F_rho and F_W;
the two identity environments in S†(b ⊗ I_E)=b ⊗ I_F are typed separately. -/
theorem local_information_disturbance [Nonempty H] [Nonempty E] [Nonempty F]
    (A : ObservableAlgebra H) (N M : Superop H H)
    (hN : IsChannel N) (hM : IsChannel M)
    (hNB : FixesObservables (A.algebra : Set (Mat H)) N)
    (hMB : FixesObservables (A.algebra : Set (Mat H)) M)
    (VN : Matrix (H × E) H ℂ) (VM : Matrix (H × F) H ℂ)
    (hVN : IsChannelDilation N VN) (hVM : IsChannelDilation M VM) (c : Comparison H) :
    SameMaximum
      (fun R : Superop H H => IsChannel R ∧ FixesObservables (A.algebra : Set (Mat H)) R)
      (fun R => comparisonRootFidelity c (R ∘ N) M)
      (fun S : Superop (H × F) (H × E) => IsChannel S ∧
        ∀ X ∈ A.algebra,
          operatorTraceDual S (Matrix.kronecker X (1 : Mat E)) =
            Matrix.kronecker X (1 : Mat F))
      (fun S => comparisonRootFidelity c (localComplement A VN) (S ∘ localComplement A VM)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P44

end

Source

Approximate recovery with locality and symmetry constraints, arXiv:1806.10324v2, PDF p. 8, Theorem 8, Eq.(35): local information–disturbance duality (seed result announced on p.1)

Read-back

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

Let $H,E,F$ be nonempty finite types with decidable equality, and write $\operatorname{Mat}(I)$ for square complex matrices indexed by $I$ . For a map $T:\operatorname{Mat}(I)\to\operatorname{Mat}(J)$ , define its trace dual by $T^\vee(Y)_{ab}=\operatorname{Tr}(T(E_{ba})Y)$ , where $E_{ba}$ is a matrix unit; a channel means a map admitting a finite representation $T(X)=\sum_\ell K_\ell XK_\ell^\dagger$ with $\sum_\ell K_\ell^\dagger K_\ell=I_I$ . Let $A$ consist of a unital complex star subalgebra $\mathcal A\subseteq\operatorname{Mat}(H)$ and a channel $P$ such that $P(X)\in\mathcal A$ and $\operatorname{Tr}((X-P(X))^\dagger Y)=0$ for all matrices $X$ and all $Y\in\mathcal A$ . Suppose $N,M:\operatorname{Mat}(H)\to\operatorname{Mat}(H)$ are channels satisfying $N^\vee(Y)=M^\vee(Y)=Y$ for every $Y\in\mathcal A$ . Suppose matrices $V_N:H\to H\times E$ and $V_M:H\to H\times F$ satisfy $V_N^\dagger V_N=V_M^\dagger V_M=I_H$ and

N(X)_{ab}=\sum_{e\in E}(V_NXV_N^\dagger)_{(a,e),(b,e)},\qquad M(X)_{ab}=\sum_{f\in F}(V_MXV_M^\dagger)_{(a,f),(b,f)}

for every $X$ . Define $L_N=(P\otimes\mathrm{id}_E)\circ(X\mapsto V_NXV_N^\dagger)$ and $L_M=(P\otimes\mathrm{id}_F)\circ(X\mapsto V_MXV_M^\dagger)$ , where $P\otimes\mathrm{id}$ applies $P$ to each matrix block indexed by the second factor. Let $c$ be either a positive semidefinite trace-one matrix $\rho$ on $H$ , or an integer $k>0$ and matrix $W:\mathbb C^k\to\mathbb C^H$ satisfying $W^\dagger W=I_k$ . To define its comparison value $\mathcal F_c(T,U)$ , put $S(Z)=\operatorname{cfc}(\sqrt{\cdot})(Z)$ , $(\Pi_\rho)_{(a,b),(c,d)}=S(\rho)_{ba}\overline{S(\rho)_{dc}}$ , and $F_\rho(T,U)=\operatorname{Re}\operatorname{Tr}S(S(B)CS(B))$ , where $B=(\mathrm{id}\otimes T)(\Pi_\rho)$ , $C=(\mathrm{id}\otimes U)(\Pi_\rho)$ , and the reference extension applies each map to the corresponding matrix blocks. In the fixed case set $\mathcal F_c(T,U)=F_\rho(T,U)$ ; in the code case take the real infimum of $F_\rho(T\circ(X\mapsto WXW^\dagger),U\circ(X\mapsto WXW^\dagger))$ over all positive semidefinite trace-one $k\times k$ matrices $\rho$ . Then there exist channels $R:\operatorname{Mat}(H)\to\operatorname{Mat}(H)$ and $S:\operatorname{Mat}(H\times F)\to\operatorname{Mat}(H\times E)$ such that $R^\vee(Y)=Y$ for every $Y\in\mathcal A$ , $S^\vee(Y\otimes I_E)=Y\otimes I_F$ for every $Y\in\mathcal A$ , and

\mathcal F_c(R\circ N,M)=\mathcal F_c(L_N,S\circ L_M).

Moreover, every channel $R'$ satisfying $R'^\vee(Y)=Y$ on $\mathcal A$ has $\mathcal F_c(R'\circ N,M)\le\mathcal F_c(R\circ N,M)$ , and every channel $S'$ satisfying $S'^\vee(Y\otimes I_E)=Y\otimes I_F$ on $\mathcal A$ has $\mathcal F_c(L_N,S'\circ L_M)\le\mathcal F_c(L_N,S\circ L_M)$ . Thus both displayed optimizations have attained, equal maxima; uniqueness of the maximizing channels is not asserted.

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