Theorem 11: the complement itself approximately degrades a low-noise channel

Open

QAlgorithms.Papers.Independent.Intakethird100.P50.complement_approximately_degrades

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

prove2quantum

Let $N:A\to A$ be a quantum channel on a nonzero finite-dimensional system, and fix any isometric dilation and its full complement $N^c$ . If $0\le\varepsilon\le2$ and $\|N-\mathrm{id}_A\|_\diamond\le\varepsilon$ , then the specified degrading map $N^c$ satisfies

\|N^c-N^c\circ N\|_\diamond\le2\varepsilon^{3/2}.

This retains the constructive approximate degrader, including the exact zero-noise endpoint. It is the explicit norm inequality on the full stated parameter interval.

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)

/-- Theorem 11, PDF p.11: the SPECIFIED degrader is N^c itself. The norm bound
holds on the full [0,2] interval; no inadmissible degradability parameter is introduced. -/
theorem complement_approximately_degrades [Nonempty A] [Nonempty E]
    (V : Matrix (A × E) A ℂ) (hV : IsIsometry V)
    (eps : ℝ) (heps : eps ∈ Set.Icc 0 2)
    (hclose : diamond (channelDifference (receiverChannel V) id) ≤ eps) :
    diamond (channelDifference (complementaryChannel V) (complementaryChannel V ∘ receiverChannel V)) ≤
      2 * eps ^ (3 / 2 : ℝ) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P50

end

Source

Quantum and private capacities of low-noise channels, arXiv:1705.04335v3, PDF p. 11, Theorem 11: the complement itself approximately degrades a low-noise channel

Read-back

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

For finite nonempty types $A,E$ equipped with decidable equality, let $V:A\times E\leftarrow A$ be a complex matrix with $V^\dagger V=I_A$ , and put

N(\rho)=\operatorname{Tr}_E(V\rho V^\dagger), \qquad N^c(\rho)=\operatorname{Tr}_A(V\rho V^\dagger).

For every real $0\le\varepsilon\le2$ , if $\|N-\mathrm{id}\|_\diamond\le\varepsilon$ , then

\|N^c-N^c\circ N\|_\diamond\le2\varepsilon^{3/2}.

For either map, the diamond quantity is the real supremum of $\|(\mathrm{id}_A\otimes\Phi)(X)\|_1$ over all complex matrices $X$ on $A\times A$ with $\|X\|_1\le1$ ; amplification applies $\Phi$ to each reference matrix block, and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . The exponent $3/2$ is a real exponent. Both endpoints are included, so at $\varepsilon=0$ the asserted diamond quantity is at most 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