Vanishing key rate under degradability to Eve

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.degradable_key_rate

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

prove2quantum

Let $\mathcal N:A'\to BE$ be a memoryless finite-register quantum wiretap channel with qubit input, with a fixed isometric extension $V:A'\to BES_2$ . Choose two unit purifications $|\psi_z\rangle^{A'S_1}$ of the input states, with $z\in\{0,1\}$ equiprobable. Both shields $S_1,S_2$ are excluded from Eve. Let $W_{A,B}$ and $W_{A,E}$ be the resulting amplitude channels to Bob and Eve. The virtual phase channel $W_{P,B}$ has output $BCS_1S_2$ , obtained by phase modulating the reference of the coherent source $2^{-1/2}\sum_z|z\rangle^C|\psi_z\rangle$ and tracing only Eve after $V$ . Entropies and Holevo information are in bits, and $F$ denotes squared fidelity.

Fix $0<\beta<1/2$ and blocklength $N=2^n$ . Use Arikan's fixed transform $G_N$ for amplitude and its transpose for phase; amplitude splitting reveals previous bits and averages future bits, while phase splitting reveals future bits and averages previous bits. An index is good precisely when its synthesized root fidelity is strictly less than $2^{-N^\beta}$ . Write $\mathcal G_A,\mathcal G_P$ for the good sets and define $\mathcal A=\mathcal G_A\cap\mathcal G_P$ , $\mathcal X=\mathcal G_A\setminus\mathcal G_P$ , $\mathcal Z=\mathcal G_P\setminus\mathcal G_A$ , and $\mathcal B=[N]\setminus(\mathcal G_A\cup\mathcal G_P)$ . The code sends independent uniform private bits on $\mathcal A$ , local random bits on $\mathcal X$ , frozen bits known to Bob on $\mathcal Z$ , and preshared uniform secret key bits on $\mathcal B$ . Error and leakage average over these uniform choices.

Assume that a CPTP map $\mathcal D:B\to E$ satisfies $\mathcal D\circ\mathcal N_B=\mathcal N_E$ on all input operators. Then

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

This guarantees vanishing preshared-key consumption per channel use for this code. The degrading map targets Eve alone; it need not simulate the shield $S_2$ .

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 p.5, §III: this scheme's key consumption RATE vanishes for channels degradable
to Eve's marginal; finite-block zero consumption is not claimed. -/
theorem degradable_key_rate (d : WiretapData B E S1 S2) (hd : d.Valid)
    (hdegradable : EveDegradable d) (beta : ℝ)
    (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    Filter.Tendsto (keyRate d 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. 5, §III, unnumbered: vanishing key rate for degradable wiretap channels

Read-back

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

For finite index types $B,E,S_1,S_2$ , with decidable equality as required, let $d=(V,\psi)$ satisfy $V^*V=I_2$ and $\|\psi_z\|=1$ for both Boolean $z$ . Suppose there exists a map $D$ from $B\times B$ complex matrices to $E\times E$ complex matrices, represented for every matrix $X$ by $D(X)=\sum_{j<r}K_jXK_j^*$ for some natural $r$ and matrices $K_j:\mathbb C^B\to\mathbb C^E$ with $\sum_jK_j^*K_j=I_B$ , such that for every complex $2\times2$ matrix $\rho$ ,

D\!\left(\operatorname{Tr}_{E\times S_2}(V\rho V^*)\right) = \left[\sum_{b\in B}\sum_{s\in S_2} (V\rho V^*)_{(b,e,s),(b,f,s)}\right]_{e,f\in E}.

Let $0<\beta<\tfrac12$ , define

s_z(b,e,s,t)=\sum_aV_{(b,e,t),a}\psi_z(a,s),\quad W^A_z=\operatorname{Tr}_{E,S_1,S_2}(s_zs_z^*),\quad W^P_x=\operatorname{Tr}_E(\varphi_x\varphi_x^*), \quad\varphi_x((z,b,s,t),e)=2^{-1/2}(-1)^{xz}s_z(b,e,s,t).

For each natural $n$ , including zero, put $N=2^n$ , $I=\{0,\ldots,N-1\}$ , and define $G_{ij}=1$ precisely when every bit $k<n$ set in $j$ has bit $n-1-k$ set in $i$ . Set $e_-(u)_j=\sum_i u_iG_{ij}\pmod2$ and $e_+(u)_j=\sum_i u_iG_{ji}\pmod2$ . For $J_i^-=\{j:j<i\}$ and $J_i^+=\{j:i<j\}$ , form

[\Sigma^{W,\pm}_{i,b}]_{(h,y),(h',y')}= \begin{cases} 2^{-(N-1)} \displaystyle\sum_{\substack{u\in\{0,1\}^I\\u_i=b,\ u|_{J_i^\pm}=h}} \prod_{\ell\in I}W_{e_\pm(u)_\ell}(y_\ell,y'_\ell),&h=h',\\ 0,&h\ne h'. \end{cases}

With $F(R,S)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt R\,S\sqrt R}$ , let

D_n=\{i:F(\Sigma^{W^A,-}_{i,0},\Sigma^{W^A,-}_{i,1})<2^{-N^\beta}\},\qquad P_n=\{i:F(\Sigma^{W^P,+}_{i,0},\Sigma^{W^P,+}_{i,1})<2^{-N^\beta}\}.

Then

\lim_{n\to\infty}\frac{|I\setminus(D_n\cup P_n)|}{2^n}=0.

The numerator counts the indices belonging to neither set; either set, and their complement, may be empty.

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