Example 3 / Eqs.(62),(63): amplitude-damping zero-error cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.damping_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.

For $0\le r\le1$ , let $\mathcal N_r$ be the qubit channel with Kraus matrices $E_0=|0\rangle\langle0|+\sqrt{1-r}|1\rangle\langle1|$ and $E_1=\sqrt r|0\rangle\langle1|$ . Then

S_{\rm NS,0}(\mathcal N_r)=\tfrac12\log_2\bigl(2(1+\sqrt{1-r})-r\bigr).

The subtraction of $r$ is outside the factor two. The regularized zero-error cost is one qubit at $r=0$ and zero at $r=1$ .

The matrices $V=(1+\sqrt{1-r})|0\rangle\langle0|+(\sqrt{1-r}+1-r)|1\rangle\langle1|$ and $X=(|00\rangle+|11\rangle)(\langle00|+\langle11|)$ satisfy the primal and dual constraints in Eqs.(57),(58), and both objective values equal the independently defined minimum $t_0(\mathcal N_r)$ . Thus the displayed witnesses in Eq.(62) 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 3, Eqs.(62)--(63), PDF p.14: -r is outside the factor 2.
The displayed primal optimizer and unnormalized plus-Bell dual optimizer are
feasible and attain the independently defined zero-error trace optimum. -/
theorem damping_zeroError (r : ℝ) (h0 : 0 ≤ r) (h1 : r ≤ 1) :
    zeroErrorCost (damping r) = Real.logb 2 (2*(1 + Real.sqrt (1-r)) - r) / 2 ∧
    ZeroErrorWitnessPair (damping r) (dampingPrimalWitness r)
      (choi (fun X : Mat Bool => 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 3 / Eqs.(62),(63): amplitude-damping zero-error cost

Read-back

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

For every real $r$ satisfying $0\le r\le1$ , let $Q=\{\mathrm{false},\mathrm{true}\}$ , ordered in that order, and define the map $D_r$ by

D_r(Y)=K_0YK_0^\dagger+K_1YK_1^\dagger,\qquad K_0=\begin{pmatrix}1&0\\0&\sqrt{1-r}\end{pmatrix},\qquad K_1=\begin{pmatrix}0&\sqrt r\\0&0\end{pmatrix}.

The theorem asserts

C_0(D_r)=\frac12\log_2\!\left(2(1+\sqrt{1-r})-r\right)

and the matrix certificate specified below. To define $C_0(D_r)$ , a channel means a map $Y\mapsto\sum_jL_jYL_j^\dagger$ for a finite family satisfying $\sum_jL_j^\dagger L_j=I$ ; for every natural $n$ , define $D_r^{[n]}$ on matrix units by

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

For each positive integer $m$ , range over channels $P$ from matrices on $Q^n\times\{0,\ldots,m-1\}$ to matrices on $\{0,\ldots,m-1\}\times Q^n$ for which there exist channels $F:Q^n\to\{0,\ldots,m-1\}$ and $G:\{0,\ldots,m-1\}\to Q^n$ such that, for every matrix $Y$ ,

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

Define

W_P(Y)(b,b')=\sum_{u,v=0}^{m-1}P(Y\otimes E_{uv})((u,b),(v,b')), \qquad e_n(m)=\inf_P\frac12\sup_{\|Z\|_1\le1} \left\|(\operatorname{id}_{Q^n}\otimes(W_P-D_r^{[n]}))(Z)\right\|_1.

Here $Z$ is any complex matrix on $Q^n\times Q^n$ , amplification applies the map to each reference-indexed block, and $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ . With $c_n=\inf\{\log_2m:m\in\mathbb N,\ m>0,\ e_n(m)\le0\}$ , the cost is

C_0(D_r)=\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\}.

The condition $e_n(m)\le0$ is a condition on an infimum and does not require an attaining $P$ . For the certificate, let $J_{D_r}((a,b),(a',b'))=D_r(E_{aa'})(b,b')$ , let $J_{\mathrm{id}}((a,b),(a',b'))$ equal $1$ when $a=b$ and $a'=b'$ and $0$ otherwise, and set

V=\operatorname{diag}(1+\sqrt{1-r},\,\sqrt{1-r}+1-r),\qquad z(D_r)=\inf\{\operatorname{Re}\operatorname{tr}W:W=W^\dagger,\ I_Q\otimes W-J_{D_r}\succeq0\}.

The asserted certificate is

V=V^\dagger,\quad I_Q\otimes V-J_{D_r}\succeq0,\quad J_{\mathrm{id}}\succeq0,\quad I_Q-\operatorname{tr}_QJ_{\mathrm{id}}\succeq0,\quad \operatorname{Re}\operatorname{tr}V=z(D_r),\quad \operatorname{Re}\operatorname{tr}(J_{D_r}J_{\mathrm{id}})=z(D_r).

The endpoints $r=0$ and $r=1$ are included; all infima above are total real infima, taking value $0$ for empty or unbounded-below sets.

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