Information-set rate tends to symmetric private information

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.wiretap_rate

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

prove2quantum

Let $x\mapsto\rho_x^{BE}$ be a binary cq wiretap channel with finite nonempty registers. Its Bob and Eve marginals are $W$ and $W^*$ , one CPTP map degrades $W$ to $W^*$ for both letters, and the two Eve letter states commute. Fix $0<\beta<1/2$ . At each $N=2^n$ , use the prescribed fidelity-defined sets and put $\mathcal A_N=\mathcal P_N(W^*,\beta)\cap\mathcal G_N(W,\beta)$ . The polar construction places its information bits on these indices, so its information rate satisfies

\lim_{n\to\infty}\frac{|\mathcal A_{2^n}|}{2^n}=I(W)-I(W^*).

This is the rate of the specified index-set construction. The separate preshared-key consumption is not subtracted, and no unrestricted private-capacity optimization is asserted.

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 pp.5–6, Theorem 5: prescribed information-set rate along N=2^n.
This is |A|/N without subtracting the separate secret-key consumption. -/
theorem wiretap_rate {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 (informationSet V n beta)) atTop
      (nhds (symmetricInformation V.bob - symmetricInformation V.eve)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 5, Theorem 5: quantum wiretap polar-code 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 two positive semidefinite trace-one matrices $\Omega_0,\Omega_1$ indexed by $B\times E$ , together with a map $D$ from matrices on $B$ to matrices on $E$ admitting a finite Kraus representation $D(X)=\sum_{\ell=0}^{m-1}K_\ell XK_\ell^\dagger$ , where $\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'))$ , and assume $Q_x=D(R_x)$ for both Boolean values $x$ , and $Q_0Q_1=Q_1Q_0$ . Let $0<\beta<\tfrac12$ . For any binary matrix family $W=(W_0,W_1)$ , define its synthesized matrices as follows: put $N=2^n$ , let $d_t(j)$ be the most-significant-first $n$ -bit digits of $j<N$ , set $c_{jk}=1$ if every $t<n$ with $d_t(k)=1$ has $d_{n-1-t}(j)=1$ , and set $c_{jk}=0$ otherwise; put $v_k(u)=\sum_{j<N}u_jc_{jk}\pmod2$ . On indices $(h,a),(h',b)$ , where $h,h'$ are Boolean words of length $i$ and $a,b$ are length- $N$ words in the matrix index set, set

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}

Write $F_{\mathrm r}(X,Y)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X}$ , using continuous functional calculus, and $S(X)=-\operatorname{Re}\operatorname{tr}(f(X))$ for $f(t)=t\log_2t$ . Put $I(W)=S((W_0+W_1)/2)-(S(W_0)+S(W_1))/2$ . The assertion is

\lim_{n\to\infty} \frac{\#\left\{i<N: \begin{array}{l} 1-2^{-N^\beta}<F_{\mathrm r}(Q_{n,i}^{(0)},Q_{n,i}^{(1)}),\\ F_{\mathrm r}(R_{n,i}^{(0)},R_{n,i}^{(1)})<2^{-N^\beta} \end{array}\right\}}{N} =I(R)-I(Q).

Both displayed membership inequalities are strict. The sequence includes $n=0$ , where $N=1$ , the bit condition is vacuous, and the transformed word is unchanged.

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