IV.B.4: weak-laser, zero-error quadratic approximation

Proved

QAlgorithms.Papers.Independent.Gap48.P25.zeroErrorOptimum

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

prove2quantum

Write $s=tt_B\eta\in(0,1]$ for the total transmission. In the zero-error weak-pulse truncation with negligible higher photons and dark counts and perfect error correction, the normalized rate proxy is $q_s(\mu)=\mu s-\mu^2/2$ for $\mu\ge0$ . It has the unique maximum

\mu_0=s,\qquad \max_{\mu\ge0}q_s(\mu)=s^2/2.

Consequently, for $s=tb$ with other transmission factors $b$ fixed, the optimized proxy equals $t^2b^2/2$ . The source's photon-number approximations define this quadratic proxy; no exact Poisson optimization is asserted.

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.B.4, PDF p.29: exact optimization of the zero-error weak-pulse proxy. -/
theorem zeroErrorOptimum (s : ℝ) (hs : 0 < s) (hs1 : s ≤ 1) :
    zeroProxy s s = s^2/2 ∧
    (∀ mu : ℝ, 0 ≤ mu → zeroProxy s mu ≤ s^2/2) ∧
    (∀ mu : ℝ, 0 ≤ mu → (zeroProxy s mu = s^2/2 ↔ mu = s)) ∧
    (∀ t b : ℝ, (t*b)^2/2 = t^2*(b^2/2)) := 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: weak-laser, zero-error quadratic approximation

Read-back

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

For every real $s$ with $0<s\le1$ , define $Z(s,\mu)=\mu s-\mu^2/2$ . Then $Z(s,s)=s^2/2$ ; for every real $\mu\ge0$ , $Z(s,\mu)\le s^2/2$ , with equality if and only if $\mu=s$ . The range of $\mu$ has no upper bound. In addition, for all real $t,b$ , without sign or size restrictions,

\frac{(tb)^2}{2}=t^2\frac{b^2}{2}.

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