§IV-D, unnumbered strong achievability below degraded capacity (33)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.strong_degraded

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$ .

There is no excitation cost constraint. Rates and target exponents are nonnegative. Let $\mathcal R$ be the closure of triples $(R,E,F)$ attained by a single code sequence satisfying the entropy-rate lower bound and $\liminf[-\log_2\Pr(K_A\ne K_B)]/n\ge E$ , $\liminf[-\log_2 I(K_A;Z^n,\Phi)]/n\ge F$ . A zero error or leakage has decay rate $+\infty$ . Strong achievability requires both $E>0$ and $F>0$ .

For a channel stochastically degraded in Bob's favor, every normalized input law $p$ and rate

0\le R<I(X,S;Y)-I(X,S;Z)

yield a strongly achievable key rate. Zero rate is strongly achievable by the one-value-key protocol, and

\sup\{R:R\text{ strongly achievable}\}=C_{\rm SK}(\text{no cost constraint}).

This states strict-interior achievability and equality of suprema; it does not assert positive exponents at the maximizing endpoint.

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 pp.7--8, (33): strict interior rates are strong, and suprema agree.
No positive-exponent senderExcitedCapacity-endpoint claim. Zero rate uses one key value. -/
theorem strong_degraded (W : DMBC S X Y Z) (hdeg : SenderExcitedDegraded W) :
    (∀ p : S → ℝ, IsLaw p → ∀ R : ℝ, 0 ≤ R → R < advantage W p →
      StrongAchievable W R) ∧ StrongAchievable W 0 ∧
    strongCapacity W = senderExcitedCapacity W (fun _ => 0) none := 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. 7, §IV-D, unnumbered strong achievability below degraded capacity (33)

Read-back

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

Let $S,X,Y,Z$ be finite nonempty sets, and let $W_s(x,y,z)$ be a probability distribution for every $s$ . Assume there is a stochastic kernel $d(z\mid y)$ , with $d(z\mid y)\ge0$ and $\sum_zd(z\mid y)=1$ , such that

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

For any probability law $p$ on $S$ , let $q(s,x,y,z)=p(s)W_s(x,y,z)$ , and put $A(p)=I_q((X,S);Y)-I_q((X,S);Z)$ , where $H_q(U)=-\sum_o q(o)\log_2\sum_{o':U(o')=U(o)}q(o')$ and $I_q(U;V)=H_q(U)+H_q(V)-H_q(U,V)$ . The theorem says that every $R\ge0$ with $R<A(p)$ is strongly achievable, that zero is strongly achievable independently of this strict inequality, and that the supremum of strongly achievable rates equals the supremum of weakly achievable rates with zero cost function and no cost constraint, both suprema being taken in the extended real line after embedding the real rates. Here the rate notions have the following literal meanings. For each positive blocklength $N$ , a code has positive integers $M_N,P_N,K_N$ , a stochastic encoder $a_N(s^N\mid m)$ , and deterministic functions giving a public value $T_N(m,x^N)$ , Alice’s key $K_{A,N}(m,x^N)$ , and Bob’s key $K_{B,N}(y^N,T_N)$ , with respective ranges of sizes $P_N,K_N,K_N$ ; its probability law is

M_N^{-1}a_N(s^N\mid m)\prod_{i=1}^{N}W_{s_i}(x_i,y_i,z_i).

A permitted family has fixed nonnegative constants $r_M,r_P,r_K$ such that $M_N=2^{\lceil Nr_M\rceil}$ , $P_N=2^{\lceil Nr_P\rceil}$ , and $K_N\le2^{Nr_K}$ for every $N$ . Write $e_N=\Pr(K_{A,N}\ne K_{B,N})$ and $\ell_N=I(K_{A,N};(Z^N,T_N))$ . Strong achievability of $R$ means $R\ge0$ and the existence of such a family and positive real numbers $E,F$ for which $R-\varepsilon\le H(K_{A,N})/N$ eventually for every $\varepsilon>0$ , and

E\le\liminf_{N\to\infty}L_N(e_N),\qquad F\le\liminf_{N\to\infty}L_N(\ell_N),\qquad L_N(t)= \begin{cases} +\infty,&t=0,\\ -\log_2(t)/N,&t\ne0. \end{cases}

Weak achievability with the specified absent cost constraint means $R\ge0$ and the existence of a permitted family satisfying the same eventual entropy lower bounds, together with $e_N\to0$ and $\ell_N/N\to0$ . These definitions impose an entropy rate requirement on Alice’s key; they do not impose a separate uniformity requirement on its distribution.

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