Proposition 2 (Upper Bound in Secret Key Capacity)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.secret_key_upper_bound

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

prove2quantum

Let $S,X,Y,Z$ be finite nonempty alphabets and let $W(x,y,z\mid s)$ be a normalized discrete memoryless broadcast channel. All entropies and information quantities are in bits. For an input law $p$ , information quantities below use exactly the induced law $p(s)W(x,y,z\mid s)$ .

Alice draws a uniform finite message $M$ , uses a possibly stochastic encoder to excite $n$ channel uses, and observes $(M,X^n)$ . A public forward message $\Phi=\phi(M,X^n)$ is visible to Bob and Eve. Their keys are $K_A=k_A(M,X^n)$ and $K_B=k_B(Y^n,\Phi)$ . All design maps are fixed publicly before observations. Message and public alphabets follow the fixed-rate ceiling convention; the key alphabet at rate $R$ has exactly $2^{\lceil nR\rceil}$ labels. A weakly achievable rate $R$ has one sequence of such codes with disagreement tending to zero, $I(K_A;Z^n,\Phi)/n\to0$ , and $\liminf H(K_A)/n\ge R$ .

Let $\Lambda:S\to[0,L]$ be bounded and nonnegative, and let $\Gamma>0$ be admissible, meaning that a normalized input law of expected cost at most $\Gamma$ exists. Every operational code obeys $n^{-1}\sum_i\Lambda(S_i)\le\Gamma$ almost surely; each single-letter optimization obeys $\sum_s p(s)\Lambda(s)\le\Gamma$ . Excitation and public rates are unrestricted.

The cost-feasible single-letter maximum is attained, and

C_{\rm SK}(\Gamma)\le\max_{p:\,\mathbb E\Lambda(S)\le\Gamma} I(X,S;Y\mid Z).

This upper bound requires no auxiliary variables.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P76

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P76

noncomputable section

open scoped BigOperators

open Filter Set

attribute [local instance] Classical.propDecidable

-- Exact pinned primitives, inspected at their definitions before reuse.

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Frontier30.P12 (IsStochastic)

variable {S X Y Z : Type} [Fintype S] [Fintype X] [Fintype Y] [Fintype Z]
  [Nonempty S] [Nonempty X] [Nonempty Y] [Nonempty Z]

variable {n u w : ℕ}

/-- PDF p.5, Proposition 2, (11): an attained cost-feasible upper bound. -/
theorem secret_key_upper_bound (W : DMBC S X Y Z) (cost : S → ℝ) (Gamma : ℝ)
    (hcost : AdmissibleCost cost Gamma) :
    ∃ p : S → ℝ, CostFeasibleInput cost Gamma p ∧
      IsGreatest {v | ∃ q, CostFeasibleInput cost Gamma q ∧ v = upperObjective W q}
        (upperObjective W p) ∧
      senderExcitedCapacity W cost (some Gamma) ≤ (upperObjective W p : EReal) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P76

Source

The Sender-Excited Secret Key Agreement Model: Capacity, Reliability and Secrecy Exponents, arXiv:1107.4148v4, PDF p. 5, Proposition 2 (Upper Bound in Secret Key Capacity)

Read-back

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

For finite types $S,X,Y,Z$ , let $W$ give their nonemptiness and conditional probability laws $W_s(x,y,z)$ . Suppose $c:S\to\mathbb R$ and $\Gamma\in\mathbb R$ satisfy $\Gamma>0$ , $0\le c(s)\le L$ for every $s$ for some real $L$ , and the existence of a probability law whose expected cost is at most $\Gamma$ . There exists a probability law $p$ on $S$ with $\sum_s p(s)c(s)\le\Gamma$ such that

B(p)=I_{\nu_p}((X,S);Y\mid Z),\qquad \nu_p(s,x,y,z)=p(s)W_s(x,y,z),

belongs to, and is at least every member of, the set of $B(q)$ over all probability laws $q$ satisfying $\sum_s q(s)c(s)\le\Gamma$ , and the sender-excited capacity is at most $B(p)$ , embedded in the extended real numbers. Here $I(A;B\mid C)=H(A,C)-H(C)-H(A,B,C)+H(B,C)$ , with Shannon entropy in bits. The capacity being bounded is the extended-real supremum of nonnegative real rates $R$ admitting a sequence of codes at all positive block lengths $\ell$ : each code has positive message, public-message, and key counts $M_\ell,P_\ell,K_\ell$ , normalized nonnegative encoders $e_\ell(s^\ell\mid m)$ , a public map $f_\ell(m,x^\ell)$ , an Alice key map $a_\ell(m,x^\ell)$ , and a Bob key map $b_\ell(y^\ell,t)$ ; for fixed nonnegative constants $r_M,r_P,r_K$ , their counts satisfy $M_\ell=2^{\lceil\ell r_M\rceil}$ , $P_\ell=2^{\lceil\ell r_P\rceil}$ , and $K_\ell\le2^{\ell r_K}$ ; every encoder-supported word has $\sum_i c(s_i)\le\ell\Gamma$ ; and under $M_\ell^{-1}e_\ell(s^\ell\mid m)\prod_iW_{s_i}(x_i,y_i,z_i)$ , key disagreement tends to zero, $I(a_\ell(m,x^\ell);(z^\ell,f_\ell(m,x^\ell)))/\ell$ tends to zero, and for every $\varepsilon>0$ , eventually $H(a_\ell(m,x^\ell))/\ell\ge R-\varepsilon$ .

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