§IV.B: quantum reverse Shannon theorem under NS assistance

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.ns_reverse_shannon

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\to B$ be CPTP. Let $Q_{\rm NS}$ be the supremum of operational vanishing-error quantum communication rates with NS assistance, and $S_{\rm NS}$ the infimum of operational vanishing-error simulation rates with the same assistance. These rates count the binary logarithm of noiseless resource dimension per channel use. Then

Q_{\rm NS}(\mathcal N)=S_{\rm NS}(\mathcal N)=\tfrac12 I(\mathcal N).

Here $I(\mathcal N)$ is the maximum state mutual information over purified inputs. This is the quantum reverse Shannon theorem under no-signalling assistance.

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]

/-- Section IV.B, PDF pp.10--12: quantum reverse Shannon theorem with NS
assistance. Capacity and simulation cost were defined independently of entropy. -/
theorem ns_reverse_shannon (N : Superop A B) (hN : IsChannel N) :
    vanishingErrorQuantumCapacity .ns N = vanishingErrorSimulationCost .ns N ∧
    vanishingErrorSimulationCost .ns N = ((channelMutualInfo N / 2 : ℝ) : EReal) := 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. 10, §IV.B: quantum reverse Shannon theorem under NS assistance

Read-back

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

For finite index types $A,B$ , with decidable equality, every channel $N:A\to B$ satisfies $Q_{\mathrm{ns}}(N)=C_{\mathrm{ns}}(N)=(C(N)/2:\overline{\mathbb R})$ , with the following definitions. Channels admit finite Kraus representations with $\sum_iK_i^\dagger K_i=I$ . For channels $F:U\to V$ and $G:X\to Y$ , let $E_{\mathrm{ns}}(F,G)$ be the real infimum of $\tfrac12\|\mathcal W_F(P)-G\|_\diamond$ over channels $P:X\times V\to U\times Y$ for which there are channels $P_A:X\to U$ , $P_B:V\to Y$ satisfying both marginal identities $\operatorname{Tr}_Y P(Z)=P_A(\operatorname{Tr}_VZ)$ and $\operatorname{Tr}_U P(Z)=P_B(\operatorname{Tr}_XZ)$ for every matrix $Z$ . Here

\mathcal W_F(P)(Z)_{y,y'} =\sum_{a,c\in U}\sum_{u,v\in V} F(|a\rangle\langle c|)_{u,v} P(Z\otimes|u\rangle\langle v|)_{(a,y),(c,y')},

and the diamond norm is the supremum of the output trace norm over all input matrices of trace norm at most $1$ , using a reference of the same dimension as the input; $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ . Define $Q_{\mathrm{ns}}(N)$ as the extended-real supremum of nonnegative real $r$ such that, for every error tolerance $e>0$ and slack $s>0$ , eventually every positive block length $n$ admits a positive integer $m$ with

E_{\mathrm{ns}}(N^{\otimes n},\mathrm{id}_m)\le e, \qquad (r-s)n\le\log_2m.

Define $C_{\mathrm{ns}}(N)$ as the extended-real infimum of nonnegative real $r$ with the analogous property

E_{\mathrm{ns}}(\mathrm{id}_m,N^{\otimes n})\le e, \qquad \log_2m\le(r+s)n.

The error bounds concern infima over assistance maps and do not themselves assert a realizing map. Tensor powers have entries obtained by summing $X_{x,x'}\prod_iN(|x_i\rangle\langle x'_i|)_{y_i,z_i}$ . Finally,

C(N)=\sup_{\rho\text{ density}} \left[S(\operatorname{Tr}_B R_\rho)+S(\operatorname{Tr}_A R_\rho)-S(R_\rho)\right], \quad R_\rho=(\mathrm{id}_A\otimes N)(|v_\rho\rangle\langle v_\rho|), \quad v_\rho(a,a')=(\sqrt\rho)_{a,a'},

where density means positive semidefinite with trace $1$ , and $S(X)=-\operatorname{Re}\operatorname{tr}\operatorname{cfc}(x\mapsto x\log_2x)(X)$ . Positive block lengths are required only eventually; no condition at block length $0$ enters the rate definitions.

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