Eqs.(12)–(14): universal multi-copy Choi simulation

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.universal_choi_simulation

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Fix an input dimension $d\ge2$ , output dimension $e\ge1$ , and integer $M\ge2$ . Let $T_{d,e,M}$ be the map explicitly obtained by Alice's standard PBT measurement and Bob's selection of the indicated output port; Alice's residual output is trivial. This map is trace-preserving LOCC and CPTP, and is fixed before the channel. For every CPTP channel $\mathcal E:d\to e$ , its normalized Choi state $\rho_{\mathcal E}$ , and every input operator $X$ ,

\mathcal E^M(X):=\mathcal E(\Gamma_{d,M}(X))=T_{d,e,M}(X\otimes\rho_{\mathcal E}^{\otimes M}),\qquad\|\mathcal E-\mathcal E^M\|_\diamond\le\delta_{d,M}.

The identity holds on all operators and therefore preserves reference coherences. The source attributes the underlying PBT simulation idea to reference [21]; the present bound applies also to rectangular channels.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P49

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P49

open QAlgorithms Filter

open scoped Matrix ComplexConjugate ComplexOrder BigOperators

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Information100.P63 (Mat tensorPower)

open QAlgorithms.Papers.Independent.Dependency50.P18 (bipartiteTensor)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond AdaptiveTest adaptiveInput adaptiveAccept)

open QAlgorithms.Papers.Independent.Bridge50.P25
  (LOCCOn normalizedChannelChoi TwoWayGenerationCode TwoWayChannelProtocol
   generationCodeError twoWayGenerationCapacity sendChannelRegister StateFunctional
   IsDimensionChangingLOCCMonotone privateStateInPartyOrder)

open QAlgorithms.Papers.Independent.Support50.P07 (amplitudeDampingChannel)

/-- PDF pp.3--4, (12)--(14): the explicitly computed selection LOCC is
independent of E; equality holds on all operators and hence with references.
The underlying PBT channel-simulation idea is attributed by the source to [21]. -/
theorem universal_choi_simulation (d e M : ℕ) [NeZero d] [NeZero e]
    (hd : 2 ≤ d) (hM : 2 ≤ M) :
    LOCCOn (pbtSelection d e M) ∧ IsChannel (pbtSelection d e M) ∧
    ∀ E : Superop (Fin d) (Fin e), IsChannel E →
      (∀ X a b, simulated E M X a b =
        pbtSelection d e M (pbtSimulationInput E M X) ((),a) ((),b)) ∧
      diamond (fun X => E X - simulated E M X) ≤ pbtError d M := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 4, Eqs.(12)–(14): universal multi-copy Choi simulation

Read-back

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

For all natural numbers $d,e,M$ , equipped with $d\ne0$ and $e\ne0$ , with $d\ge2$ and $M\ge2$ , define the following selection map $\mathcal T_{d,e,M}$ . Its input consists of a $d$ -dimensional register, $M$ further $d$ -dimensional registers, and $M$ $e$ -dimensional registers. On the first two parts define

S_i[(x,a),(y,b)] =\frac1d\,\mathbf1_{\{x=a_i,\ y=b_i,\ a_j=b_j\ \forall j\ne i\}}, \quad S=\sum_iS_i,\quad R=f(S),\quad f(t)=(\sqrt t)^{-1},\ f(0)=0, \quad Q_i=RS_iR+\frac1M(I-RSR).

The output, whose additional singleton factor is suppressed, is

\mathcal T_{d,e,M}(Z)_{u,v} =\sum_{\substack{i,p,q,b,c\\b_i=u,\ c_i=v\\b_j=c_j\ (j\ne i)}} (Q_i)_{q,p}Z_{(p,b),(q,c)}.

Let $\Phi_d=d^{-1}\sum_{x,y}|x,x\rangle\langle y,y|$ , let $\mathcal P_{d,M}(X)=\mathcal T_{d,d,M}(X\otimes\Phi_d^{\otimes M})$ , and, for any map $\mathcal E$ , put

J_{\mathcal E}=(\operatorname{id}_d\otimes\mathcal E)(\Phi_d), \qquad \widetilde{\mathcal E}_M=\mathcal E\circ\mathcal P_{d,M}.

The selection map is both a channel—meaning it has a finite Kraus representation with Kraus operators satisfying $\sum_jK_j^\dagger K_j=I$ —and a finite LOCC map. Here finite LOCC means that, after relabeling each finite register by its chosen bijection with a standard finite index set, the map is built recursively from the identity and local finite Kraus measurements satisfying this completeness equation, with an outcome-dependent finite LOCC continuation and a sum over outcomes. For every channel $\mathcal E$ from dimension $d$ to dimension $e$ , every complex $d\times d$ matrix $X$ , and every $a,b\in\{0,\ldots,e-1\}$ ,

\widetilde{\mathcal E}_M(X)_{a,b} =\mathcal T_{d,e,M}\bigl(X\otimes J_{\mathcal E}^{[M]}\bigr)_{a,b}, \qquad J_{\mathcal E}^{[M]}[(u,v),(u',v')] =\prod_{i=0}^{M-1}J_{\mathcal E}[(u_i,v_i),(u_i',v_i')].

Furthermore,

\Delta_d(\mathcal E-\widetilde{\mathcal E}_M) \le \Delta_d(\operatorname{id}-\mathcal P_{d,M}), \qquad \Delta_d(\mathcal F)= \sup_{\|Z\|_1\le1}\|(\operatorname{id}_d\otimes\mathcal F)(Z)\|_1, \quad \|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z},

where the supremum ranges over all matrices $Z$ on two $d$ -dimensional registers.

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