Prove2Me

III.C.1: exact optimization of the displayed rate polynomial, (16)–(18)

Open
QAlgorithms.Papers.Independent.Intakethird100.P33.ratePolynomialOptimum

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let 0<t<10<t<1, 0<tB≤10<t_B\le1, 0<η≤10<\eta\le1, and 0≤f<10\le f<1. Regard the expression displayed in (16) solely as the polynomial

P(μ)=μttBη(1−f)[1−μ(1−t)],μ≥0.P(\mu)=\mu t t_B\eta(1-f)\bigl[1-\mu(1-t)\bigr],\qquad \mu\ge0.

Its unique maximizer and maximum are

μ∗=12(1−t),P(μ∗)=ttBη(1−f)4(1−t).\mu_*={1\over2(1-t)},\qquad P(\mu_*)={t t_B\eta(1-f)\over4(1-t)}.

For every μ≥0\mu\ge0, P(μ)≤P(μ∗)P(\mu)\le P(\mu_*), with equality exactly when μ=μ∗\mu=\mu_*. The strictly lossy domain avoids division by zero and the positive prefactors exclude the identically zero polynomial.

This is the page's exact algebraic optimization. It does not identify the polynomial with an operational secure-key rate or certify an approximation regime.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P33
Formal statement
noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P33

open scoped BigOperators ENNReal

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity rankOne)

open QAlgorithms.Papers.Independent.Dependency50.P39 (coherentCoefficient)

open QAlgorithms.Papers.Independent.Support50.P48 (vacuumAmplitude)

open QAlgorithms.Papers.Independent.Next46.P32 (FockPOVM realFockTracePair)

open QAlgorithms.Papers.Independent.Dependency50.P34
  (TwoModeFock fockKet photonMean)

open QAlgorithms.Papers.Independent.Frontier18.P14
  (coherentPair coherentPairCoefficients)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- PDF p.5, (16)-(18): exact optimization of the printed polynomial over mu≥0.
Strictly lossy t and positive prefactors are the nontrivial protocol branch.
This is not a secure-key achievability or security theorem. -/
theorem ratePolynomialOptimum (t tB eta f : ℝ)
    (ht : 0 < t) (ht1 : t < 1) (htB : 0 < tB) (htB1 : tB ≤ 1)
    (heta : 0 < eta) (heta1 : eta ≤ 1) (hf : 0 ≤ f) (hf1 : f < 1) :
    let muOpt := 1 / (2 * (1 - t))
    0 < muOpt ∧
    ratePolynomial t tB eta f muOpt = t * tB * eta * (1 - f) / (4 * (1 - t)) ∧
    (∀ mu : ℝ, 0 ≤ mu →
      ratePolynomial t tB eta f mu ≤ ratePolynomial t tB eta f muOpt) ∧
    (∀ mu : ℝ, 0 ≤ mu →
      (ratePolynomial t tB eta f mu = ratePolynomial t tB eta f muOpt ↔ mu = muOpt)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P33

end
Source
Towards practical and fast Quantum Cryptography, arXiv:quant-ph/0411022v1, PDF p. 5, III.C.1, (16)–(18)
Read-back

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

For all real numbers t,tB,η,ft,t_B,\eta,f satisfying 0<t<10<t<1, 0<tB≤10<t_B\le1, 0<η≤10<\eta\le1, and 0≤f<10\le f<1, define R(μ)=μttBη(1−f)(1−μ(1−t))R(\mu)=\mu t t_B\eta(1-f)(1-\mu(1-t)) for every real μ\mu, and set μ∗=12(1−t)\mu_*=\frac{1}{2(1-t)}. Then μ∗>0\mu_*>0, its value is

R(μ∗)=ttBη(1−f)4(1−t),R(\mu_*)=\frac{t t_B\eta(1-f)}{4(1-t)},

and, for every real μ≥0\mu\ge0, R(μ)≤R(μ∗)R(\mu)\le R(\mu_*), with R(μ)=R(μ∗)R(\mu)=R(\mu_*) if and only if μ=μ∗\mu=\mu_*. The maximization ranges over all nonnegative real μ\mu, with no upper bound on μ\mu.

Human review

  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph