Theorem 6 / Eq.(32): exact one-shot operational interpretation

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.oneShot_operational

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 a quantum channel and $\varepsilon\ge0$ . Write $I_{\max}^\varepsilon(\mathcal N)$ for the infimum of the channel max-information over CPTP maps $\widetilde{\mathcal N}:A'\to B$ with $\frac12\|\widetilde{\mathcal N}-\mathcal N\|_\diamond\le\varepsilon$ . Let $S_{\mathrm{NS},\varepsilon}^{(1)}$ be the minimum binary logarithm of an integer noiseless resource dimension, using one channel use and a bipartite CPTP code that is no-signalling in both directions. Then

S_{\mathrm{NS},\varepsilon}^{(1)}(\mathcal N)=\log_2\left\lceil 2^{I_{\max}^\varepsilon(\mathcal N)/2}\right\rceil=\tfrac12I_{\max}^\varepsilon(\mathcal N)+\delta.

Here $\delta=\log_2\lceil2^{I_{\max}^\varepsilon(\mathcal N)/2}\rceil-I_{\max}^\varepsilon(\mathcal N)/2$ belongs to $[0,1]$ and is the least nonnegative correction that makes the right-hand side the logarithm of a positive integer. This is the exact one-shot operational interpretation, including zero error and tolerances at least one.

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]

/-- Theorem 6, Eq.(32), PDF pp.8--9; ceiling form in Remark 4, p.9.
The rounding correction is computed and is the least nonnegative one. -/
theorem oneShot_operational (N : Superop A B) (hN : IsChannel N) (e : ℝ) (he : 0 ≤ e) :
    oneUseSimulationCost .ns N e = roundedInfoCost (smoothChannelInfo N e) ∧
    oneUseSimulationCost .ns N e = smoothChannelInfo N e / 2 + roundingCorrection (smoothChannelInfo N e) ∧
    0 ≤ roundingCorrection (smoothChannelInfo N e) ∧
    roundingCorrection (smoothChannelInfo N e) ≤ 1 ∧
    (∀ delta : ℝ, 0 ≤ delta →
      (∃ m : ℕ, 0 < m ∧ smoothChannelInfo N e / 2 + delta = Real.logb 2 m) →
      roundingCorrection (smoothChannelInfo N e) ≤ delta) := 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. 8, Theorem 6 / Eq.(32): exact one-shot operational interpretation

Read-back

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

For finite register types $A,B$ with decidable equality, every channel $N$ from matrices on $A$ to matrices on $B$ , meaning a map $N(X)=\sum_jK_jXK_j^\dagger$ for finitely many matrices with $\sum_jK_j^\dagger K_j=I_A$ , and every real $e\ge0$ , the following assertions hold. To specify the quantities, write

\|X\|_1=\operatorname{ReTr}\sqrt{X^\dagger X}, \qquad d_\diamond(F,G)=\frac12 \sup_{\|X\|_1\le1} \left\|(\operatorname{id}_A\otimes(F-G))(X)\right\|_1,

where $X$ ranges over all complex matrices on $A\times A$ , the amplification acts blockwise, and matrix square roots use continuous functional calculus. For each positive integer $m$ , let $\mathcal P_m$ consist of channels $P:A\times\{0,\ldots,m-1\}\to\{0,\ldots,m-1\}\times B$ for which there exist channels $F:A\to\{0,\ldots,m-1\}$ and $G:\{0,\ldots,m-1\}\to B$ such that, for every matrix $X$ ,

\operatorname{Tr}_{B}P(X)=F(\operatorname{Tr}_{\mathrm{second}}X), \qquad \operatorname{Tr}_{\mathrm{first}}P(X)=G(\operatorname{Tr}_{A}X).

Every channel here has the same finite Kraus meaning. For $P\in\mathcal P_m$ , define

W_P(X)(b,b')= \sum_{a,c=0}^{m-1} P(X\otimes E_{a,c})((a,b),(c,b')), \quad E_m=\inf_{P\in\mathcal P_m}d_\diamond(W_P,N), \quad K_e=\inf_{\substack{m\ge1\\ E_m\le e}}\log_2m.

Thus the condition defining $K_e$ bounds an infimum of simulation errors; it does not itself assert an error-attaining code. Next, for a matrix $Z$ on $A\times B$ , put

I_{\max}(Z)= \inf_{\substack{\omega\succeq0\\ \operatorname{Tr}\omega=1}} \inf\{\lambda\in\mathbb R: 2^\lambda(Z_A\otimes\omega)-Z\succeq0\}, \qquad Z_A=\operatorname{Tr}_B Z,

where these infima are extended-real. Let

\Phi_A((a,a'),(c,c'))= \begin{cases} |A|^{-1},&a=a'\text{ and }c=c',\\ 0,&\text{otherwise}, \end{cases} \qquad C_e=\inf_{\substack{M\ \mathrm{channel}\\d_\diamond(M,N)\le e}} \left(I_{\max}\bigl((\operatorname{id}_A\otimes M)(\Phi_A)\bigr)\right)_{\mathbb R}.

The subscript $\mathbb R$ sends finite extended-real values to their real values and sends both infinities to zero. Define $J(x)=\log_2\lceil2^{x/2}\rceil$ and $c(x)=J(x)-x/2$ , with the ceiling taking values in the natural numbers. The theorem asserts

K_e=J(C_e),\qquad K_e=\frac{C_e}{2}+c(C_e),\qquad 0\le c(C_e)\le1,

and, for every real $\delta\ge0$ ,

\left(\exists m\in\mathbb N,\ m>0,\ \frac{C_e}{2}+\delta=\log_2m\right) \ \Longrightarrow\ c(C_e)\le\delta.

There is no upper bound on $e$ and no explicit nonemptiness assumption on the register types. Real infima and suprema use their totalized real-valued definitions, giving zero for empty or appropriately unbounded sets; extended-real empty infima are $+\infty$ . Reciprocals of zero and $\log_2 0$ are 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