Example 4 / Eq.(65): dephasing zero-error cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.dephasing_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 p\le1$ , let $\mathcal Z_p(X)=(1-p)X+pZXZ$ on a qubit, where $Z=\operatorname{diag}(1,-1)$ . Then

S_{\rm NS,0}(\mathcal Z_p)=\tfrac12\log_2(|4p-2|+2).

The formula covers the full probability interval: it is one at either endpoint and one half at $p=1/2$ . The separately erroneous printed dual witness is not assumed.

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 4, Eq.(65), PDF p.14: valid for the full probability range;
the erroneous fixed dual witness in Eq.(64) is not assumed. -/
theorem dephasing_zeroError (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) :
    zeroErrorCost (phaseFlipChannel p) = Real.logb 2 (|4*p-2| + 2) / 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 4 / Eq.(65): dephasing zero-error cost

Read-back

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

For every real $p$ satisfying $0\le p\le1$ , define $\mathcal Z_p(X)=(1-p)X+pZXZ^\dagger$ on the two-dimensional register indexed by $\{\mathrm{false},\mathrm{true}\}$ , where $Z=\operatorname{diag}(1,-1)$ . The assertion is

C_0(\mathcal Z_p)=\frac12\log_2\!\bigl(|4p-2|+2\bigr).

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$ ; the tensor power is defined by multiplying the individual channel matrix-unit entries. The quantity $c_{\mathrm{ns}}(H,e)$ is the real infimum of $\log_2 m$ over positive integers $m$ such that the infimum simulation error using the $m$ -dimensional identity channel is at most $e$ . That 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 two output marginals each depend only on the corresponding input marginal, with $\mathcal W_m(P)(X)_{b,d}=\sum_{a,c<m}P(X\otimes|a\rangle\langle c|)_{(a,b),(c,d)}$ . A channel means a finite Kraus map $X\mapsto\sum_jK_jXK_j^\dagger$ satisfying $\sum_jK_j^\dagger K_j=I$ ; $\|F\|_\diamond=\sup_{\|X\|_1\le1}\|(\mathrm{id}_I\otimes F)(X)\|_1$ , over arbitrary matrices on $I\times I$ , and $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ . Thus the zero-tolerance condition concerns an infimum rather than an explicitly attained exact simulation. The assertion includes $p=0,\tfrac12,1$ ; real infima take value $0$ on empty sets or sets unbounded below.

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