A fixed chain: unconditional one-slot success probability

Proved

QAlgorithms.Papers.Independent.Intakethird100.P45.pathSuccess

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

prove2quantum

Fix a chain of $k\ge1$ edges and prescribe its $k-1$ internal Bell-state measurements before the success flags are observed. External links independently produce perfect EPR pairs with probability $p\in[0,1]$ , and the prescribed BSMs have independent heralded success probability $q\in[0,1]$ , independent of the external attempts. Memories last one slot, each is used at most once, and the two terminals retain their halves. The probability $P_k$ of delivering one ebit after the external and internal phases, and hence its expected delivered count per slot, is

P_k=p^kq^{k-1}.

This is the unconditional linear-chain rate; it includes external failures, unlike the conditional path yields in global routing.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P45

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P45

open scoped BigOperators

noncomputable section

/-- PDF pp.4,7: the fixed `k`-edge chain delivers one ebit with probability
`p^k q^(k-1)`, also its expected delivered count. Terminals do not swap. -/
theorem pathSuccess (k : ℕ) (hk : 0 < k) (p q : ℝ)
    (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) :
    chainProbability k p q = p ^ k * q ^ (k - 1) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P45

Source

Routing entanglement in the quantum internet, arXiv:1708.07142v2, PDF p. 4, §II.A and §II.B.2: single-chain success probability and rate

Read-back

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

For every natural number $k>0$ and every pair of real numbers $p,q$ satisfying $0\le p\le1$ and $0\le q\le1$ , consider the sum over external Boolean assignments on $k$ indices and internal Boolean assignments on $k-1$ indices. Each pair contributes $0$ unless every flag in both assignments is true; otherwise, it contributes the product of the external weights $p$ for true and $1-p$ for false, multiplied by the product of the internal weights $q$ for true and $1-q$ for false. This sum equals

p^kq^{k-1}.

The parameter values $0$ and $1$ are allowed for both $p$ and $q$ . In particular, $k=1$ is included: the internal assignment is empty, its condition holds vacuously, and its product is $q^0=1$ , including when $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