Limiting signed net private rate

Open

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

The signed net rate of this code satisfies

\lim_{n\to\infty}\frac{|\mathcal A_{2^n}|-|\mathcal B_{2^n}|}{2^n} =I(W_{A,B})-I(W_{A,E}).

This identifies the rate for the fixed uniform input ensemble, with preshared key consumption subtracted. It does not optimize the ensemble or clip negative rates.

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.1,4, abstract and §II.C: limiting signed net rate equals fixed-ensemble
symmetric private information, without capacity optimization or positive-part clipping. -/
theorem net_rate (d : WiretapData B E S1 S2) (hd : d.Valid)
    (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    Filter.Tendsto (netRate d beta) Filter.atTop (nhds (symmetricPrivateInformation d)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74

Source

Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 4, Abstract and §II.C, unnumbered: symmetric private information net 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 $z\in\{0,1\}$ , 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$ , including $n=0$ , set $N=2^n$ , $I=\{0,\ldots,N-1\}$ , and let $G_{ij}$ be the Boolean condition that every bit $k<n$ set in $j$ has bit $n-1-k$ set in $i$ . Over $\mathbb F_2$ , put $e_-(u)_j=\sum_i u_iG_{ij}$ and $e_+(u)_j=\sum_i u_iG_{ji}$ . For a binary output family $W$ , 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} \quad J_i^-=\{j:j<i\},\quad J_i^+=\{j:i<j\}.

Using $F(R,S)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt R\,S\sqrt R}$ , define

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{|D_n\cap P_n|-|I\setminus(D_n\cup P_n)|}{2^n} = \chi(W^A)-\chi(W^E),

where

\chi(W)=S_2\!\left(\frac{W_0+W_1}{2}\right) -\frac{S_2(W_0)+S_2(W_1)}2,\qquad S_2(R)=-\operatorname{Re}\operatorname{tr} \bigl(\operatorname{cfc}[r\mapsto r\log_2r](R)\bigr).

The cardinalities in the numerator are cast to real numbers before subtraction, so negative values are included; the index sets 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