Appendix B.2.b: direct pair-link rate, Eq.(B1)

Proved

QAlgorithms.Papers.Independent.Gap48.P25.directLink

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

prove2quantum

In Appendix B's perfect-pair, noiseless-channel toy model, let $\nu_S>0$ be the source clock, $t\in[0,1]$ total pair propagation transmission and $0<\eta\le1$ each endpoint detector's efficiency. Dark counts, dead times and other nuisances are absent. The independent propagation and two detection factors define a nonnegative normalized round law. Its coincidence rate, equal to the toy model's noiseless secret-key rate, is

K_1=R_1=\nu_St\eta^2.

The channel factor is the total path transmission $t$ , whereas the two endpoint detections contribute $\eta^2$ . In particular zero propagation transmission gives zero rate.

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.(B1), PDF p.46: direct-link coincidence rate, with eta^2 and total loss t. -/
theorem directLink (nu t eta : ℝ) (hnu : 0 < nu) (ht : t ∈ Set.Icc (0 : ℝ) 1)
    (heta : 0 < eta ∧ eta ≤ 1) :
    (∀ b, 0 ≤ directLaw t eta b) ∧ (∑ b : Fin 3 → Bool, directLaw t eta b) = 1 ∧
    directRate nu t eta = nu*t*eta^2 := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 46, Appendix B.2.b: direct pair-link rate, Eq.(B1)

Read-back

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

For every real $\nu>0$ , $t\in[0,1]$ , and $0<\eta\le1$ , define, for each Boolean triple $b=(b_0,b_1,b_2)$ ,

P(b)= \begin{cases}t&b_0=\mathrm{true}\\1-t&b_0=\mathrm{false}\end{cases} \prod_{i=1}^{2} \begin{cases}\eta&b_i=\mathrm{true}\\1-\eta&b_i=\mathrm{false}.\end{cases}

Then $P(b)\ge0$ for every triple, the sum of $P(b)$ over all eight triples is $1$ , and the quantity $\nu\sum_{b:\,\forall i,\ b_i=\mathrm{true}}P(b)$ equals $\nu t\eta^2$ . The cases $t=0$ , $t=1$ , and $\eta=1$ are included.

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