IV.B.4: approximate decoy optimization, Eqs.(38)–(39)

Proved

QAlgorithms.Papers.Independent.Gap48.P25.decoyOptimum

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

prove2quantum

Let $\widetilde\nu_S>0$ and $s\in(0,1]$ , $Q\in[0,1]$ and $h=h(Q)<1/2$ , in bits. Under the source's honest-rate, exact-parameter, dominant-intensity decoy estimate with perfect error correction and negligible dark counts, replacing $e^{-\mu}$ by $1-\mu$ gives $q(\mu)=\widetilde\nu_Ss\mu[(1-\mu)(1-h)-h]$ . Its unique maximum on $\mu\ge0$ is

\mu_*={1\over2}\left(1-{h\over1-h}\right)>0,\qquad \max q={\widetilde\nu_Ss\mu_*(1-2h)\over2}.

The other root is $2\mu_*$ and the optimized proxy is linear in $s$ , hence in line transmission with other factors fixed. These are statements about the quadratic approximation, not arbitrary physical operating intensities.

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.(38)–(39), PDF p.30: decoy proxy optimizer, critical root and linear scaling. -/
theorem decoyOptimum (nu s Q : ℝ) (hnu : 0 < nu) (hs : 0 < s) (hs1 : s ≤ 1)
    (hQ : Q ∈ Set.Icc (0 : ℝ) 1) (hh : QAlgorithms.binEntropy2 Q < 1/2) :
    0 < decoyOptimizer Q ∧
    decoyProxy nu s Q (decoyOptimizer Q) = nu*s*decoyOptimizer Q*(1-2*QAlgorithms.binEntropy2 Q)/2 ∧
    (∀ mu : ℝ, 0 ≤ mu → decoyProxy nu s Q mu ≤ decoyProxy nu s Q (decoyOptimizer Q)) ∧
    (∀ mu : ℝ, 0 ≤ mu → (decoyProxy nu s Q mu =
      decoyProxy nu s Q (decoyOptimizer Q) ↔ mu = decoyOptimizer Q)) ∧
    decoyProxy nu s Q (2*decoyOptimizer Q) = 0 ∧
    (∀ t b : ℝ, decoyProxy nu (t*b) Q (decoyOptimizer Q) = t*decoyProxy nu b Q (decoyOptimizer Q)) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 30, IV.B.4: approximate decoy optimization, Eqs.(38)–(39)

Read-back

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

Let $\nu,s,Q$ be real numbers with $\nu>0$ , $0<s\le1$ , $0\le Q\le1$ , and $H(Q)<1/2$ , where $H(x)=[-x\log x-(1-x)\log(1-x)]/\log2$ is binary entropy, with endpoint products $0\log0$ interpreted as zero. Put $h=H(Q)$ and define

m_*=\frac{1-h/(1-h)}{2}, \qquad D(r,\mu)=\nu r\mu\bigl((1-\mu)(1-h)-h\bigr).

Then $m_*>0$ , $D(s,m_*)=\nu s m_*(1-2h)/2$ , and for every real $\mu\ge0$ , $D(s,\mu)\le D(s,m_*)$ , with equality if and only if $\mu=m_*$ . Also $D(s,2m_*)=0$ , and for every pair of real numbers $t,b$ , without sign or size restrictions, $D(tb,m_*)=tD(b,m_*)$ . No upper bound on $\mu$ , and no additional restriction $Q\le1/2$ , is assumed.

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