III A / Appendix A: exact repetition threshold and Alice/Bob equivalence, (9), (A1)–(A3)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.repetitionThreshold

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

prove2quantum

Let $n\ge1$ , $R_n=\{0^n,1^n\}$ , and $0\le Q\le\tfrac12$ . Let $P_B(Q)$ be the unnormalized six-state operator after Bob filters on $R_n$ , and let $P_{AB}(Q)$ be the operator when both parties filter on that code. Define

F_n(Q)=4Q^{2n}-4Q^n(1-Q)^n+(1-2Q)^{2n}.

Then

\mathrm{Ext}_B(P_B(Q))\Longleftrightarrow \mathrm{Ext}_B(P_{AB}(Q))\Longleftrightarrow F_n(Q)\le0.

The thresholds in the two regimes coincide, and their common value is the least root of $F_n$ in $[0,\tfrac12]$ . This specifies the first transition root, because $\tfrac12$ is also a root. The endpoint $Q=\tfrac12$ remains included and is extendable. The result analytically identifies the repetition-code threshold without assuming that Alice's filtering is reversible for general codes.

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 pp.4–5, (9), and p.10, (A1)–(A3): exact iff, both filtering regimes,
and the least root (not the extraneous root at 1/2). -/
theorem repetitionThreshold {n : ℕ} (hn : 1 ≤ n) :
    (∀ Q : ℝ, 0 ≤ Q → Q ≤ 1 / 2 →
      (BobExtendible (bobState (repetition (Fin n)) Q) ↔
        BobExtendible (bothState (repetition (Fin n)) Q)) ∧
      (BobExtendible (bothState (repetition (Fin n)) Q) ↔
        repetitionPolynomial n Q ≤ 0)) ∧
    bothThreshold (repetition (Fin n)) = bobThreshold (repetition (Fin n)) ∧
    IsLeast {q : ℝ | 0 ≤ q ∧ q ≤ 1 / 2 ∧ repetitionPolynomial n q = 0}
      (bobThreshold (repetition (Fin n))) := 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. 10, III A / Appendix A: exact repetition threshold and Alice/Bob equivalence, (9), (A1)–(A3)

Read-back

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

Let $n\ge1$ , and let $R:\{0,1\}\to\{0,1\}^{n}$ assign to $b$ the constant string $\bar b$ . Define

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

and the two complex matrix families

B_Q((a,b),(a',b')) =\prod_{i=0}^{n-1}s_Q(a_i,b;a'_i,b'),\qquad T_Q((b,c),(b',c')) =\prod_{i=0}^{n-1}s_Q(b,c;b',c').

These are respectively the matrices obtained by selecting repetition-code strings on the second subsystem alone and on both subsystems. Say that a matrix on $A\times B$ is extendible when it has a positive semidefinite extension on $(A\times B)\times B$ whose partial traces over either copy of $B$ both equal that matrix; no trace-one condition is imposed. Put

f_n(q)=4q^{2n}-4q^n(1-q)^n+(1-2q)^{2n},

and define $b_B=\sup(\{0\}\cup\{q\in[0,1/2]:B_q\text{ is not extendible}\})$ and $b_T=\sup(\{0\}\cup\{q\in[0,1/2]:T_q\text{ is not extendible}\})$ . The theorem asserts that for every $Q\in[0,1/2]$ ,

B_Q\text{ is extendible}\ \Longleftrightarrow\ T_Q\text{ is extendible}, \qquad T_Q\text{ is extendible}\ \Longleftrightarrow\ f_n(Q)\le0.

It also asserts $b_T=b_B$ and that $b_B$ is the least zero of $f_n$ in $[0,1/2]$ : explicitly, $0\le b_B\le1/2$ , $f_n(b_B)=0$ , and $b_B\le q$ for every $q\in[0,1/2]$ satisfying $f_n(q)=0$ .

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