Positive signal surplus yields enough matching bases with probability tending to one

Proved

QAlgorithms.Papers.Independent.Intakenext100.P17.sifting_surplus

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Fix an overhead $\gamma>0$ and let $N_n=\lceil(4+\gamma)n\rceil$ . Assume all $N_n$ ideal signals are received. Alice and Bob independently choose uniform strings $A,B\in\{0,1\}^{N_n}$ specifying their preparation and measurement bases. Let $M(A,B)=|\{i:A_i=B_i\}|$ . Then

\lim_{n\to\infty}\Pr[M(A,B)\ge2n]=1.

Here the probability is the explicit uniform average over all ordered pairs $(A,B)$ , and a shortage of matches is an abort. This gives the sifting surplus in Protocol 3, step 6; it concerns matching bases, not the later error test.

Formalization Note The integer ceiling implements the source's signal count and agrees with it whenever $(4+\gamma)n$ is integral. The overhead is called $\gamma$ to distinguish it from an error threshold.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P17

Formal statement

namespace QAlgorithms.Papers.Independent.Intakenext100.P17

noncomputable section

open scoped ComplexConjugate

open Classical

open QAlgorithms.DopedTomography (bellVector)

open QAlgorithms.Papers.Independent.Support50.P04 (BinaryWord)

/-- PDF p.4, Protocol 3 step 6: for each fixed positive surplus gamma, the
probability that at least 2n matching-basis positions remain tends to one.
Only ideal receipt and independent uniform bases enter this combinatorial
statement. It does not assert acceptance of the subsequent error test. -/
theorem sifting_surplus (gamma : ℝ) (hgamma : 0 < gamma) :
    Filter.Tendsto (fun n : ℕ => siftingSuccess n (signalCount gamma n))
      Filter.atTop (nhds (1 : ℝ)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakenext100.P17

Source

Simple Proof of Security of the BB84 Quantum Key Distribution Protocol, arXiv:quant-ph/0003004v2, PDF p. 4, Protocol 3 step 6: enough matching bases with high probability

Read-back

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

For every real number $\gamma>0$ , put $N_n=\lceil(4+\gamma)n\rceil_{\mathbb N}$ , the least nonnegative integer at least $(4+\gamma)n$ . The theorem asserts

\lim_{n\to\infty} \frac1{2^{2N_n}} \sum_{a\in\{0,1\}^{N_n}}\sum_{b\in\{0,1\}^{N_n}} \mathbf1\!\left\{2n\le \bigl|\{i\in\{0,\ldots,N_n-1\}:a_i=b_i\}\bigr|\right\} =1.

Thus the fraction of ordered pairs of length- $N_n$ Boolean strings agreeing in at least $2n$ coordinates tends to $1$ as the natural number $n$ tends to infinity.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph