VII.C: continuous linear-network toy cost and optimal link length, Eqs.(79)–(80)

Proved

QAlgorithms.Papers.Independent.Gap48.P25.networkOptimum

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

prove2quantum

In the continuous linear-network toy model, let $C_1,L,K_{\rm target},a,k,\alpha>0$ . Arbitrarily parallel devices and trusted stations with neglected station costs give the continuous device count $N=(L/\ell)K_{\rm target}/K(\ell)$ , with $K(\ell)=a10^{-k\alpha\ell/10}$ . For $\ell>0$ ,

C_{\rm tot}(\ell)={C_1LK_{\rm target}\over\ell K(\ell)},\qquad \ell_*={10\over k\alpha\ln10}.

The function $\ell K(\ell)$ has its unique maximum over positive lengths at $\ell_*$ , which minimizes cost. If a finite chain requires $\ell\le L$ , the constrained maximizer is $\min\{L,\ell_*\}$ . No integer rounding, station cost, or discrete network-design optimality 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)

/-- Eqs.(79)–(80), PDF p.40: continuous device-count relaxation, including the
unique unconstrained optimum and the finite-chain constrained optimizer. -/
theorem networkOptimum (C L target a k alpha : ℝ) (hC : 0 < C) (hL : 0 < L)
    (htarget : 0 < target) (ha : 0 < a) (hk : 0 < k) (halpha : 0 < alpha) :
    let K := fun ell : ℝ => a*Real.rpow 10 (-k*alpha*ell/10)
    let opt := 10/(k*alpha*Real.log 10)
    0 < opt ∧
    (∀ ell : ℝ, 0 < ell → networkCost C L target ell (K ell) = C*L*target/(ell*K ell)) ∧
    (∀ ell : ℝ, 0 < ell → ell*K ell ≤ opt*K opt ∧
      (ell*K ell = opt*K opt ↔ ell = opt) ∧
      networkCost C L target opt (K opt) ≤ networkCost C L target ell (K ell)) ∧
    (∀ ell : ℝ, 0 < ell → ell ≤ L → ell*K ell ≤ min L opt*K (min L opt)) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P25

end

Source

The Security of Practical Quantum Key Distribution, arXiv:0802.4155v3, PDF p. 40, VII.C: continuous linear-network toy cost and optimal link length, Eqs.(79)–(80)

Read-back

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

For every collection of positive real numbers $C,L,T,a,k,\alpha$ , where $T$ is the parameter named target, define

K(\ell)=a\,10^{-k\alpha\ell/10},\qquad o=\frac{10}{k\alpha\log10},\qquad \mathcal C(\ell,r)=C\left(\frac L\ell\right)\left(\frac Tr\right).

Then $o>0$ , and for every real $\ell>0$ , $\mathcal C(\ell,K(\ell))=CLT/(\ell K(\ell))$ . For every such $\ell$ ,

\ell K(\ell)\le oK(o),\qquad \ell K(\ell)=oK(o)\iff\ell=o,\qquad \mathcal C(o,K(o))\le\mathcal C(\ell,K(\ell)).

Furthermore, whenever $0<\ell\le L$ ,

\ell K(\ell)\le \min\{L,o\}\,K(\min\{L,o\}).

The unrestricted optimum $o$ is not assumed to be at most $L$ .

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