II A: concatenated-code tensor product and max threshold, (5)–(6)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.directSum

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

prove2quantum

Let $S$ be a finite nonempty set of blocks. For each $s\in S$ , let $C_s$ be a nonempty code of distinct words on a finite nonempty coordinate register $D_s$ , with finite label set $K_s$ . Form the full Cartesian concatenation $C=\lvert C_s:s\in S\rvert$ , labeled by $\prod_s K_s$ , with coordinates $\coprod_sD_s$ . For $0\le Q\le\tfrac12$ , write $P_s(Q)$ and $P_C(Q)$ for the constructed Bob-only filtered operators. Under the explicit regrouping into corresponding Alice/Bob blocks,

P_C(Q)=\bigotimes_{s\in S}P_s(Q),\qquad \mathrm{Ext}_B(P_C(Q))\Longleftrightarrow\forall s\in S,\ \mathrm{Ext}_B(P_s(Q)),\qquad Q_C^*=\max_{s\in S}Q_{C_s}^*.

Here $Q_C^*$ is the upper boundary of nonextendable QBERs in $[0,\tfrac12]$ , with value zero when none exist. The statement includes two codes and all finite nonempty iterates. Concatenation is a Cartesian product, and the constructed factors have positive trace.

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.4, (5)–(6), including the finite iterated version: explicit block
regrouping yields the product coefficients and the maximum component threshold. -/
theorem directSum {S : Type} [Fintype S] [Nonempty S]
    {D M : S → Type} [∀ s, Fintype (D s)] [∀ s, Nonempty (D s)]
    [∀ s, Fintype (M s)] [∀ s, Nonempty (M s)]
    (C : (s : S) → M s → (D s → Bool)) (hC : ∀ s, Function.Injective (C s)) :
    (∀ Q : ℝ, 0 ≤ Q → Q ≤ 1 / 2 →
      (∀ (w w2 : Sigma D → Bool) (k l : (s : S) → M s),
        bobState (multiCode C) Q (w, k) (w2, l) =
          ∏ s, bobState (C s) Q ((fun i => w ⟨s, i⟩), k s)
            ((fun i => w2 ⟨s, i⟩), l s)) ∧
      (BobExtendible (bobState (multiCode C) Q) ↔
        ∀ s, BobExtendible (bobState (C s) Q))) ∧
    bobThreshold (multiCode C) = sSup (Set.range (fun s => bobThreshold (C s))) := 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. 4, II A: concatenated-code tensor product and max threshold, (5)–(6)

Read-back

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

Let $S$ be a finite nonempty type; for each $s\in S$ , let $D_s$ and $M_s$ be finite nonempty coordinate and label types, and let $C_s:M_s\to\{0,1\}^{D_s}$ be injective. Define the combined code by $C_{\mathrm{multi}}(k)_{(s,i)}=C_s(k_s)_i$ , where $k\in\prod_sM_s$ . For any finite-coordinate code $E:L\to\{0,1\}^{J}$ , define

B_{E,Q}((a,k),(a',l)) =\prod_{i\in J} \left( \frac{1-2Q}{2}\mathbf1_{a_i=E(k)_i}\mathbf1_{a'_i=E(l)_i} +\frac Q2\mathbf1_{a_i=a'_i}\mathbf1_{E(k)_i=E(l)_i} \right).

Say that a matrix $P$ indexed by $A\times B$ admits a Bob-copy extension when there exists a positive semidefinite matrix indexed by $(A\times B)\times B$ whose two partial traces, obtained by summing over either copy of $B$ , both equal $P$ ; no trace-one condition is imposed on this extension. Define

b(E)=\sup\!\left(\{0\}\cup \{q\in[0,1/2]:B_{E,q}\text{ admits no Bob-copy extension}\}\right).

The theorem asserts that, for every $Q\in[0,1/2]$ , every pair of Boolean strings $w,w'$ on the disjoint union of the $D_s$ , and every $k,l\in\prod_sM_s$ ,

B_{C_{\mathrm{multi}},Q}((w,k),(w',l)) =\prod_{s\in S}B_{C_s,Q}((w_s,k_s),(w'_s,l_s)), \qquad w_s(i)=w(s,i),

and that $B_{C_{\mathrm{multi}},Q}$ admits a Bob-copy extension if and only if every $B_{C_s,Q}$ does. It also asserts

b(C_{\mathrm{multi}})=\sup\{b(C_s):s\in S\}.

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