Theorem 2: unconditional strong security

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.strong_security

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.

Let $U_{\mathcal A}$ denote the uniformly distributed private message and let $E^N$ denote only Eve's output of the actual memoryless channel after the polar encoder. Then

I(U_{\mathcal A};E^N)=o\!\left(2^{-N^\beta/2}\right) \quad(n\to\infty).

The conditional Eve states are computed by averaging all independent nonmessage bits, and the leakage is their uniform-message Holevo information. This is the unconditional security criterion printed in Theorem 2; it does not assert arbitrary-prior security or a bound for each fixed frozen string.

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.4, Theorem 2: unconditional uniform-message leakage is little-o of
2^(-N^beta/2). No arbitrary-prior or per-frozen-string claim is added. The paper's last
polynomial-factor bound alone does not establish the stated little-o. -/
theorem strong_security (d : WiretapData B E S1 S2) (hd : d.Valid)
    (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    Asymptotics.IsLittleO Filter.atTop (privateMessageLeakageBits d beta) (decayHalf beta) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74

Source

Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 4, Theorem 2: strong security

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$ , and let $0<\beta<\tfrac12$ . Define

s_z(b,e,s,t)=\sum_{a\in\{0,1\}}V_{(b,e,t),a}\psi_z(a,s),\quad W^A_z=\operatorname{Tr}_{E,S_1,S_2}(s_zs_z^*),\quad W^E_z=\operatorname{Tr}_{B,S_1,S_2}(s_zs_z^*),

and $W^P_x=\operatorname{Tr}_E(\varphi_x\varphi_x^*)$ , where $\varphi_x((z,b,s,t),e)=2^{-1/2}(-1)^{xz}s_z(b,e,s,t)$ . For each natural $n$ , put $N=2^n$ , $I=\{0,\ldots,N-1\}$ , define $G_{ij}=1$ exactly when every bit $k<n$ set in $j$ has bit $n-1-k$ set in $i$ , and put $e_-(u)_j=\sum_i u_iG_{ij}\pmod2$ , $e_+(u)_j=\sum_i u_iG_{ji}\pmod2$ . With $J_i^-=\{j:j<i\}$ and $J_i^+=\{j:i<j\}$ , define

[\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}

Let $F(R,S)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt R\,S\sqrt R}$ and

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

For every assignment $m:A_n\to\{0,1\}$ , put

\rho_m=2^{|A_n|-N} \sum_{\substack{u\in\{0,1\}^I\\u|_{A_n}=m}} \bigotimes_{i\in I}W^E_{e_-(u)_i}, \qquad L_n=S_2\!\left(2^{-|A_n|}\sum_m\rho_m\right) -2^{-|A_n|}\sum_mS_2(\rho_m),

where $S_2(R)=-\operatorname{Re}\operatorname{tr}(\operatorname{cfc}[r\mapsto r\log_2r](R))$ . Then $L_n=o(2^{-(2^n)^\beta/2})$ as $n\to\infty$ , meaning that for every $c>0$ , eventually

|L_n|\le c\,2^{-(2^n)^\beta/2}.

The sequence is defined also at $n=0$ ; the sets $A_n$ may be empty, in which case the message-assignment set has one element and $L_n=0$ .

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