Example 5 / Eq.(67): erasure zero-error cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.erasure_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 the input dimension be $d\ge1$ , let $0\le p\le1$ , and let $|e\rangle$ be a new orthogonal erasure flag. Extend $\mathcal E_p$ linearly by $\mathcal E_p(X)=(1-p)X+p\operatorname{Tr}(X)|e\rangle\langle e|$ , with the data block embedded in the output. Then

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

This regularized zero-error cost includes complete erasure and dimension one. The extra dummy index in the printed witness is not used.

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 5, Eq.(67), PDF p.14: an orthogonal flag, with the dimension-one
case included. The erroneous extra index in Eq.(66) is not used. -/
theorem erasure_zeroError (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) :
    zeroErrorCost (flaggedErasureChannel A p) =
      Real.logb 2 ((Fintype.card A : ℝ)^2*(1-p) + p) / 2 := 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 5 / Eq.(67): erasure zero-error cost

Read-back

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

For every finite type $A$ with decidable equality and every real $p$ with $0\le p\le1$ , put $d=|A|$ and define $\mathcal E_p:\operatorname{Mat}(A)\to\operatorname{Mat}(A\cup\{\bot\})$ by $\mathcal E_p(X)_{a,b}=(1-p)X_{a,b}$ for $a,b\in A$ , $\mathcal E_p(X)_{\bot,\bot}=p\operatorname{tr}X$ , and zero on the other entries. The assertion is $C_0(\mathcal E_p)=\tfrac12\log_2(d^2(1-p)+p)$ . Here $C_0(T)$ is the real infimum of all $r$ such that, for every $s>0$ , eventually for all positive integers $n$ , $c_{\mathrm{ns}}(T^{\otimes n},0)/n\le r+s$ ; tensor powers act by products of the individual matrix-unit entries. The quantity $c_{\mathrm{ns}}(H,e)$ is the real infimum of $\log_2 m$ over positive integers $m$ whose infimum simulation error is at most $e$ . This error is the infimum of $\tfrac12\|\mathcal W_m(P)-H\|_\diamond$ over channels $P:\operatorname{Mat}(I\times\{0,\ldots,m-1\})\to\operatorname{Mat}(\{0,\ldots,m-1\}\times O)$ whose output marginals each depend only on the corresponding input marginal, where $\mathcal W_m(P)(X)_{b,d}=\sum_{a,c<m}P(X\otimes|a\rangle\langle c|)_{(a,b),(c,d)}$ . Channels have finite Kraus representations with $\sum_jK_j^\dagger K_j=I$ , and $\|F\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_I\otimes F)(X)\|_1$ , over arbitrary matrices on $I\times I$ , with $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . Zero tolerance constrains the infimum error without asserting its attainment. Both endpoints of $p$ are included, and no nonemptiness condition on $A$ is displayed. Real infima use $0$ when empty or unbounded below, 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