Direct random-pair verification requires exponential resources

Proved

QAlgorithms.Papers.Independent.Intakenext100.P87.direct_sampling_cost

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

prove2quantum

Let $N\ge1$ and $0\le m<N$ . Among $N$ pairs, exactly one fixed pair is a nonsinglet and all others are singlets. Test a uniformly chosen $m$ -element subset. Write $p_{\rm miss}$ for the probability the nonsinglet remains untested. Then

p_{\rm miss}=\frac{N-m}{N}\ge\frac1N.

For $k\ge0$ , the requirement $p_{\rm miss}\le e^{-k}$ therefore entails $N\ge e^k$ and $m\ge(1-e^{-k})N$ . This is a resource lower bound for this direct-testing scheme.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P87

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakenext100.P87

open scoped Matrix ComplexConjugate

open QAlgorithms.Measurements

/-- PDF p.7: the direct scheme needs exponentially many pairs to make its
one-defective-pair cheating probability at most exp(-k); m=N is excluded. -/
theorem direct_sampling_cost (N m : ℕ) (hm : m < N) (bad : Fin N) :
    directMissProbability N m bad = (N - m : ℕ) / (N : ℝ) ∧
    1 / (N : ℝ) ≤ directMissProbability N m bad ∧
    ∀ k : ℝ, 0 ≤ k → directMissProbability N m bad ≤ Real.exp (-k) →
      Real.exp k ≤ (N : ℝ) ∧
      (1 - Real.exp (-k)) * (N : ℝ) ≤ (m : ℝ) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P87

end

Source

Unconditional Security Of Quantum Key Distribution Over Arbitrarily Long Distances, arXiv:quant-ph/9803006v5, PDF p. 7, Direct random-pair verification requires exponential resources

Read-back

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

For every pair of natural numbers $N,m$ with $m<N$ , and every $b\in\{0,\ldots,N-1\}$ , let $p$ be the number of $m$ -element subsets of $\{0,\ldots,N-1\}$ omitting $b$ , divided by the total number of $m$ -element subsets. Then all of the following hold:

p=\frac{N-m}{N}, \qquad \frac1N\leq p, \qquad \forall k\in\mathbb R,\quad \bigl(0\leq k\ \text{and}\ p\leq e^{-k}\bigr) \Longrightarrow \bigl(e^k\leq N\ \text{and}\ (1-e^{-k})N\leq m\bigr).

The numerator $N-m$ in the first equality is natural-number subtraction, which agrees with ordinary subtraction under $m<N$ . These hypotheses ensure $N>0$ ; they permit $m=0$ , in which case $p=1$ .

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