IV: Alice filtering cannot increase the threshold, (20)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.alicePostselection

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

prove2quantum

Let $C=(C_k)_{k\in K}$ be any nonempty code of distinct $n$ -bit words, $n\ge1$ , and define $K_C=\sum_k|k\rangle\langle C_k|$ . For $0\le Q\le\tfrac12$ , let $P_B(Q)$ and $P_{AB}(Q)$ be the six-state operators after Bob-only and same-code Alice/Bob filtering. The latter is positive with strictly positive trace and satisfies

P_{AB}(Q)=(K_C\otimes I)P_B(Q)(K_C\otimes I)^\dagger,

\mathrm{Ext}_B(P_B(Q))\Longrightarrow\mathrm{Ext}_B(P_{AB}(Q)), \qquad Q_{C,\mathrm{both}}^*\le Q_{C,\mathrm{Bob}}^*.

All filtered operators are unnormalized. This shows that allowing this extra Alice filter cannot increase the threshold. The converse is not asserted for arbitrary codes; the repetition-code equivalence is stated separately.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P30

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P30

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

variable {I J K L A B : Type}

variable [Fintype I] [Fintype J] [Fintype K] [Fintype L]

variable [Fintype A] [Fintype B]

/-- PDF p.7, (20): actual Alice-filter factorization and preservation of extendability,
with the threshold comparison in the correct direction. -/
theorem alicePostselection {n : ℕ} (hn : 1 ≤ n) [Nonempty K]
    (C : K → Qubits n) (hC : Function.Injective C) :
    (∀ Q : ℝ, 0 ≤ Q → Q ≤ 1 / 2 →
      (bothState C Q).PosSemidef ∧ 0 < (bothState C Q).trace.re ∧
      bothState C Q =
        Matrix.kronecker (codeKraus C) (1 : Matrix K K ℂ) * bobState C Q *
          (Matrix.kronecker (codeKraus C) (1 : Matrix K K ℂ))ᴴ ∧
      (BobExtendible (bobState C Q) → BobExtendible (bothState C Q))) ∧
    bothThreshold C ≤ bobThreshold C := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P30

end

Source

Numerical evidence for bound secrecy from two-way post-processing in quantum key distribution, arXiv:1612.07734v2, PDF p. 7, IV: Alice filtering cannot increase the threshold, (20)

Read-back

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

Let $n$ be a natural number with $1\le n$ , let $K$ be a nonempty finite index type with decidable equality, and let $C:K\to\{0,1\}^n$ be injective. Define $\phi_{ab}=1/\sqrt2$ when $a=b$ and $0$ otherwise, for Boolean $a,b$ , and set $s_Q=(1-2Q)\phi\phi^\dagger+(Q/2)I_4$ and

\Sigma_Q((a,b),(a',b'))=\prod_{i=0}^{n-1}s_Q((a_i,b_i),(a'_i,b'_i)).

Let $F_{k,w}=1$ if $w=C(k)$ and $0$ otherwise, and define

R_Q=(I_{\{0,1\}^n}\otimes F)\Sigma_Q(I_{\{0,1\}^n}\otimes F)^\dagger, \qquad B_Q=(F\otimes F)\Sigma_Q(F\otimes F)^\dagger.

For a matrix $P$ indexed by $A\times B$ , write $E(P)$ for the existence of a positive semidefinite matrix $X$ indexed by $(A\times B)\times B$ such that, for every $a,a',b,b'$ ,

\sum_c X(((a,b),c),((a',b'),c))=P((a,b),(a',b')), \qquad \sum_c X(((a,c),b),((a',c),b'))=P((a,b),(a',b')).

No trace normalization is required in this extension condition. The assertion is that, for every real $Q$ with $0\le Q\le\tfrac12$ , $B_Q$ is positive semidefinite, $\operatorname{Re}\operatorname{tr}(B_Q)>0$ ,

B_Q=(F\otimes I_K)R_Q(F\otimes I_K)^\dagger, \qquad E(R_Q)\ \Longrightarrow\ E(B_Q),

and, additionally,

\sup\bigl(\{0\}\cup\{q\in[0,\tfrac12]:\neg E(B_q)\}\bigr) \le \sup\bigl(\{0\}\cup\{q\in[0,\tfrac12]:\neg E(R_q)\}\bigr).

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