IV.A.1: photon-number thinning through random loss

Proved

QAlgorithms.Papers.Independent.Gap48.P25.photonThinning

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

prove2quantum

Let $p_A$ be a nonnegative photon-number distribution with sum one and let $0\le t\le1$ . Each of the $n$ photons independently survives with probability $t$ . Summing these independent outcomes and mixing over the input photon number produces a nonnegative normalized law

p_B^t(k)=\sum_{m=0}^\infty p_A(m+k)\binom{m+k}{k}t^k(1-t)^m.

The conditional probability for $k$ survivors from $n$ photons is zero when $k>n$ and otherwise equals $\binom nk t^k(1-t)^{n-k}$ . At $t=0$ the output is vacuum and at $t=1$ it is $p_A$ . This is an independent-loss identity, without an assertion about arbitrary adversarial loss.

Formalization Note The printed factorial on page 27 is corrected to the binomial coefficient; independent moderation of this source correction remains pending.

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)

/-- IV.A.1, PDF p.27: independent-loss thinning. Corrects the printed reciprocal
factorial k!/[n!(n-k)!] to Nat.choose; n=2,k=1 requires 2, not 1/2.
Round-one independent moderation confirmed this minimal correction. -/
theorem photonThinning (p : PhotonLaw) (t : ℝ) (ht : t ∈ Set.Icc (0 : ℝ) 1) :
    (∀ n k, survivorLaw n t k =
      if k ≤ n then (Nat.choose n k : ℝ)*t^k*(1-t)^(n-k) else 0) ∧
    (∀ k, thinned p t k = ∑' m : ℕ,
      p.mass (m+k)*(Nat.choose (m+k) k : ℝ)*t^k*(1-t)^m) ∧
    (∀ k, 0 ≤ thinned p t k) ∧ HasSum (thinned p t) 1 ∧
    thinned p 0 = vacuumLaw.mass ∧ thinned p 1 = p.mass := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 27, IV.A.1: photon-number thinning through random loss

Read-back

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

Let $p=(p_n)_{n\ge0}$ be any real sequence with $p_n\ge0$ and $\sum_{n\ge0}p_n=1$ , and let $0\le t\le1$ . For natural numbers $n,k$ , define $S_{n,t}(k)$ by summing, over all Boolean strings $b$ of length $n$ having exactly $k$ true entries, the product $\prod_{i=0}^{n-1}(t\text{ if }b_i\text{ is true, and }1-t\text{ otherwise})$ , and define $T_{p,t}(k)=\sum_{n\ge0}p_nS_{n,t}(k)$ . The assertion is that, for every $n,k$ ,

S_{n,t}(k)= \begin{cases} \binom nk t^k(1-t)^{n-k},&k\le n,\\ 0,&k>n, \end{cases}

and, for every $k$ , $T_{p,t}(k)=\sum_{m\ge0}p_{m+k}\binom{m+k}{k}t^k(1-t)^m\ge0$ . It also asserts that $\sum_{k\ge0}T_{p,t}(k)=1$ , that $T_{p,0}(0)=1$ and $T_{p,0}(k)=0$ for $k>0$ , and that $T_{p,1}(k)=p_k$ for all $k$ . The cases $n=0$ , $k=0$ , and $t\in\{0,1\}$ are included; empty products and zeroth powers equal $1$ .

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