Appendix A / LP (69): classical-channel one-shot simulation

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.classical_oneShot_lp

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 $W(y|x)$ be a finite stochastic channel, with nonempty input and output alphabets, and $\varepsilon\ge0$ . Embed it as the quantum map $X\mapsto\sum_{x,y}W(y|x)X_{xx}|y\rangle\langle y|$ . Let $t_\varepsilon$ be the infimum of $\sum_yV_y$ over real arrays $Y_{xy},T(y|x),V_y$ satisfying $Y_{xy}\ge T(y|x)-W(y|x)$ , $Y_{xy}\ge0$ , $T(y|x)\ge0$ , $\sum_yT(y|x)=1$ , $T(y|x)\le V_y$ , and $\sum_yY_{xy}\le\varepsilon$ for every input $x$ . Then

S_{\rm NS,\varepsilon}^{(1)}(W)=\log_2\lceil\sqrt{t_\varepsilon}\rceil.

The linear optimum is attained. The resource is quantum communication even though the target is classical.

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]

/-- Appendix A, LP (69), PDF p.18: quantum-resource cost for a classical target.
The linear optimum is attained, and every error constraint is per input. -/
theorem classical_oneShot_lp (W : A → B → ℝ) (hW : Stochastic (fun y x => W x y)) (e : ℝ) (he : 0 ≤ e) :
    oneUseSimulationCost .ns (classicalMap W) e = roundedTraceCost (classicalValue W e) ∧
    ∃ Y T : A → B → ℝ, ∃ V : B → ℝ,
      classicalFeasible W e Y T V ∧ (∑ y, V y) = classicalValue W e := 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. 18, Appendix A / LP (69): classical-channel one-shot simulation

Read-back

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

For finite types $A,B$ with decidable equality, every function $W:A\times B\to\mathbb R$ satisfying $W(x,y)\ge0$ and $\sum_yW(x,y)=1$ for every $x$ , and every real $e\ge0$ , define $\mathcal W(X)=\operatorname{diag}_y(\sum_xW(x,y)X_{x,x})$ . Let $v_e$ be the real infimum of $\sum_yV(y)$ over real arrays $Y,T:A\times B\to\mathbb R$ and $V:B\to\mathbb R$ satisfying

T(x,y)-W(x,y)\le Y(x,y),\quad 0\le Y(x,y),\quad 0\le T(x,y)\le V(y),\quad \sum_yT(x,y)=1,\quad \sum_yY(x,y)\le e.

Then $c_{\mathrm{ns}}(\mathcal W,e)=\log_2\lceil\sqrt{v_e}\rceil$ , and there exist such $Y,T,V$ with $\sum_yV(y)=v_e$ . Here $c_{\mathrm{ns}}(H,e)$ is the real infimum of $\log_2 m$ over positive integers $m$ for which the infimum of $\tfrac12\|\mathcal W_m(P)-H\|_\diamond$ is at most $e$ , with the latter infimum over channels $P:\operatorname{Mat}(A\times\{0,\ldots,m-1\})\to\operatorname{Mat}(\{0,\ldots,m-1\}\times B)$ whose output marginals each depend only on the corresponding input marginal; $\mathcal W_m(P)(X)_{b,d}=\sum_{a,c<m}P(X\otimes|a\rangle\langle c|)_{(a,b),(c,d)}$ . A channel is a finite Kraus map with $\sum_jK_j^\dagger K_j=I$ , and $\|F\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_A\otimes F)(X)\|_1$ , over arbitrary matrices on $A\times A$ , where $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . The ceiling is the natural-number ceiling. There is no upper bound on $e$ ; $e=0$ is included. Empty finite types are not explicitly excluded: if $A\ne\varnothing$ and $B=\varnothing$ , the stochasticity hypothesis is impossible. Real infima use value $0$ when empty or unbounded below, $\sqrt{x}=0$ for $x<0$ , and $\log_2 0=0$ .

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