IV.C.1–2: calibrated statistical identities, Eqs.(44)–(48)

Proved

QAlgorithms.Papers.Independent.Gap48.P25.calibratedStatistics

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

prove2quantum

Let $p_A$ be a normalized photon law, $\widetilde\nu_S>0$ , calibrated apparatus transmission $b=t_B\eta\in[0,1]$ , $0\le p_d<1/2$ , and photon forwarding and line-error probabilities $f_n,\varepsilon_n\in[0,1]$ . Assume $f_0=0$ , excluding photon creation on vacuum inputs as in footnote 57. In the restricted one-forwarded-photon model define $R_{n,p}=\widetilde\nu_Sp_A(n)f_nb$ , $R_{n,d}=\widetilde\nu_Sp_A(n)(1-f_nb)2p_d$ and $R=\sum_n(R_{n,p}+R_{n,d})>0$ . For $Y=\sum_nR_{n,p}/R$ and $\delta=(1-Y)/2$ ,

0\le Y\le1,\qquad Y={1-2p_d\widetilde\nu_S/R\over1-2p_d},\qquad {\sum_nR_{n,d}\over R}=2\delta.

The observed error is $Q=(\sum_nR_{n,p}\varepsilon_n)/R+\delta$ , or $Q=Y\varepsilon+\delta$ if $Y>0$ and $\varepsilon$ is the normalized photon-error average. These are calibrated statistical identities, without an unconditional security conclusion.

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.(44)–(48), PDF p.31: calibrated statistical ratio, with IV.C's distinct
Y_n convention and independent dark-count law. Footnote 57 excludes photon
creation on vacuum inputs, so f 0 = 0; no operational security conclusion. -/
theorem calibratedStatistics (p : PhotonLaw) (nu b pd : ℝ) (f e : ℕ → ℝ)
    (hnu : 0 < nu) (hb : b ∈ Set.Icc (0 : ℝ) 1) (hpd : 0 ≤ pd ∧ pd < 1/2)
    (hf : ∀ n, f n ∈ Set.Icc (0 : ℝ) 1) (hf0 : f 0 = 0)
    (he : ∀ n, e n ∈ Set.Icc (0 : ℝ) 1)
    (hR : 0 < calibratedTotal p nu b pd f) :
    let R := calibratedTotal p nu b pd f
    let Y := calibratedFraction p nu b pd f
    let delta := (1-Y)/2
    let photonWrong := ∑' n, calibratedPhoton p nu b f n*e n
    let dark := ∑' n, calibratedDark p nu b pd f n
    Y ∈ Set.Icc (0 : ℝ) 1 ∧ Y = (1-2*pd*nu/R)/(1-2*pd) ∧
    dark/R = 2*delta ∧ (photonWrong+dark/2)/R = (photonWrong/R)+delta ∧
    (0 < Y → (photonWrong+dark/2)/R = Y*(photonWrong/(R*Y))+delta) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 31, IV.C.1–2: calibrated statistical identities, Eqs.(44)–(48)

Read-back

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

Let $p$ be a sequence of real masses $p_n\ge0$ , indexed by all natural numbers including zero, whose series sums to $1$ . Let $\nu,b,p_d$ be real numbers with $\nu>0$ , $0\le b\le1$ , and $0\le p_d<1/2$ , and let $f,e:\mathbb N\to\mathbb R$ satisfy $0\le f_n,e_n\le1$ for every $n$ and $f_0=0$ . Define the photon and dark contributions, their total, the photon fraction, and the photon error contribution by

P_n=\nu p_n f_n b,\qquad D_n=\nu p_n(1-f_n b)(2p_d),\qquad R=\sum_{n=0}^{\infty}(P_n+D_n),\qquad Y=\frac{\sum_{n=0}^{\infty}P_n}{R},\qquad \delta=\frac{1-Y}{2},\qquad W=\sum_{n=0}^{\infty}P_ne_n,\qquad D=\sum_{n=0}^{\infty}D_n.

Assume $R>0$ . Then

0\le Y\le1,\qquad Y=\frac{1-2p_d\nu/R}{1-2p_d},\qquad \frac{D}{R}=2\delta,\qquad \frac{W+D/2}{R}=\frac WR+\delta.

If additionally $Y>0$ , then $(W+D/2)/R=Y\bigl(W/(RY)\bigr)+\delta$ . The unconditional conclusions allow $Y=0$ ; the final identity is asserted only under the additional strict positivity condition.

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