Corollary 3 (Secret Key Capacity of Degraded DMBCs)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.degraded_capacity

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.

Assume the channel is degraded in Bob's favor. Physical degradation is $(X,S)-Y-Z$ . Stochastic degradation permits a coupling $W'(x,y,z\mid s)=W_{XY}(x,y\mid s)d(z\mid y)$ preserving both $W_{XY}$ and $W_{XZ}$ for a normalized kernel $d$ . Then

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

The maximum is attained.

This specializes the operational capacity to a single input-law optimization.

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, Corollary 3, (12): stochastic degradation preserves Alice's X. -/
theorem degraded_capacity (W : DMBC S X Y Z) (cost : S → ℝ) (Gamma : ℝ)
    (hcost : AdmissibleCost cost Gamma) (hdeg : SenderExcitedDegraded W) :
    ∃ p : S → ℝ, CostFeasibleInput cost Gamma p ∧
      IsGreatest {v | ∃ q, CostFeasibleInput cost Gamma q ∧ v = advantage W q}
        (advantage W p) ∧ senderExcitedCapacity W cost (some Gamma) = (advantage 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, Corollary 3 (Secret Key Capacity of Degraded DMBCs)

Read-back

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

Let $S,X,Y,Z$ be finite nonempty alphabets, let $W_s(x,y,z)\ge0$ sum to $1$ for each $s$ , and let $c:S\to\mathbb R$ , $\Gamma\in\mathbb R$ satisfy $\Gamma>0$ , $0\le c(s)\le L$ for some real $L$ and every $s$ , and the existence of a probability law on $S$ of expected cost at most $\Gamma$ . Suppose also that there exists a stochastic kernel $d(y,z)\ge0$ , with $\sum_zd(y,z)=1$ for every $y$ , such that

\sum_y W_s(x,y,z) =\sum_y\left(\sum_t W_s(x,y,t)\right)d(y,z) \quad\text{for every }s,x,z.

Then there exists a probability law $p$ on $S$ with $\sum_sp(s)c(s)\le\Gamma$ whose value $A(p)=I_p((X,S);Y)-I_p((X,S);Z)$ , computed in bits under $p(s)W_s(x,y,z)$ , is greatest among all such cost-feasible laws, and the extended-real sender-excited capacity equals $A(p)$ . This capacity is the supremum of nonnegative real rates $R$ admitting codes at every positive length $N$ , each with a uniform message $m<M_N$ , a conditional excitation distribution $e_{N,m}$ , a public function $F_N(m,x^N)$ , Alice’s key $K_A(m,x^N)$ , and Bob’s key $K_B(y^N,F_N(m,x^N))$ . Fixed nonnegative constants $r_M,r_P,r_K$ must give message and public-range sizes $2^{\lceil Nr_M\rceil_+},2^{\lceil Nr_P\rceil_+}$ and key-range size at most $2^{Nr_K}$ ; every excitation word with positive encoder probability must have total cost at most $N\Gamma$ . Under weights $M_N^{-1}e_{N,m}(s^N)\prod_iW_{s_i}(x_i,y_i,z_i)$ , eventual $H(K_A)/N\ge R-\varepsilon$ must hold for every $\varepsilon>0$ , key disagreement must tend to zero, and $I(K_A;(Z^N,F_N))/N$ must tend to zero.

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