IV.D: SARG04 acceptance and conditional error, Eqs.(53)–(54)

Proved

QAlgorithms.Papers.Independent.Gap48.P25.sargAcceptance

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

prove2quantum

Consider the displayed SARG04 example in IV.D, with source clock $\nu_S\ge0$ , photon probability $p_A(n)\in[0,1]$ , forwarding probability $f_n\in[0,1]$ and channel perturbation $\widetilde\varepsilon_n\in[0,1]$ . Bob's bases are equally likely. In the same-basis branch the accepted minus result has probability $\widetilde\varepsilon_n$ and is wrong; in the other-basis branch it has probability $1/2$ and is correct, the assumption of footnote 58. With $\widetilde\nu_S=\nu_S/2$ ,

R_n=\widetilde\nu_Sp_A(n)f_n(1/2+\widetilde\varepsilon_n),\qquad R_n^w=\widetilde\nu_Sp_A(n)f_n\widetilde\varepsilon_n.

For a nonempty detection class the conditional error is $\varepsilon_n=\widetilde\varepsilon_n/(1/2+\widetilde\varepsilon_n)$ . Acceptance is nondecreasing when comparing perturbations in $[0,1]$ . This states the source's explicit symmetric example, with its required wrong-basis assumption.

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)

/-- Eqs.(53)–(54), footnote 58, PDF p.32. Conditional error is asserted only
for a nonempty detection class; both source basis assumptions are in sargAccepted. -/
theorem sargAcceptance (nu pa f e : ℝ) (hnu : 0 ≤ nu)
    (hpa : pa ∈ Set.Icc (0 : ℝ) 1) (hf : f ∈ Set.Icc (0 : ℝ) 1)
    (he : e ∈ Set.Icc (0 : ℝ) 1) :
    sargAccepted nu pa f e = (nu/2)*pa*f*(1/2+e) ∧
    sargWrong nu pa f e = (nu/2)*pa*f*e ∧
    (0 < nu*pa*f → sargWrong nu pa f e/sargAccepted nu pa f e = e/(1/2+e)) ∧
    (∀ e2 : ℝ, e2 ∈ Set.Icc (0 : ℝ) 1 → e ≤ e2 →
      sargAccepted nu pa f e ≤ sargAccepted nu pa f e2) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 32, IV.D: SARG04 acceptance and conditional error, Eqs.(53)–(54)

Read-back

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

For all real $\nu,p_a,f,e$ satisfying $\nu\ge0$ and $p_a,f,e\in[0,1]$ , define $A(e)=\nu p_af(e/2+1/4)$ and $W(e)=\nu p_af(e/2)$ . Then

A(e)=\frac{\nu}{2}p_af\left(\frac12+e\right), \qquad W(e)=\frac{\nu}{2}p_afe.

If $\nu p_af>0$ , then $W(e)/A(e)=e/(1/2+e)$ . Furthermore, every real $e_2\in[0,1]$ with $e\le e_2$ satisfies $A(e)\le A(e_2)$ . Zero values of $\nu,p_a$ , or $f$ are allowed in the unconditional assertions; the ratio identity requires the stated strict positivity hypothesis.

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