Eq.(41): operational capacity/simulation-cost ordering

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.operational_ordering

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.

For a CPTP channel $\mathcal N$ , write $Q_E,Q_{\rm NS}$ for operational quantum capacities with entanglement and NS assistance, and $S_E,S_{\rm NS}$ for the corresponding operational simulation costs. All are vanishing-error rates of noiseless quantum dimensions. Then

Q_E(\mathcal N)\le Q_{\rm NS}(\mathcal N)\le S_{\rm NS}(\mathcal N)\le S_E(\mathcal N).

The four quantities are independently defined using communication or simulation codes, and entanglement assistance is implemented by local maps and a shared density matrix.

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]

/-- Eq.(41), PDF p.10: all four operational quantities and all three inequalities. -/
theorem operational_ordering (N : Superop A B) (hN : IsChannel N) :
    vanishingErrorQuantumCapacity .ent N ≤ vanishingErrorQuantumCapacity .ns N ∧ vanishingErrorQuantumCapacity .ns N ≤ vanishingErrorSimulationCost .ns N ∧
    vanishingErrorSimulationCost .ns N ≤ vanishingErrorSimulationCost .ent N := 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, Eq.(41): operational capacity/simulation-cost ordering

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{ent}}(N)\le Q_{\mathrm{ns}}(N) \le C_{\mathrm{ns}}(N)\le C_{\mathrm{ent}}(N),

where a channel is a finite Kraus sum with $\sum_iK_i^\dagger K_i=I$ , and the four extended-real quantities are defined as follows. For assistance $o$ , let $E_o(F,G)$ be the real infimum of $\tfrac12\|\mathcal W_F(P)-G\|_\diamond$ over permitted maps $P:X\times V\to U\times Y$ , when $F:U\to V$ , $G:X\to Y$ , and

\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')}.

For nonsignalling assistance, $P$ must be a channel and there must be channels $P_A:X\to U$ , $P_B:V\to Y$ satisfying $\operatorname{Tr}_Y P(Z)=P_A(\operatorname{Tr}_V Z)$ and $\operatorname{Tr}_U P(Z)=P_B(\operatorname{Tr}_X Z)$ for every matrix $Z$ . For entanglement assistance, there must be positive integers $e,f$ , a density matrix $\eta$ on $\mathbb C^e\otimes\mathbb C^f$ , and channels $E:X\times\{0,\ldots,e-1\}\to U$ , $F':V\times\{0,\ldots,f-1\}\to Y$ such that

P(Z)_{(b,d),(b',d')} =\sum_{i,j,u,v,a,c,s,t} Z_{(i,u),(j,v)}\,\eta_{(a,s),(c,t)} E(|i,a\rangle\langle j,c|)_{b,b'} F'(|u,s\rangle\langle v,t|)_{d,d'}.

Density means positive semidefinite with trace $1$ . The diamond norm uses all matrices of trace norm at most $1$ on an input-sized reference tensor the input, with $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . For $o\in\{\mathrm{ent},\mathrm{ns}\}$ , $Q_o(N)$ is the extended-real supremum of nonnegative real $r$ such that, for every $e>0$ and $s>0$ , eventually every positive integer $n$ admits $m>0$ with $E_o(N^{\otimes n},\mathrm{id}_m)\le e$ and $(r-s)n\le\log_2m$ ; $C_o(N)$ is the extended-real infimum of nonnegative real $r$ such that the same quantifiers admit $m>0$ with $E_o(\mathrm{id}_m,N^{\otimes n})\le e$ and $\log_2m\le(r+s)n$ . Tensor powers are defined by $(N^{\otimes n}(Z))_{y,z}=\sum_{x,x'}Z_{x,x'}\prod_iN(|x_i\rangle\langle x'_i|)_{y_i,z_i}$ . These definitions bound the infimum error, without asserting attainment by a particular assistance map.

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