IV A: fixed-size simplex families approach the Chau threshold

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.simplexDistanceLimit

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

prove2quantum

Fix a number of codewords $m\ge2$ . For every integer $j\ge0$ , let $C_j$ be an actual equidistant code of $m$ distinct binary words of length $n_j\ge1$ , without constant columns, and common distance $1\le d_j\le n_j$ . Assume $d_j\to\infty$ . Write $q_j$ for its symmetric-extendability threshold after Alice and Bob both filter on $C_j$ , and $r_j$ for the repetition-code threshold at length $n_j$ . Then

\lim_{j\to\infty}q_j=\frac{5-\sqrt5}{10},\qquad \lim_{j\to\infty}(q_j-r_j)=0.

The family ranges only through feasible codes; existence at every distance and uniformity over unbounded code size are not claimed. Fixing $m$ follows the source's distance-limit reading, since the common factor depending on $n_j-d_j$ cancels when the Bell-diagonal operator is normalized.

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: fix m and range through actual feasible equidistant codes with d→infinity.
Neither existence at every distance nor uniform convergence in unbounded m is asserted. -/
theorem simplexDistanceLimit {m : ℕ} (hm : 2 ≤ m)
    (n d : ℕ → ℕ) (C : (j : ℕ) → Fin m → Qubits (n j))
    (hn : ∀ j, 1 ≤ n j) (hd0 : ∀ j, 1 ≤ d j) (hdn : ∀ j, d j ≤ n j)
    (hC : ∀ j, Function.Injective (C j)) (hd : ∀ j, Equidistant (C j) (d j))
    (hcols : ∀ j, NoConstantColumns (C j)) (hinfty : Filter.Tendsto d Filter.atTop Filter.atTop) :
    Filter.Tendsto (fun j => bothThreshold (C j)) Filter.atTop (nhds chau) ∧
    Filter.Tendsto (fun j => bothThreshold (C j) - bobThreshold (repetition (Fin (n j))))
      Filter.atTop (nhds 0) := 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: fixed-size simplex families approach the Chau threshold

Read-back

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

For every natural number $m\ge2$ , every pair of sequences $n,d:\mathbb N\to\mathbb N$ , and every sequence of maps $C_j:\{0,\ldots,m-1\}\to\{0,1\}^{n(j)}$ , suppose that, for every $j$ , $n(j)\ge1$ , $1\le d(j)\le n(j)$ , $C_j$ is injective, every two distinct indexed words of $C_j$ have Hamming distance exactly $d(j)$ , and each coordinate takes different values on some two indexed words. Suppose also that $d(j)\to+\infty$ , meaning that every natural lower bound is eventually satisfied. To specify the thresholds, set

\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 define

P_j(q)_{(k,l),(k',l')}= \prod_{i=0}^{n(j)-1}\sigma_q((C_j(k)_i,C_j(l)_i),(C_j(k')_i,C_j(l')_i)), \qquad R_j(q)_{(x,b),(x',b')}= \prod_{i=0}^{n(j)-1}\sigma_q((x_i,b),(x'_i,b')),

where $x,x'$ range over $n(j)$ -bit words and $b,b'$ over bits. A matrix $P$ indexed by $A\times B$ is extendible here precisely when there exists a positive semidefinite matrix $E$ indexed by $(A\times B)\times B$ satisfying

\sum_cE_{((a,b),c),((a',b'),c)} = \sum_cE_{((a,c),b),((a',c),b')} =P_{(a,b),(a',b')}

for all $a,a',b,b'$ ; no normalization is required. Write

T(F)=\sup\left(\{0\}\cup\{q\in[0,\tfrac12]:F(q)\text{ is not extendible}\}\right).

Then, as $j\to\infty$ ,

T(P_j)\longrightarrow\frac{5-\sqrt5}{10}, \qquad T(P_j)-T(R_j)\longrightarrow0.

The threshold is $0$ if its 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