Appendix B.2.b: Bell-measurement error and repeater yield, Eq.(B3)

Proved

QAlgorithms.Papers.Independent.Gap48.P25.bellErrorRate

by Goku · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $R_2\ge0$ be the mean-cycle detection rate and let $F\in[0,1]$ be the Bell measurement fidelity. The desired Bell state has probability $F$ and each other Bell state has probability $(1-F)/3$ . One wrong Bell state preserves the bit correlation and the other two reverse it. The error and assigned signed one-way perfect-EC toy yield are

\varepsilon={2\over3}(1-F),\qquad K_2=R_2[1-2h(\varepsilon)],\qquad K_2^+=R_2\max\{1-2h(\varepsilon),0\}.

There is a unique $q_*\in(0,1/2)$ with $h(q_*)=1/2$ . In the useful branch $F\ge1/4$ , $K_2>0$ exactly when $R_2>0$ and $F>1-3q_*/2$ . This gives the source's threshold implicitly, without treating its approximate 83.5 percent decimal as exact.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Gap48_P25

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Gap48.P25

open scoped BigOperators ComplexConjugate

open Filter

open QAlgorithms.Papers.Independent.Claimed50.P08 (classicalEntropy)

/-- Eq.(B3), PDF p.47: computed Bell error and assigned mean-cycle yield.
The approximate decimal threshold is replaced by its implicit entropy definition. -/
theorem bellErrorRate (R F : ℝ) (hR : 0 ≤ R) (hF : F ∈ Set.Icc (0 : ℝ) 1) :
    (∀ i, 0 ≤ bellLaw F i) ∧ (∑ i : Fin 4, bellLaw F i) = 1 ∧
    bellError F = (2/3)*(1-F) ∧
    repeaterKey R F = R*(1-2*QAlgorithms.binEntropy2 ((2/3)*(1-F))) ∧
    max (repeaterKey R F) 0 = R*max (1-2*QAlgorithms.binEntropy2 ((2/3)*(1-F))) 0 ∧
    ∃ q : ℝ, 0 < q ∧ q < 1/2 ∧ QAlgorithms.binEntropy2 q = 1/2 ∧
      (∀ z : ℝ, z ∈ Set.Icc (0 : ℝ) (1/2) → (QAlgorithms.binEntropy2 z = 1/2 ↔ z = q)) ∧
      (1/4 ≤ F → (0 < repeaterKey R F ↔ 0 < R ∧ 1-(3/2)*q < F)) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 47, Appendix B.2.b: Bell-measurement error and repeater yield, Eq.(B3)

Read-back

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

For every real $R\ge0$ and $F\in[0,1]$ , define $P_F(0)=F$ and $P_F(i)=(1-F)/3$ for $i=1,2,3$ , let $e_F=\sum_{i=2}^{3}P_F(i)$ , and let $H(q)=[-q\log q-(1-q)\log(1-q)]/\log2$ , with $0\log0=0$ . Define $K(R,F)=R(1-H(e_F)-H(e_F))$ . Then all four $P_F(i)$ are nonnegative, their sum is $1$ , and

e_F=\frac23(1-F),\qquad K(R,F)=R\left(1-2H\left(\frac23(1-F)\right)\right),\qquad \max\{K(R,F),0\}=R\max\left\{1-2H\left(\frac23(1-F)\right),0\right\}.

There exists a real $q$ with $0<q<1/2$ and $H(q)=1/2$ , such that for every $z\in[0,1/2]$ , $H(z)=1/2$ if and only if $z=q$ , and, if $F\ge1/4$ ,

K(R,F)>0\iff R>0\ \text{and}\ F>1-\frac32q.

The assumptions permit $R=0$ and $F=0$ or $1$ ; the final positivity equivalence is asserted only under $F\ge1/4$ .

Human review

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

View graph