Eq.(11), Supplement I: exact qubit PBT number

Open

QAlgorithms.Papers.Independent.Intakethird100.P49.qubit_pbt_number

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For standard qubit PBT with integer $M\ge2$ , put $s_k=(M-1)/2-k$ for $0\le k\le\lfloor(M-1)/2\rfloor$ . The actual depolarizing probability is

\xi_M=\frac{M+2}{3\,2^{M-1}}+\frac13\sum_{k=0}^{\lfloor(M-1)/2\rfloor}\frac{s_k(s_k+1)}{2^{M-4}}\binom Mk\frac{M+2-\sqrt{(M+2)^2-(2s_k+1)^2}}{(M+2)^2-(2s_k+1)^2}.

The powers are real powers, so negative exponents at $M=2,3$ are retained. In particular $\xi_2=(6-\sqrt3)/6$ and $\xi_3=1/2$ . The formula makes the qubit simulation error explicit without assuming an optimized or probabilistic teleportation resource.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P49

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P49

open QAlgorithms Filter

open scoped Matrix ComplexConjugate ComplexOrder BigOperators

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Information100.P63 (Mat tensorPower)

open QAlgorithms.Papers.Independent.Dependency50.P18 (bipartiteTensor)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond AdaptiveTest adaptiveInput adaptiveAccept)

open QAlgorithms.Papers.Independent.Bridge50.P25
  (LOCCOn normalizedChannelChoi TwoWayGenerationCode TwoWayChannelProtocol
   generationCodeError twoWayGenerationCapacity sendChannelRegister StateFunctional
   IsDimensionChangingLOCCMonotone privateStateInPartyOrder)

open QAlgorithms.Papers.Independent.Support50.P07 (amplitudeDampingChannel)

/-- PDF p.3, (11), Supplement I and p.9, (58): exact qubit PBT number.
The two smallest admissible port counts also pin its indexing convention. -/
theorem qubit_pbt_number :
    (∀ M : ℕ, 2 ≤ M → pbtNumber 2 M = qubitNumberFormula M) ∧
    pbtNumber 2 2 = (6-Real.sqrt 3)/6 ∧ pbtNumber 2 3 = 1/2 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P49

end

Source

Fundamental limits to quantum channel discrimination, arXiv:1803.02834v4, PDF p. 3, Eq.(11), Supplement I: exact qubit PBT number

Read-back

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

Define a map $\mathcal P_M$ on complex $2\times2$ matrices using an input qubit and $M$ qubit ports: its signal matrices have entries $S_i[(x,a),(y,b)]=1/2$ when $x=a_i$ , $y=b_i$ , and $a_j=b_j$ for every $j\ne i$ , and have entry zero otherwise; put $S=\sum_iS_i$ , $R=f(S)$ for $f(t)=(\sqrt t)^{-1}$ with $f(0)=0$ , and $Q_i=RS_iR+M^{-1}(I-RSR)$ . On an input $X$ and $M$ shared matrices $\Phi_2=\frac12\sum_{x,y}|x,x\rangle\langle y,y|$ , this map measures the input and its first halves with the $Q_i$ , keeps the second half of port $i$ , and sums over $i$ ; explicitly its output entries are

\mathcal P_M(X)_{u,v} =\sum_{\substack{i,p,q,b,c\\b_i=u,\ c_i=v\\b_j=c_j\ (j\ne i)}} (Q_i)_{q,p}(X\otimes\Phi_2^{\otimes M})_{(p,b),(q,c)}.

Let $\nu_M=1-\operatorname{Re}(\mathcal P_M(|0\rangle\langle1|)_{0,1})$ . For every natural number $M\ge2$ ,

\nu_M =\frac{M+2}{3\,2^{M-1}} +\frac13\sum_{k=0}^{\lfloor(M-1)/2\rfloor} \frac{s_k(s_k+1)}{2^{M-4}}\binom Mk \frac{M+2-\sqrt{(M+2)^2-(2s_k+1)^2}} {(M+2)^2-(2s_k+1)^2}, \qquad s_k=\frac{M-1}{2}-k.

Here the exponents $M-1$ and $M-4$ on $2$ are real-number differences, so negative exponents are included; the summation endpoint uses natural-number subtraction and division. In particular,

\nu_2=\frac{6-\sqrt3}{6}, \qquad \nu_3=\frac12.

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