Erasure-channel sufficient criterion for vanishing key rate

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.erasure_key_rate

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

prove2quantum

Let $\epsilon\in[0,1]$ and consider the complementary qubit erasure wiretap dilation

V|a\rangle=\sqrt{1-\epsilon}|a\rangle^B|e\rangle^E+ \sqrt\epsilon|e\rangle^B|a\rangle^E,

where $a\in\{0,1\}$ and $|e\rangle$ is orthogonal to both input basis states. Use uniform computational-basis inputs and trivial shields. Bob's amplitude and virtual phase channels satisfy

\sqrt{F(W_{A,B})}=\sqrt{F(W_{P,B})}=\epsilon, \qquad I(W_{A,B})-I(W_{A,E})=1-2\epsilon.

For every fixed $0<\beta<1/2$ , the polar code defined above consequently satisfies

2\epsilon<1\quad\Longrightarrow\quad \lim_{n\to\infty}\frac{|\mathcal B_{2^n}|}{2^n}=0.

Thus the criterion applies exactly when this symmetric private information is positive. This is a finite-register erasure result, without a bosonic energy constraint.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P74

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P74

open QAlgorithms

open scoped ComplexConjugate Matrix

noncomputable section

local instance (p : Prop) : Decidable p := Classical.propDecidable p

variable {B E S1 S2 : Type}

variable [Fintype B] [Fintype E] [Fintype S1] [Fintype S2]

variable [DecidableEq B] [DecidableEq E] [DecidableEq S1] [DecidableEq S2]

/-- PDF pp.9–10, Appendix C.B: both initial root fidelities are eps and the strict
criterion 2eps<1 gives vanishing key rate, precisely where symmetric private information
is positive. Source correction: p.10's phase-mixture display swaps eps and 1-eps;
the defining erasure map, its discrimination argument and its final criterion fix the
weights used here. Independent moderation of this correction remains required. -/
theorem erasure_key_rate (eps : ℝ) (he0 : 0 ≤ eps) (he1 : eps ≤ 1)
    (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    rootFidelity (amplitudeBob (erasureData eps) false)
      (amplitudeBob (erasureData eps) true) = eps ∧
    rootFidelity (phaseBob (erasureData eps) false)
      (phaseBob (erasureData eps) true) = eps ∧
    symmetricPrivateInformation (erasureData eps) = 1 - 2 * eps ∧
    (2 * eps < 1 → Filter.Tendsto (keyRate (erasureData eps) beta) Filter.atTop (nhds 0)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74

Source

Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 10, Appendix C.B, unnumbered: erasure-channel criterion

Read-back

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

For all real numbers $\varepsilon,\beta$ satisfying $0\le\varepsilon\le1$ and $0<\beta<\tfrac12$ , identify Boolean values with $0,1$ and let $|i\rangle$ denote coordinate vectors. Define $|s_a\rangle=\sqrt{1-\varepsilon}|a,2\rangle+\sqrt{\varepsilon}|2,a\rangle$ on Bob’s and Eve’s three-dimensional registers, and $|\phi_x\rangle=2^{-1/2}\sum_{a=0}^1(-1)^{xa}|a\rangle_C|s_a\rangle_{BE}$ ; the singleton ancillary registers in the supplied data are omitted through their canonical identifications. Put $B_a=\operatorname{tr}_E|s_a\rangle\langle s_a|=(1-\varepsilon)|a\rangle\langle a|+\varepsilon|2\rangle\langle2|$ , $E_a=\operatorname{tr}_B|s_a\rangle\langle s_a|=\varepsilon|a\rangle\langle a|+(1-\varepsilon)|2\rangle\langle2|$ , and $P_x=\operatorname{tr}_E|\phi_x\rangle\langle\phi_x|$ , which retains registers $C,B$ . For density matrices write $F_{\mathrm r}(\rho,\sigma)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt\rho\,\sigma\sqrt\rho}$ , and write $\chi_{\mathrm{unif}}(W)=S_2((W_0+W_1)/2)-(S_2(W_0)+S_2(W_1))/2$ , where $S_2(\rho)=-\operatorname{Re}\operatorname{tr}(\rho\log_2\rho)$ and zero spectral terms contribute zero. The assertions are

F_{\mathrm r}(B_0,B_1)=\varepsilon,\qquad F_{\mathrm r}(P_0,P_1)=\varepsilon,\qquad \chi_{\mathrm{unif}}(B)-\chi_{\mathrm{unif}}(E)=1-2\varepsilon.

The remaining assertion uses the following explicit index sets. For each natural number $n$ , including $n=0$ , put $N=2^n$ and define a binary matrix $A$ with indices $0\le i,j<N$ by $A_{ij}=1$ exactly when, for every $0\le k<n$ , a set bit in position $k$ of $j$ implies a set bit in position $n-1-k$ of $i$ . For $r\in\{0,1\}$ define $e_0(u)=uA$ and $e_1(u)=uA^{\mathsf T}$ , with arithmetic modulo two, and let $J_{0,i}=\{j:j<i\}$ and $J_{1,i}=\{j:i<j\}$ . For any binary-input matrix family $W$ , define a matrix $\Sigma^{W,r}_{i,b}$ indexed by pairs $(v,y)$ , where $v:J_{r,i}\to\mathrm{Bool}$ and $y:\{0,\ldots,N-1\}\to O$ for the output index set $O$ of $W$ , by

\Sigma^{W,r}_{i,b}((v,y),(v',y')) =\begin{cases} 2^{-(N-1)} \displaystyle\sum_{\substack{u\in\mathrm{Bool}^N\\u_i=b,\ u|_{J_{r,i}}=v}} \prod_{j=0}^{N-1}W_{e_r(u)_j}(y_j,y'_j),&v=v',\\ 0,&v\ne v'. \end{cases}

Set $G_r(W)=\{i:F_{\mathrm r}(\Sigma^{W,r}_{i,0},\Sigma^{W,r}_{i,1})<2^{-N^\beta}\}$ . If $2\varepsilon<1$ , then the fraction

\frac{\bigl|\{0,\ldots,N-1\}\setminus(G_0(B)\cup G_1(P))\bigr|}{N}

tends to zero as $n\to\infty$ . The convergence conclusion is conditional on $2\varepsilon<1$ ; the three preceding equalities are asserted throughout $0\le\varepsilon\le1$ .

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