Degradability makes the entanglement consumption rate vanish

Open

QAlgorithms.Papers.Independent.Intakethird100.P23.degradable_zero_ebit_rate

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

prove2quantum

Let $U:\mathbb C^2\to\mathbb C^b\otimes\mathbb C^e$ be an isometry, so $U^\dagger U=I$ , defining a memoryless channel to Bob and its fixed complementary channel to Eve. All binary inputs are uniform and entropies are in bits. At recursion depth $n\ge0$ , let $N=2^n$ and apply the coherent Arikan encoder $G_N=B_NF^{\otimes n}$ , where $F=\left(\begin{smallmatrix}1&0\\1&1\end{smallmatrix}\right)$ . Amplitude synthesis retains previous bits and averages future bits; phase synthesis retains future bits and averages previous bits, with Bob's coherent copy register $C^N$ retained. Write $r(W)=\|\sqrt{\rho_0}\sqrt{\rho_1}\|_1=\sqrt{F(W)}$ for the root fidelity of a binary channel $W$ . Fix $0<\beta<1/2$ and put $t_n=2^{-N^\beta}$ . Let $G_A,G_P,G_E$ be the respective amplitude-good, phase-good, and Eve-amplitude-good sets, with the strict rule $r(W_N^{(i)})<t_n$ . Write $\mathcal A=G_A\cap G_P$ and $\mathcal B=(G_A\cup G_P)^c$ . Each set depends on $n$ and $\beta$ .

Assume that there is a completely positive trace-preserving map $D:B\to E$ with $\mathcal N^c=D\circ\mathcal N$ for the fixed extension $U$ . Then

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

This concerns asymptotic consumption per channel use; the finite-blocklength set $\mathcal B$ need not be empty.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P23

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P23

open scoped BigOperators ComplexConjugate Matrix

open Filter

open QAlgorithms (Qubits)

open QAlgorithms.Papers.Independent.Information100.P67 (IsDegradable)

attribute [local instance] Classical.propDecidable

/-- The consumed-ebit RATE vanishes for degradable channels; this is not a
finite-blocklength zero-consumption assertion (II, Appendix C, PDF pp.4,8–9). -/
theorem degradable_zero_ebit_rate {b e : ℕ} (U : Matrix (Fin b × Fin e) Bool ℂ)
    (hU : Uᴴ * U = 1) (hdeg : IsDegradable U)
    (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    Tendsto (fun n => indexRate (consumedSet U n beta)) atTop (nhds 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P23

Source

Quantum polar codes for arbitrary channels, arXiv:1201.2906v2, PDF p. 9, II and Appendix C

Read-back

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

For all natural numbers $b,e$ , every complex matrix $U$ with rows indexed by $\{0,\ldots,b-1\}\times\{0,\ldots,e-1\}$ and Boolean columns satisfying $U^\dagger U=I_2$ , assume also that there exists a map $D$ from $b\times b$ complex matrices to $e\times e$ complex matrices with a finite Kraus representation

D(X)=\sum_{\ell=0}^{m-1}K_\ell X K_\ell^\dagger, \qquad \sum_{\ell=0}^{m-1}K_\ell^\dagger K_\ell=I_b,

such that, for every $2\times2$ complex matrix $\rho$ ,

\operatorname{Tr}_{B}(U\rho U^\dagger) = D\!\left(\operatorname{Tr}_{E}(U\rho U^\dagger)\right).

For any real $0<\beta<\tfrac12$ , define the following sets. For $n\in\mathbb N$ , including zero, put $N=2^n$ , identify bits with $0,1$ , and define

G^{(n)}_{rj} = \mathbf1\!\left\{ \forall\,0\le k<n,\ \left\lfloor j/2^k\right\rfloor\bmod2 \le \left\lfloor r/2^{n-1-k}\right\rfloor\bmod2 \right\}, \qquad p_n(u)_j=\left(\sum_{r<N}u_rG^{(n)}_{rj}\right)\bmod2.

Set

v_u(\mathbf r,\mathbf z)=\prod_{j<N}U_{(r_j,z_j),p_n(u)_j}, \qquad w_x(\mathbf r,u,\mathbf z) = 2^{-N/2}(-1)^{\sum_jx_ju_j}v_u(\mathbf r,\mathbf z),

and $A_n(u)=\operatorname{Tr}_{\mathbf z}|v_u\rangle\langle v_u|$ , $Q_n(x)=\operatorname{Tr}_{\mathbf z}|w_x\rangle\langle w_x|$ . Let $m_i^-(u)$ retain exactly the bits with $j<i$ , setting the others to zero, and $m_i^+(u)$ retain exactly those with $i<j$ , setting the others to zero. Put

A_{n,i}(a)=2^{-(N-1)}\sum_{u:u_i=a} |m_i^-(u)\rangle\langle m_i^-(u)|\otimes A_n(u), \quad P_{n,i}(a)=2^{-(N-1)}\sum_{x:x_i=a} |m_i^+(x)\rangle\langle m_i^+(x)|\otimes Q_n(x).

Writing $F_{\mathrm r}(K,L)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt K\,L\,\sqrt K}$ , with matrix square roots given by real continuous functional calculus, let

\mathcal C_n = \left\{i<N: F_{\mathrm r}(A_{n,i}(0),A_{n,i}(1))\ge 2^{-N^\beta} \ \text{and}\ F_{\mathrm r}(P_{n,i}(0),P_{n,i}(1))\ge 2^{-N^\beta} \right\}.

Then

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

The hypotheses cannot hold if $b=0$ or $e=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