IV.B.4: approximate no-decoy optimization, Eqs.(36)–(37)

Proved

QAlgorithms.Papers.Independent.Gap48.P25.noDecoyOptimum

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

prove2quantum

Let $\widetilde\nu_S>0$ and $s\in(0,1]$ , $0\le Q<1/4$ , $A=1-h(2Q)>0$ and $F(Q)=1-h(2Q)-h(Q)\ge0$ , with entropy in bits. Using the source's substitution $Q/Y_1\approx2Q$ only inside entropy defines the quadratic proxy $q(\mu)=\widetilde\nu_S[\mu sF(Q)-\mu^2 A/2]$ . On $\mu\ge0$ its unique optimizer and maximum are

\mu_*={sF(Q)\over A},\qquad \max q={\widetilde\nu_Ss\mu_*F(Q)\over2}={\widetilde\nu_Ss^2F(Q)^2\over2A}.

Also $q(2\mu_*)=0$ , including the degenerate $F=0$ case, where the optimizer is zero. The optimized proxy has quadratic transmission scaling. This is exact optimization of the displayed approximation, without a certified approximation error or an exact physical optimizing intensity.

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.(36)–(37), PDF p.29: source quadratic's maximum and optimizer, with
informative entropy domain. The equality F=0 is allowed. -/
theorem noDecoyOptimum (nu s Q : ℝ) (hnu : 0 < nu) (hs : 0 < s) (hs1 : s ≤ 1)
    (hQ : 0 ≤ Q ∧ Q < 1/4) (hA : 0 < 1-QAlgorithms.binEntropy2 (2*Q))
    (hF : 0 ≤ noDecoyF Q) :
    0 ≤ noDecoyOptimizer s Q ∧
    noDecoyProxy nu s Q (noDecoyOptimizer s Q) = nu*s*noDecoyOptimizer s Q*noDecoyF Q/2 ∧
    (∀ mu : ℝ, 0 ≤ mu → noDecoyProxy nu s Q mu ≤ noDecoyProxy nu s Q (noDecoyOptimizer s Q)) ∧
    (∀ mu : ℝ, 0 ≤ mu → (noDecoyProxy nu s Q mu =
      noDecoyProxy nu s Q (noDecoyOptimizer s Q) ↔ mu = noDecoyOptimizer s Q)) ∧
    noDecoyProxy nu s Q (2*noDecoyOptimizer s Q) = 0 ∧
    noDecoyProxy nu s Q (noDecoyOptimizer s Q) =
      s^2*(nu*(noDecoyF Q)^2/(2*(1-QAlgorithms.binEntropy2 (2*Q)))) := 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: approximate no-decoy optimization, Eqs.(36)–(37)

Read-back

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

Let $\nu,s,Q$ be real numbers satisfying $\nu>0$ , $0<s\le1$ , and $0\le Q<1/4$ . Write $H(x)=[-x\log x-(1-x)\log(1-x)]/\log2$ for binary entropy, with the endpoint products $0\log0$ interpreted as zero, and suppose also that $A=1-H(2Q)>0$ and $F=1-H(2Q)-H(Q)\ge0$ . Define

m_*=\frac{sF}{A}, \qquad P(\mu)=\nu\left(\mu sF-\frac{\mu^2A}{2}\right).

Then $m_*\ge0$ , $P(m_*)=\nu s m_*F/2$ , and every real $\mu\ge0$ satisfies $P(\mu)\le P(m_*)$ , with equality if and only if $\mu=m_*$ . Moreover,

P(2m_*)=0, \qquad P(m_*)=s^2\frac{\nu F^2}{2A}.

There is no upper restriction on $\mu$ ; the hypotheses permit $F=0$ , in which case $m_*=0$ and the asserted maximum is 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