Example 2 / Eqs.(59)–(61): depolarizing zero-error cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.depolarizing_zeroError

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 $d\ge1$ be the dimension of a system and $0\le p\le1$ . Extend the depolarizing channel linearly by $\mathcal D_p(X)=(1-p)X+p\operatorname{Tr}(X)I_d/d$ . Its regularized zero-error NS simulation cost is

S_{\rm NS,0}(\mathcal D_p)=\tfrac12\log_2(d^2(1-p)+p).

This is not the rounded one-shot cost. It equals $\log_2d$ at $p=0$ and zero at $p=1$ or $d=1$ .

The explicit matrices $V=(d(1-p)+p/d)I$ and $X=\sum_{i,j}|ii\rangle\langle jj|$ satisfy the primal and dual constraints in Eqs.(57),(58), and both objective values equal the independently defined minimum $t_0(\mathcal D_p)$ . Thus both displayed witnesses in Eq.(59) are optimal.

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]

/-- Example 2, Eqs.(59)--(61), PDF pp.13--14: noise probability p in [0,1],
including d=1. This is the regularized zero-error cost. The explicit primal and
dual optimizers in Eq.(59) are retained with their common optimal objective. -/
theorem depolarizing_zeroError (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) :
    zeroErrorCost (basisDepolarizing A p) =
      Real.logb 2 ((Fintype.card A : ℝ)^2 * (1-p) + p) / 2 ∧
    ZeroErrorWitnessPair (basisDepolarizing A p) (depolarizingPrimalWitness A p)
      (choi (fun X : Mat A => X)) := 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. 14, Example 2 / Eqs.(59)–(61): depolarizing zero-error cost

Read-back

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

For a finite type $A$ with decidable equality and every real $p$ satisfying $0\le p\le1$ , put $d=|A|$ and define

N(Y)=(1-p)Y+\frac{p\,\operatorname{tr}Y}{d}I_A.

The theorem asserts

C_0(N)=\frac12\log_2\!\left(d^2(1-p)+p\right)

and the matrix certificate specified below. Here $C_0(N)$ is defined as follows, including its nested infima: a channel is any map admitting a finite representation $Y\mapsto\sum_jK_jYK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ ; for each natural number $n$ , let $N^{[n]}$ act on matrix units by

N^{[n]}(E_{xx'})(y,y')=\prod_{i=0}^{n-1}N(E_{x_i x'_i})(y_i,y'_i), \qquad x,x',y,y'\in A^n.

For each positive integer $m$ , consider channels $P$ from matrices on $A^n\times\{0,\ldots,m-1\}$ to matrices on $\{0,\ldots,m-1\}\times A^n$ for which there exist channels $F:A^n\to\{0,\ldots,m-1\}$ and $G:\{0,\ldots,m-1\}\to A^n$ satisfying, for every input matrix $Y$ ,

\operatorname{tr}_{A^n}(P(Y))=F(\operatorname{tr}_{\{0,\ldots,m-1\}}Y), \qquad \operatorname{tr}_{\{0,\ldots,m-1\}}(P(Y))=G(\operatorname{tr}_{A^n}Y).

Such a $P$ , wired to the identity map on the $m$ -dimensional register, induces

W_P(Y)(b,b')=\sum_{u,v=0}^{m-1}P(Y\otimes E_{uv})((u,b),(v,b')).

Let $e_n(m)$ be the infimum over these $P$ of

\frac12\sup_{\|Z\|_1\le1} \left\|(\operatorname{id}_{A^n}\otimes(W_P-N^{[n]}))(Z)\right\|_1,

where $Z$ ranges over all complex matrices on $A^n\times A^n$ , the amplified map applies the indicated map to each reference-indexed block, and $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ . Set $c_n=\inf\{\log_2m:m\in\mathbb N,\ m>0,\ e_n(m)\le0\}$ ; then

C_0(N)=\inf\left\{s\in\mathbb R: \forall\delta>0\ \exists n_0\in\mathbb N\ \forall n\ge n_0,\ n>0\Rightarrow \frac{c_n}{n}\le s+\delta\right\}.

In particular, the condition defining $c_n$ concerns the infimum error and does not itself require an attaining code. For the asserted certificate, define $J_N((a,b),(a',b'))=N(E_{aa'})(b,b')$ , let $J_{\mathrm{id}}((a,b),(a',b'))$ equal $1$ when $a=b$ and $a'=b'$ and $0$ otherwise, and put $V=(d(1-p)+p/d)I_A$ and

z(N)=\inf\{\operatorname{Re}\operatorname{tr}W:W=W^\dagger,\ I_A\otimes W-J_N\succeq0\}.

The certificate asserts

V=V^\dagger,\quad I_A\otimes V-J_N\succeq0,\quad J_{\mathrm{id}}\succeq0,\quad I_A-\operatorname{tr}_A J_{\mathrm{id}}\succeq0,\quad \operatorname{Re}\operatorname{tr}V=z(N),\quad \operatorname{Re}\operatorname{tr}(J_NJ_{\mathrm{id}})=z(N).

Both endpoints $p=0,1$ are included. No nonemptiness assumption on $A$ is displayed; the formulas use total real arithmetic, with division by $0$ and $\log_2 0$ equal to $0$ , and real infima of empty or unbounded-below sets equal to $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