Phase-good positions are very bad for Eve, with eventual packing

Open

QAlgorithms.Papers.Independent.Intakethird100.P23.good_set_disjointness

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$ .

For every $n$ and every $i\in G_P$ ,

r(W_{E,N}^{(i)})>1-2t_n.

There is a depth $n_0$ such that for every $n\ge n_0$ , the sets $G_P$ and $G_E$ are disjoint, as are $\mathcal B$ and $G_P$ . If the channel is degradable from Bob to Eve, then $\mathcal B$ and $G_E$ are also disjoint, and

|G_E|+|G_P|+|\mathcal B|\le N.

This packing statement is the finite-blocklength input to the vanishing consumption-rate argument.

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

/-- Quantitative very-bad conclusion and eventual disjoint-set packing,
Appendix C, PDF p.9. Degradability is needed only for the final two clauses. -/
theorem good_set_disjointness {b e : ℕ} (U : Matrix (Fin b × Fin e) Bool ℂ)
    (hU : Uᴴ * U = 1) (beta : ℝ) (hbeta0 : 0 < beta) (hbeta1 : beta < 1 / 2) :
    (∀ n, ∀ i ∈ goodPhase U n beta,
      1 - 2 * threshold n beta < channelRootFidelity (environmentSplit U n i)) ∧
    (∃ n0 : ℕ, ∀ n ≥ n0,
      Disjoint (goodPhase U n beta) (goodEnvironment U n beta) ∧
      Disjoint (consumedSet U n beta) (goodPhase U n beta) ∧
      (IsDegradable U →
        Disjoint (consumedSet U n beta) (goodEnvironment U n beta) ∧
        (goodEnvironment U n beta).card + (goodPhase U n beta).card +
          (consumedSet U n beta).card ≤ 2 ^ n)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P23

Source

Quantum polar codes for arbitrary channels, arXiv:1201.2906v2, PDF p. 9, 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$ , and every real $0<\beta<\tfrac12$ , define the following objects. For each $n\in\mathbb N$ , including zero, put $N=2^n$ , identify bits with $0,1$ , and set

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,

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).

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

A_{n,i}(a)=2^{-(N-1)}\sum_{u:u_i=a} |m_i^-(u)\rangle\langle m_i^-(u)|\otimes A_n(u),

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

Write $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, and $\tau_n=2^{-N^\beta}$ . Let

\mathcal A_n=\{i<N:F_{\mathrm r}(A_{n,i}(0),A_{n,i}(1))<\tau_n\}, \quad \mathcal P_n=\{i<N:F_{\mathrm r}(P_{n,i}(0),P_{n,i}(1))<\tau_n\},

\mathcal E_n=\{i<N:F_{\mathrm r}(E_{n,i}(0),E_{n,i}(1))<\tau_n\}, \qquad \mathcal C_n=\{0,\ldots,N-1\}\setminus(\mathcal A_n\cup\mathcal P_n).

The statement asserts that, for every $n$ and every $i\in\mathcal P_n$ ,

1-2\tau_n<F_{\mathrm r}(E_{n,i}(0),E_{n,i}(1)),

and that there exists a natural number $n_0$ , with no stipulated positive lower bound, such that every $n\ge n_0$ satisfies

\mathcal P_n\cap\mathcal E_n=\varnothing, \qquad \mathcal C_n\cap\mathcal P_n=\varnothing.

For those same $n$ , if there exists a finite Kraus map $D(X)=\sum_{\ell<m}K_\ell X K_\ell^\dagger$ , with $K_\ell$ of size $e\times b$ and $\sum_{\ell<m}K_\ell^\dagger K_\ell=I_b$ , satisfying

\operatorname{Tr}_{B}(U\rho U^\dagger) = D\!\left(\operatorname{Tr}_{E}(U\rho U^\dagger)\right) \quad\text{for every complex }2\times2\text{ matrix }\rho,

then also

\mathcal C_n\cap\mathcal E_n=\varnothing, \qquad |\mathcal E_n|+|\mathcal P_n|+|\mathcal C_n|\le 2^n.

If $b=0$ or $e=0$ , the isometry hypothesis is impossible.

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