Corollary 4: nearby channels admit nearby complementary channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.complementaryChannels_close

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

prove2quantum

Let $N_1,N_2:\mathcal B(A)\to\mathcal B(B)$ be finite-dimensional quantum channels with $\|N_1-N_2\|_\diamond\le\varepsilon$ and $0\le\varepsilon\le2$ . For every isometric dilation $V_1:A\to B\otimes E_1$ of $N_1$ , there exist a nonzero finite-dimensional common environment $F$ , an isometry $J:E_1\to F$ and an isometric dilation $V_2:A\to B\otimes F$ of $N_2$ such that

\|J N_1^c(\,\cdot\,)J^\dagger-N_2^c\|_\diamond\le2\sqrt\varepsilon.

Both complements use the displayed receiver dilations. Enlarging the first environment realizes the paper's equivalence-under-isometry convention without assuming equal minimal Choi ranks.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P50

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P50

variable {A B E F : Type}

variable [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B]

variable [Fintype E] [DecidableEq E] [Fintype F] [DecidableEq F]

open QAlgorithms.Papers.Independent.Information100.P67
  (IsIsometry receiverChannel complementaryChannel maximumCoherentInformation
    dilationPower idealJoint)

open QAlgorithms.Papers.Independent.Information100.P80 (log2)

open QAlgorithms.Papers.Independent.Information100.P69 (diamond choi)

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

open QAlgorithms.Papers.Independent.Frontier18.P17 (clock)

/-- Corollary 4, PDF p.6, with the isometric-equivalence convention of PDF p.4.
FOR ANY first complement, embed its environment into a common larger finite space,
then choose the second complement there. -/
theorem complementaryChannels_close [Nonempty A] [Nonempty B] [Nonempty E]
    (V1 : Matrix (B × E) A ℂ) (hV1 : IsIsometry V1)
    (N2 : Superop A B) (hN2 : IsChannel N2)
    (eps : ℝ) (heps : eps ∈ Set.Icc 0 2)
    (hclose : diamond (channelDifference (receiverChannel V1) N2) ≤ eps) :
    ∃ k : ℕ, 0 < k ∧ ∃ J : Matrix (Fin k) E ℂ, IsIsometry J ∧
      ∃ V2 : Matrix (B × Fin k) A ℂ, IsIsometry V2 ∧ receiverChannel V2 = N2 ∧
        diamond (channelDifference (conjSuperop J ∘ complementaryChannel V1) (complementaryChannel V2)) ≤
          2 * Real.sqrt eps := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 6, Corollary 4: nearby channels admit nearby complementary channels

Read-back

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

Let $A,B,E$ be finite nonempty types equipped with decidable equality, let $V_1:B\times E\leftarrow A$ be a complex matrix with $V_1^\dagger V_1=I_A$ , and let $N_2$ be a channel from matrices on $A$ to matrices on $B$ , meaning that $N_2(\rho)=\sum_jK_j\rho K_j^\dagger$ for a finite family satisfying $\sum_jK_j^\dagger K_j=I_A$ . For any real $0\le\varepsilon\le2$ , if

\bigl\|\rho\mapsto\operatorname{Tr}_E(V_1\rho V_1^\dagger)-N_2(\rho)\bigr\|_\diamond\le\varepsilon,

then there exist a positive natural number $k$ , a complex matrix $J:\{0,\ldots,k-1\}\leftarrow E$ with $J^\dagger J=I_E$ , and a complex matrix $V_2:B\times\{0,\ldots,k-1\}\leftarrow A$ with $V_2^\dagger V_2=I_A$ , such that $\operatorname{Tr}_{\{0,\ldots,k-1\}}(V_2\rho V_2^\dagger)=N_2(\rho)$ for every complex matrix $\rho$ , and

\bigl\|\rho\mapsto J\,\operatorname{Tr}_B(V_1\rho V_1^\dagger)J^\dagger -\operatorname{Tr}_B(V_2\rho V_2^\dagger)\bigr\|_\diamond \le2\sqrt{\varepsilon}.

For either map, the diamond quantity is the real supremum of the output trace norm after amplification by the identity on an $A$ -indexed reference, over all complex matrices on $A\times A$ of trace norm at most one; amplification acts separately on each reference matrix block, and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . Both endpoints $\varepsilon=0,2$ are included.

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