Eqs.(19),(20),(30), Remark 1: zero-error cost and regularization

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.zeroError_characterization

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 and $t_0(\mathcal N)=\inf\{\operatorname{Tr}V_B:J_{\mathcal N}\le I_A\otimes V_B\}$ , with Hermitian $V_B$ . Then

S_{\rm NS,0}^{(1)}(\mathcal N)=\log_2\lceil\sqrt{t_0(\mathcal N)}\rceil=\tfrac12 I_{\max}(\mathcal N)+\delta,

\lim_{n\to\infty}\frac1n S_{\rm NS,0}^{(1)}(\mathcal N^{\otimes n})=S_{\rm NS,0}(\mathcal N)=\tfrac12\log_2t_0(\mathcal N)=\tfrac12I_{\max}(\mathcal N).

Here $\delta$ is the computed integer-rounding correction. Zero error is fixed before blocklength tends to infinity. The convergence is asserted, and the regularized quantity is defined through operational zero-error rates.

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]

/-- Eqs.(19),(20),(30) and Remark 1, PDF pp.7--8. Zero error is imposed
before n tends to infinity; the rounded one-shot and regularized costs differ. -/
theorem zeroError_characterization (N : Superop A B) (hN : IsChannel N) :
    oneUseSimulationCost .ns N 0 = roundedTraceCost (zeroTraceValue N) ∧
    oneUseSimulationCost .ns N 0 = channelInfo N / 2 + roundingCorrection (channelInfo N) ∧
    zeroErrorCost N = Real.logb 2 (zeroTraceValue N) / 2 ∧
    zeroErrorCost N = channelInfo N / 2 ∧
    Tendsto (fun n : ℕ => oneUseSimulationCost .ns (channelPower N (n+1)) 0 / (n+1))
      atTop (nhds (zeroErrorCost 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. 7, Eqs.(19),(20),(30), Remark 1: zero-error cost and regularization

Read-back

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

For finite index types $A,B$ , with decidable equality, let $N:A\to B$ be a channel, meaning a finite Kraus sum with $\sum_iK_i^\dagger K_i=I_A$ . Write $J_N((a,b),(a',b'))=N(|a\rangle\langle a'|)_{b,b'}$ , and define

t_0=\inf\{\operatorname{Re}\operatorname{tr}V: V=V^\dagger,\ I_A\otimes V-J_N\ge0\}.

For positive $m$ , define $E_m(N)$ as the infimum of $\tfrac12\|\mathcal W(P)-N\|_\diamond$ over nonsignalling channels $P:A\times\{0,\ldots,m-1\}\to\{0,\ldots,m-1\}\times B$ , where nonsignalling requires both output marginals to be channel functions of their respective input marginals on every matrix, and $\mathcal W(P)(X)_{b,b'}=\sum_{u,v}P(X\otimes|u\rangle\langle v|)_{(u,b),(v,b')}$ . Set $C_1(N)=\inf\{\log_2m:m>0,\ E_m(N)\le0\}$ . The diamond expression uses all matrices on an input-sized reference tensor the input, with trace norm $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . Define $D_{\max}(R\|S)=\inf\{\lambda\in\mathbb R:2^\lambda S-R\ge0\}$ , taking this infimum in the extended reals, and

I_{\max}(R)=\inf_{\substack{\sigma\ge0\\\operatorname{tr}\sigma=1}} D_{\max}(R\|(\operatorname{Tr}_B R)\otimes\sigma),\qquad I(N)=\left(I_{\max}((\mathrm{id}_A\otimes N)(\Phi_A))\right)_{\mathrm{toReal}},

where $(\Phi_A)_{(a,a'),(b,b')}=|A|^{-1}$ when $a=a'$ and $b=b'$ , and is $0$ otherwise; extended-real conversion sends either infinity to $0$ . Define $R(x)=\log_2\lceil2^{x/2}\rceil_{\mathbb N}-x/2$ , and let $C_0(N)$ be the infimum of real $r$ such that, for every $s>0$ , eventually for every positive integer $n$ , $C_1(N^{\otimes n})/n\le r+s$ . The tensor power acts by

(N^{\otimes n}(X))_{y,z} =\sum_{x,x'}X_{x,x'}\prod_{i=0}^{n-1} N(|x_i\rangle\langle x'_i|)_{y_i,z_i}.

The declaration asserts all of

C_1(N)=\log_2\lceil\sqrt{t_0}\rceil_{\mathbb N} =\frac{I(N)}2+R(I(N)),\qquad C_0(N)=\frac{\log_2t_0}{2}=\frac{I(N)}2, \qquad \lim_{n\to\infty}\frac{C_1(N^{\otimes(n+1)})}{n+1}=C_0(N).

Only positive block lengths occur in these asymptotic assertions; the real logarithm and divisions remain total.

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