Prove2Me

IV.B.4: ideal single-photon rate estimate, Eq.(35)

Proved
QAlgorithms.Papers.Independent.Gap48.P25.singlePhotonModel

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

prove2quantum

In the ideal single-photon model of IV.B.4, let ν~S>0\widetilde\nu_S>0 be the sifted source clock, t,tB,η∈[0,1]t,t_B,\eta\in[0,1] the line, apparatus and detector transmissions, and Q∈[0,1]Q\in[0,1] the error. Assume negligible dark counts, honest model detection rate R=ν~SttBηR=\widetilde\nu_Stt_B\eta, information cost h(Q)h(Q) and perfect error-correction leakage h(Q)h(Q), where hh is binary entropy in bits. The assigned signed rate and its physical nonnegative part obey

Kmodel=ν~SttBη[1−2h(Q)],Kmodel+=ν~SttBηmax⁡{1−2h(Q),0}.K_{\rm model}=\widetilde\nu_Stt_B\eta[1-2h(Q)],\qquad K_{\rm model}^{+}=\widetilde\nu_Stt_B\eta\max\{1-2h(Q),0\}.

This is the identity of the explicitly idealized rate model underlying the source's approximate equation, without a quantitative approximation assertion for an arbitrary device.

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.(35), PDF p.29: ideal single-photon model identity, with honest detection
rate, negligible dark counts, information cost h(Q) and optimal EC. -/
theorem singlePhotonModel (nu t tB eta Q : ℝ) (hnu : 0 < nu)
    (ht : t ∈ Set.Icc (0 : ℝ) 1) (htB : tB ∈ Set.Icc (0 : ℝ) 1)
    (heta : eta ∈ Set.Icc (0 : ℝ) 1) (hQ : Q ∈ Set.Icc (0 : ℝ) 1) :
    signedRate (nu*t*tB*eta) (QAlgorithms.binEntropy2 Q) (QAlgorithms.binEntropy2 Q) =
      nu*t*tB*eta*(1-2*QAlgorithms.binEntropy2 Q) ∧
    max (signedRate (nu*t*tB*eta) (QAlgorithms.binEntropy2 Q) (QAlgorithms.binEntropy2 Q)) 0 =
      nu*t*tB*eta*max (1-2*QAlgorithms.binEntropy2 Q) 0 := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end
Source
The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 29, IV.B.4: ideal single-photon rate estimate, Eq.(35)
Read-back

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

For every real ν>0\nu>0 and t,tB,η,Q∈[0,1]t,t_B,\eta,Q\in[0,1], let H(q)=[−qlog⁡q−(1−q)log⁡(1−q)]/log⁡2H(q)=[-q\log q-(1-q)\log(1-q)]/\log 2 denote binary entropy, with 0log⁡0=00\log0=0, and define S(R,ℓ,i)=R(1−ℓ−i)S(R,\ell,i)=R(1-\ell-i). Then

S(νttBη,H(Q),H(Q))=νttBη(1−2H(Q)),max⁡{S(νttBη,H(Q),H(Q)),0}=νttBηmax⁡{1−2H(Q),0}.S(\nu t t_B\eta,H(Q),H(Q))=\nu t t_B\eta(1-2H(Q)), \qquad \max\{S(\nu t t_B\eta,H(Q),H(Q)),0\} =\nu t t_B\eta\max\{1-2H(Q),0\}.

The parameters t,tB,η,Qt,t_B,\eta,Q may equal either endpoint of their intervals; in particular, the prefactor may be zero.

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