Prove2Me

III A: monotone repetition thresholds and Chau limit, (10)

Open
QAlgorithms.Papers.Independent.Intakethird100.P30.repetitionLimit

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

prove2quantum

For n≥1n\ge1, let qn=QRn∗q_n=Q_{R_n}^* denote the Bob-only repetition-code threshold. Set rn=(1/4)1/nr_n=(1/4)^{1/n}, an=4rn+1a_n=4r_n+1, and

q~n=an−an2−4rnan2an,c=5−510.\widetilde q_n=\frac{a_n-\sqrt{a_n^2-4r_na_n}}{2a_n}, \qquad c=\frac{5-\sqrt5}{10}.

The sequence (qn)n≥1(q_n)_{n\ge1} is nondecreasing, and

lim⁡n→∞q~n=c,lim⁡n→∞(qn−q~n)=0,lim⁡n→∞qn=c,qn≤c.\lim_{n\to\infty}\widetilde q_n=c,\qquad \lim_{n\to\infty}(q_n-\widetilde q_n)=0,\qquad \lim_{n\to\infty}q_n=c,\qquad q_n\le c.

No convergence rate is asserted. Positive block length is essential for the reciprocal exponent; the formal sequence is indexed by n=k+1n=k+1. This establishes that finite repetition codes approach Chau's threshold.

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.5, (10): monotone positive-length thresholds, the explicit approximation,
its limit, and the Chau limit. No convergence rate is asserted. -/
theorem repetitionLimit :
    Monotone (fun k : ℕ => bobThreshold (repetition (Fin (k + 1)))) ∧
    Filter.Tendsto (fun k : ℕ => repetitionApprox (k + 1)) Filter.atTop (nhds chau) ∧
    Filter.Tendsto (fun k : ℕ => bobThreshold (repetition (Fin (k + 1))) -
      repetitionApprox (k + 1)) Filter.atTop (nhds 0) ∧
    Filter.Tendsto (fun k : ℕ => bobThreshold (repetition (Fin (k + 1))))
      Filter.atTop (nhds chau) ∧
    (∀ n : ℕ, 1 ≤ n → bobThreshold (repetition (Fin n)) ≤ chau) := 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. 5, III A: monotone repetition thresholds and Chau limit, (10)
Read-back

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

For each integer n≥1n\ge1, let Cn:{0,1}→{0,1}nC_n:\{0,1\}\to\{0,1\}^n send a bit to the constant word with that bit. Define the matrix Bn(q)B_n(q), indexed by pairs (a,b)∈{0,1}n×{0,1}(a,b)\in\{0,1\}^n\times\{0,1\}, by

Bn(q)(a,b),(a′,b′)=∏i=0n−1(1−2q21ai=b1ai′=b′+q21ai=ai′1b=b′).B_n(q)_{(a,b),(a',b')}= \prod_{i=0}^{n-1} \left(\frac{1-2q}{2}\mathbf1_{a_i=b}\mathbf1_{a'_i=b'} +\frac q2\mathbf1_{a_i=a'_i}\mathbf1_{b=b'}\right).

Call a matrix PP indexed by X×YX\times Y Bob-extendible if there exists a positive semidefinite matrix RR, indexed by (X×Y)×Y(X\times Y)\times Y, such that, for every x,x′∈Xx,x'\in X and y,y′∈Yy,y'\in Y,

∑c∈YR((x,y),c),((x′,y′),c)=P(x,y),(x′,y′)=∑c∈YR((x,c),y),((x′,c),y′).\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')}.

No trace-one condition is part of this definition. Set

bn=sup⁡({0}∪{q∈[0,12]:Bn(q) is not Bob-extendible}),rn=(14)1/n,an=4rn+1,un=an−an2−4rnan2an,c=5−510.b_n=\sup\bigl(\{0\}\cup\{q\in[0,\tfrac12]:B_n(q)\text{ is not Bob-extendible}\}\bigr), \quad r_n=(\tfrac14)^{1/n},\quad a_n=4r_n+1,\quad u_n=\frac{a_n-\sqrt{a_n^2-4r_na_n}}{2a_n}, \quad c=\frac{5-\sqrt5}{10}.

The declaration asserts all five facts: bk+1≤bℓ+1b_{k+1}\le b_{\ell+1} for every k,ℓ∈Nk,\ell\in\mathbb N with k≤ℓk\le\ell; uk+1→cu_{k+1}\to c; bk+1−uk+1→0b_{k+1}-u_{k+1}\to0; bk+1→cb_{k+1}\to c, with all three limits taken as k→∞k\to\infty through natural numbers; and bn≤cb_n\le c for every natural number n≥1n\ge1. These assertions concern only positive word lengths, including length 11.

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