II: accepting several partition cells cannot help when each cell is extendable

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.announcementReduction

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

prove2quantum

Let $n\ge1$ and $0\le Q\le\tfrac12$ . Partition the binary words of length $n$ into finitely many nonempty disjoint cells $C_s$ , and let $S_0$ be a nonempty set of accepted cells. For each cell, form its Bob-only filtered operator $P_s$ from the six-state input, labeling its distinct words individually. Let $\Omega$ be the accepted announcement operator with the cell label recorded classically by both parties, and let $\bar\Omega$ be obtained by forgetting this label. These are block-diagonal sums of branches, without coherence between different announcements. With $\mathrm{Ext}_B$ denoting positive-operator symmetric extendability to a copy of Bob,

\bigl[\forall s\in S_0,\ \mathrm{Ext}_B(P_s)\bigr] \Longrightarrow \mathrm{Ext}_B(\Omega)\ \text{and}\ \mathrm{Ext}_B(\bar\Omega).

Equivalently, a nonextendable accepted public announcement has a nonextendable cell branch. This justifies reducing the partition search to single accepted cells; it makes no claim that nonextendability suffices to distill key.

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.3: accepting several partition cells cannot help if every accepted
single-cell branch is extendable. No sufficiency claim for key distillation. -/
theorem announcementReduction {n : ℕ} (hn : 1 ≤ n)
    {S : Type} [Fintype S] [Nonempty S]
    (cells : S → Finset (Qubits n)) (hcells : ∀ s, (cells s).Nonempty)
    (hpartition : ∀ w : Qubits n, ∃! s, w ∈ cells s)
    (accepted : Finset S) (ha : accepted.Nonempty)
    (Q : ℝ) (hQ0 : 0 ≤ Q) (hQ1 : Q ≤ 1 / 2) :
    ((∀ s ∈ accepted,
      BobExtendible (bobState (fun w : {w : Qubits n // w ∈ cells s} => w.val) Q)) →
      BobExtendible (publicAnnouncement cells accepted Q) ∧
      BobExtendible (forgottenAnnouncement cells accepted Q)) ∧
    (¬ BobExtendible (publicAnnouncement cells accepted Q) →
      ∃ s ∈ accepted,
        ¬ BobExtendible (bobState (fun w : {w : Qubits n // w ∈ cells s} => w.val) Q)) := 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. 3, II: accepting several partition cells cannot help when each cell is extendable

Read-back

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

For every natural number $n\ge1$ , nonempty finite type $S$ with its specified finite enumeration, family of nonempty finite sets $\mathrm{cells}_s\subseteq\{0,1\}^n$ such that every word belongs to exactly one cell, nonempty finite set $\mathrm{accepted}\subseteq S$ , and real $Q$ satisfying $0\le Q\le\tfrac12$ , define

F_Q((a,b),(a',b'))= \prod_{i=0}^{n-1} \left(\frac{1-2Q}{2}\mathbf1_{a_i=b_i}\mathbf1_{a'_i=b'_i} +\frac Q2\mathbf1_{a_i=a'_i}\mathbf1_{b_i=b'_i}\right).

For each $s$ , let $B_s$ be the matrix indexed by $\{0,1\}^n\times\mathrm{cells}_s$ with entry $F_Q((a,w),(a',v))$ at $(a,w),(a',v)$ . Let $P_{\mathrm{pub}}$ , indexed by $(\{0,1\}^n\times S)\times(\{0,1\}^n\times S)$ , have entry $F_Q((a,b),(a',b'))$ at $((a,s),(b,t)),((a',s'),(b',t'))$ precisely when $s=t=s'=t'$ , $s\in\mathrm{accepted}$ , and $b,b'\in\mathrm{cells}_s$ , and have entry zero otherwise. Let $P_{\mathrm{forget}}$ have entries $\sum_{s\in\mathrm{accepted}}\mathbf1_{\{b,b'\in\mathrm{cells}_s\}}F_Q((a,b),(a',b'))$ . Here a matrix $P$ on $X\times Y$ is Bob-extendible when some positive semidefinite matrix $R$ on $(X\times Y)\times Y$ satisfies

\sum_{c\in Y}R_{((x,y),c),((x',y'),c)} =P_{(x,y),(x',y')} =\sum_{c\in Y}R_{((x,c),y),((x',c),y')}

for all indices, without a trace normalization requirement. The theorem asserts the conjunction of two implications: if $B_s$ is Bob-extendible for every accepted $s$ , then both $P_{\mathrm{pub}}$ and $P_{\mathrm{forget}}$ are Bob-extendible; and if $P_{\mathrm{pub}}$ is not Bob-extendible, then there exists an accepted $s$ for which $B_s$ is not Bob-extendible. Both endpoint values $Q=0$ and $Q=\tfrac12$ are included.

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