Theorem 3: initial root-fidelity sufficient criterion

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.root_fidelity_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.

If the two initial, unsynthesized channels obey

\sqrt{F(W_{A,B})}+\sqrt{F(W_{P,B})}<1,

then

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

This sufficient condition does not require degradability. Its conclusion concerns the asymptotic key rate; the source leaves finite-block zero key consumption open.

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, Theorem 3, Appendix B pp.6–7: a strict condition on initial,
unsynthesized ROOT fidelities suffices. No degradability or finite-block emptiness follows. -/
theorem root_fidelity_key_rate (d : WiretapData B E S1 S2) (hd : d.Valid)
    (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2)
    (hroot : rootFidelity (amplitudeBob d false) (amplitudeBob d true) +
      rootFidelity (phaseBob d false) (phaseBob d true) < 1) :
    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, Theorem 3: sufficient root-fidelity criterion for vanishing key rate

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

Writing $F(R,S)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt R\,S\sqrt R}$ , assume the strict inequality

F(W^A_0,W^A_1)+F(W^P_0,W^P_1)<1.

For each natural $n$ , including zero, 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$ . For $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

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.

No nonemptiness of either selected index set is required.

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