Lemma 13 / Eq.(106): Choi link product for a wired code

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.wired_choi_link

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

prove2quantum

All systems have finite positive dimension and fixed computational bases. Matrix order is Loewner order and logarithms are base two.

Let $\mathcal N:A_o\to B_i$ be CPTP and let $\Pi:A_iB_i\to A_oB_o$ be a bipartite CPTP code no-signalling in both directions. Define $\widetilde{\mathcal M}:A_i\to B_o$ by wiring the actual operations through $\mathcal N$ , independently of their Choi matrices. Then

J_{\widetilde{\mathcal M}}=\operatorname{Tr}_{A_oB_i}[(J_{\mathcal N}^{T}\otimes I_{A_iB_o})J_\Pi].

The transpose acts on the entire resource Choi matrix, with explicit register permutations. The formula relates the independently wired channel to its Choi representation.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P65

Formal statement

noncomputable section

open Filter QAlgorithms

open scoped BigOperators Matrix ComplexConjugate ComplexOrder Topology

namespace QAlgorithms.Papers.Independent.Intakethird100.P65

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P09 (transposeBob)

open QAlgorithms.Papers.Independent.Dependency50.P35 (maxRelative)

open QAlgorithms.Papers.Independent.Independent2.P01 (dampingKraus damping)

open QAlgorithms.Papers.Independent.Gap48.P33 (phaseFlipChannel)

open QAlgorithms.Papers.Independent.Information100.P06 (Below)

open QAlgorithms.Papers.Independent.Information100.P34 (choi)

open QAlgorithms.Papers.Independent.Information100.P62 (Stochastic)

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

open QAlgorithms.Papers.Independent.Information100.P67 (IsSubnormalized purifiedDistance)

open QAlgorithms.Papers.Independent.Information100.P69 (replacer permute)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond channelPower channelRelative)

open QAlgorithms.Papers.Independent.Support50.P39 (quantumMutualInformation)

variable {A B C D R : Type} [Fintype A] [DecidableEq A]
  [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C]
  [Fintype D] [DecidableEq D] [Fintype R] [DecidableEq R]

variable [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] [Nonempty R]

/-- Lemma 13, Eq.(106), PDF p.21: link product of independently wired operations.
The entry formula includes the full resource transpose via trace contraction. -/
theorem wired_choi_link (N : Superop B C) (hN : IsChannel N)
    (P : Superop (A × C) (B × D)) (hP : BipartiteNSOperation P) :
    choi (wire N P) = linkChoi (choi N) (choi P) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P65

end

Source

Quantum Channel Simulation and the Channel's Smooth Max-Information, arXiv:1807.05354v2, PDF p. 21, Lemma 13 / Eq.(106): Choi link product for a wired code

Read-back

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

For finite index types $A,B,C,D$ , equipped with decidable equality, let $N$ map complex matrices on $B$ to complex matrices on $C$ , and let $P$ map complex matrices on $A\times C$ to complex matrices on $B\times D$ . Assume both are channels: each admits a finite Kraus representation $X\mapsto\sum_j K_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ , valid for every input matrix $X$ . Assume additionally that there are channels $F:A\to B$ and $G:C\to D$ such that, for every matrix $X$ on $A\times C$ , $\operatorname{Tr}_D P(X)=F(\operatorname{Tr}_C X)$ and $\operatorname{Tr}_B P(X)=G(\operatorname{Tr}_A X)$ . Write $E_{ij}$ for the matrix unit and define the unnormalized Choi matrix of a map $T$ by $J_T((i,o),(j,o'))=T(E_{ij})_{o,o'}$ . Define the wired map $W:A\to D$ on every matrix $X$ by

W(X)_{d,d'}=\sum_{b,b'\in B}\sum_{c,c'\in C} N(E_{bb'})_{c,c'}\,P(X\otimes E_{cc'})_{(b,d),(b',d')}.

Then its Choi matrix is the linked matrix specified entrywise by

J_W((a,d),(a',d'))= \sum_{b,b'\in B}\sum_{c,c'\in C} J_N((b,c),(b',c'))\, J_P(((a,c),(b,d)),((a',c'),(b',d')).

All sums run over the entire indicated finite index types, with empty sums interpreted as zero.

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