Proposition 3 / Eqs.(17),(18): one-shot cost from an SDP

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.oneShot_trace_sdp

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:A\to B$ and $\varepsilon\ge0$ , let $t_\varepsilon(\mathcal N)$ be the infimum of $\operatorname{Tr}V_B$ over Hermitian $Y,J,V_B$ with $\operatorname{Tr}_B Y\le\varepsilon I_A$ , $Y\ge J-J_{\mathcal N}$ , $Y\ge0$ , $J\ge0$ , $\operatorname{Tr}_B J=I_A$ , and $J\le I_A\otimes V_B$ . Then

S_{\rm NS,\varepsilon}^{(1)}(\mathcal N)=\log_2\left\lceil\sqrt{t_\varepsilon(\mathcal N)}\right\rceil.

The trace infimum is attained by a feasible triple. Integer resource rounding is applied after optimizing the linear objective; the communication cost is its logarithmic postprocessing.

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]

/-- Proposition 3, Eqs.(17)--(18), PDF p.6. The trace SDP optimum is attained;
root/ceiling/log are subsequent scalar operations. -/
theorem oneShot_trace_sdp (N : Superop A B) (hN : IsChannel N) (e : ℝ) (he : 0 ≤ e) :
    oneUseSimulationCost .ns N e = roundedTraceCost (traceValue N e) ∧
    ∃ Y J : Mat (A × B), ∃ V : Mat B,
      traceFeasible N e Y J V ∧ V.trace.re = traceValue N 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. 6, Proposition 3 / Eqs.(17),(18): one-shot cost from an SDP

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$ and every real $e\ge0$ satisfy the following equality and attainment statement. A channel here admits a finite Kraus representation $X\mapsto\sum_iK_iXK_i^\dagger$ with $\sum_iK_i^\dagger K_i=I$ . For each positive integer $m$ , let $E_m(N)$ be the infimum of $\tfrac12\|\mathcal W(P)-N\|_\diamond$ over channels $P:A\times\{0,\ldots,m-1\}\to\{0,\ldots,m-1\}\times B$ whose output marginals depend only on the respective input marginals, through channels, on every matrix, where

\mathcal W(P)(X)_{b,b'} =\sum_{u,v=0}^{m-1}P(X\otimes|u\rangle\langle v|)_{(u,b),(v,b')}.

Here $\|\Delta\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_A\otimes\Delta)(X)\|_1$ , over all matrices $X$ on $A\times A$ , and $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . Let $t_e$ be the real infimum of $\operatorname{Re}\operatorname{tr}V$ over matrices $Y,J$ on $A\times B$ and Hermitian matrices $V$ on $B$ satisfying

Y\ge0,\quad eI_A-\operatorname{Tr}_B Y\ge0,\quad Y-J+J_N\ge0,\quad J\ge0,\quad \operatorname{Tr}_B J=I_A,\quad I_A\otimes V-J\ge0,

where $J_N((a,b),(a',b'))=N(|a\rangle\langle a'|)_{b,b'}$ , and partial traces sum matching indices. Then

\inf_{\substack{m\in\mathbb N,\ m>0\\E_m(N)\le e}}\log_2m =\log_2\left\lceil\sqrt{t_e}\right\rceil_{\mathbb N},

and there exist $Y,J,V$ satisfying exactly these constraints with $\operatorname{Re}\operatorname{tr}V=t_e$ . The hypothesis allows $e\ge1$ . The ceiling is the natural-number ceiling; real square root and logarithm retain their total definitions, so square root of a nonpositive number is $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