Parallel attempts: probability of one usable external link

Proved

QAlgorithms.Papers.Independent.Intakethird100.P45.effectiveLink

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

prove2quantum

Assume the paper's heralded-loss model: a successful elementary attempt produces a perfect EPR pair. Let $S\ge1$ independent optical attempts across one physical edge each succeed with probability $p_0\in[0,1]$ . The neighboring repeaters retain at most one successful pair, discarding additional successes. Then the probability $p$ of a usable external link in that slot is

p=1-(1-p_0)^S.

This reduces parallel optical attempts to the single-pair-per-edge model used by the routing protocols.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P45

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P45

open scoped BigOperators

noncomputable section

/-- PDF p.4: the usable-link probability is `1-(1-p0)^S`, including `p0=0,1`. -/
theorem effectiveLink (S : ℕ) (hS : 0 < S) (p0 : ℝ)
    (hp0 : 0 ≤ p0) (hp1 : p0 ≤ 1) :
    retainedLinkProbability S p0 = 1 - (1 - p0) ^ S := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P45

Source

Routing entanglement in the quantum internet, arXiv:1708.07142v2, PDF p. 4, §II.A: parallel optical attempts give the effective link probability

Read-back

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

For every natural number $S>0$ and every real number $p_0$ satisfying $0\le p_0\le1$ , the sum over all Boolean assignments $f$ on $\{0,\ldots,S-1\}$ , in which an assignment contributes $\prod_{i=0}^{S-1}w_i$ when at least one flag is true and $0$ otherwise, with $w_i=p_0$ for a true flag and $w_i=1-p_0$ for a false flag, equals

1-(1-p_0)^S.

The hypotheses include $p_0=0$ and $p_0=1$ , but exclude $S=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