Secret-key consumption has vanishing rate

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.assistance_rate_vanishes

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

prove2quantum

Under the degraded binary cq wiretap-channel and commuting Eve-output assumptions, fix $0<\beta<1/2$ and use $N=2^n$ . Let $\mathcal P_N$ be Eve's strict poor set, and let $\mathcal B_N(W,\beta)$ be Bob's bad set. Define $\mathcal X_N=\mathcal P_N(W^*,\beta)^{\mathrm c}\cap\mathcal B_N(W,\beta)$ . Then

\lim_{n\to\infty}\frac{|\mathcal X_{2^n}|}{2^n}=0.

These indices carry independent uniform preshared secret bits in the wiretap scheme. The conclusion allows nonzero, growing sublinear key length; the same index count is the ebit-consumption rate in the coherent construction.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P10

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P10

open scoped BigOperators Matrix ComplexConjugate

open Filter

-- Accepted definitions, without paper-local aliases.

open QAlgorithms.Papers.Independent.Information100.P58 (basisDensity)

open QAlgorithms.Papers.Independent.Information100.P67 (squaredFidelity)

open QAlgorithms.Papers.Independent.Claimed50.P48 (indexedKrausDilation)

/-- PDF p.6, Proposition 7: vanishing secret-key rate, allowing nonzero sublinear
key length at every finite blocklength. -/
theorem assistance_rate_vanishes {B E : Type*} [Fintype B] [DecidableEq B] [Nonempty B]
    [Fintype E] [DecidableEq E] [Nonempty E]
    (V : Wiretap B E) (beta : ℝ) (hpos : 0 < beta) (hbeta : beta < 1 / 2) :
    Tendsto (fun n => leafProbability (assistanceSet V n beta)) atTop (nhds 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 6, Proposition 7: vanishing secret-key rate

Read-back

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

Let $B,E$ be finite, nonempty sets with decidable equality. Let $V$ consist of positive semidefinite trace-one matrices $\Omega_0,\Omega_1$ on $B\times E$ and a map $D(X)=\sum_{\ell=0}^{m-1}K_\ell XK_\ell^\dagger$ from matrices on $B$ to matrices on $E$ , with $\sum_\ell K_\ell^\dagger K_\ell=I_B$ . Define $R_x(b,b')=\sum_e\Omega_x((b,e),(b',e))$ and $Q_x(e,e')=\sum_b\Omega_x((b,e),(b,e'))$ . Assume $Q_x=D(R_x)$ for $x=0,1$ , and $Q_0Q_1=Q_1Q_0$ . Fix $0<\beta<\tfrac12$ . For either binary matrix family $W=R$ or $W=Q$ , its synthesized matrices are defined by putting $N=2^n$ , taking the most-significant-first $n$ -bit digits $d_t(j)$ of $j<N$ , setting $c_{jk}=1$ precisely when $d_t(k)=1$ implies $d_{n-1-t}(j)=1$ for every $t<n$ , and otherwise setting $c_{jk}=0$ , and defining $v_k(u)=\sum_{j<N}u_jc_{jk}\pmod2$ . For Boolean prefixes $h,h'$ of length $i$ and words $a,b$ of length $N$ in the relevant matrix index set, put

W_{n,i}^{(x)}((h,a),(h',b)) = \begin{cases} 2^{-(N-1)} \displaystyle\sum_{\substack{u\in\{0,1\}^N\\u_i=x,\;u_{<i}=h}} \prod_{k<N}W_{v_k(u)}(a_k,b_k),&h=h',\\ 0,&h\ne h'. \end{cases}

With $F_{\mathrm r}(X,Y)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X}$ , where square roots use continuous functional calculus, the conclusion is

\lim_{n\to\infty} \frac{\#\{\,i<N: F_{\mathrm r}(Q_{n,i}^{(0)},Q_{n,i}^{(1)})\le 1-2^{-N^\beta}, \quad 2^{-N^\beta}\le F_{\mathrm r}(R_{n,i}^{(0)},R_{n,i}^{(1)}) \,\}}{N} =0.

Thus equality at either threshold is included in the counted set. The sequence also has its $n=0$ term, where $N=1$ , the bit condition is vacuous, and the word transform is the identity.

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