IV A: simplex codes do not exceed repetition thresholds

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.simplexThreshold

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

prove2quantum

Let $C$ be an equidistant binary code of $m\ge2$ distinct words of length $n\ge1$ , with no constant columns, and common distance $1\le d\le n$ . Let $Q_{C,\mathrm{both}}^*$ be the symmetric-extendability threshold when Alice and Bob both postselect on this same code, and let $Q_{R_n}^*$ be the repetition-code threshold. Then

Q_{C,\mathrm{both}}^*\le Q_{R_n}^*\le c, \qquad c=\frac{5-\sqrt5}{10}.

For every $Q\in[c,\tfrac12]$ , the constructed both-party filtered operator is symmetrically extendable. Thus same-code simplex postselection cannot break symmetric extendability in the gap above Chau's threshold. This is specifically the both-party regime; no Bob-only simplex threshold equivalence is assumed.

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.8: simplex thresholds in the BOTH-party regime do not exceed the
same-length repetition threshold or Chau's limit. No Bob-only simplex claim. -/
theorem simplexThreshold {n m d : ℕ} (hn : 1 ≤ n) (hm : 2 ≤ m)
    (hd0 : 1 ≤ d) (hdn : d ≤ n) (C : Fin m → Qubits n)
    (hC : Function.Injective C) (hd : Equidistant C d) (hcols : NoConstantColumns C) :
    bothThreshold C ≤ bobThreshold (repetition (Fin n)) ∧
    bobThreshold (repetition (Fin n)) ≤ chau ∧
    (∀ Q : ℝ, 0 ≤ Q → Q ≤ 1 / 2 → chau ≤ Q → BobExtendible (bothState C 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. 8, IV A: simplex codes do not exceed repetition thresholds

Read-back

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

For all natural numbers $n,m,d$ with $n\ge1$ , $m\ge2$ , and $1\le d\le n$ , let $C:\{0,\ldots,m-1\}\to\{0,1\}^n$ be injective, suppose every two distinct indexed words have Hamming distance $d$ , and suppose each coordinate takes different values on some two indexed words. Define

\sigma_Q((u,v),(u',v')) =\frac{1-2Q}{2}\mathbf1_{u=v}\mathbf1_{u'=v'} +\frac Q2\mathbf1_{u=u'}\mathbf1_{v=v'},

and matrices

P_C(Q)_{(k,l),(k',l')}= \prod_{i=0}^{n-1}\sigma_Q((C_k(i),C_l(i)),(C_{k'}(i),C_{l'}(i))), \qquad R_n(Q)_{(x,b),(x',b')}= \prod_{i=0}^{n-1}\sigma_Q((x_i,b),(x'_i,b')),

where $x,x'\in\{0,1\}^n$ and $b,b'$ are bits; the latter matrix uses the repetition code sending $b$ to the constant word with value $b$ . For a matrix $P$ indexed by $A\times B$ , say that it admits a Bob-copy extension if there is a positive semidefinite matrix $E$ , indexed by $(A\times B)\times B$ , such that, for every $a,a'\in A$ and $b,b'\in B$ ,

\sum_{c\in B}E_{((a,b),c),((a',b'),c)}=P_{(a,b),(a',b')}, \qquad \sum_{c\in B}E_{((a,c),b),((a',c),b')}=P_{(a,b),(a',b')}.

No trace-one condition is imposed on these matrices. For any real-parameter matrix family $F$ , define

T(F)=\sup\left(\{0\}\cup \{q\in[0,\tfrac12]:F(q)\text{ admits no Bob-copy extension}\}\right).

Then

T(P_C)\le T(R_n)\le\frac{5-\sqrt5}{10},

and, for every real $Q$ satisfying $0\le Q\le\tfrac12$ and $(5-\sqrt5)/10\le Q$ , the matrix $P_C(Q)$ admits a Bob-copy extension. The inserted $0$ makes the threshold $0$ when the set of nonextendible parameters is empty.

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