Theorem 4 (Inner Bound to the Capacity-Reliability-Secrecy Region)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.exponent_inner_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$ .

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 $0\le\rho\le1$ put

e_1(\rho)=\rho R_\Phi-\log_2\sum_{s,y}p(s)W_Y(y\mid s)\left[\sum_x W_{X\mid Y,S}(x\mid y,s)^{1/(1+\rho)}\right]^{1+\rho},

e_2(\rho)=\rho(R_\Phi-R_M)-\log_2\sum_{x,y}\left[\sum_s p(s)W_{XY}(x,y\mid s)^{1/(1+\rho)}\right]^{1+\rho},

e_3(\rho)=\rho(R_\Phi-R_M)-\log_2\sum_y\left[\sum_{s,x}p(s)W_{XY}(x,y\mid s)^{1/(1+\rho)}\right]^{1+\rho}.

Let $E_o=\min_{j=1,2,3}\max_{\rho\in[0,1]} e_j(\rho)$ . Here $W_{XY}$ and $W_Y$ are the indicated channel marginals. Unsupported conditional rows have zero outer weight. The first and second displays incorporate the documented source corrections C18 and C19.

For $0<\alpha\le1$ put

f(\alpha)=-\alpha(R_{\rm SK}+R_\Phi-R_M)-\log_2\sum_{s,x,z}p(s)W_{XZ}(x,z\mid s)\left[\frac{W_{XZ}(x,z\mid s)}{p_Z(z)}\right]^\alpha, \qquad F_o=\sup_{0<\alpha\le1}f(\alpha).

Here $p_Z$ is induced by $p$ and $W$ , and null $z$ fibers contribute zero.

For a common input law $p$ and auxiliary rates $R_\Phi,R_M\ge0$ let

\widetilde{\mathcal R}(p,R_\Phi,R_M)=\{(R,E,F)\in[0,\infty)^3:E\le E_o(p,R_\Phi,R_M),\ F\le F_o(p,R,R_\Phi,R_M)\}.

Then

\bigcup_{p,R_\Phi,R_M}\widetilde{\mathcal R}(p,R_\Phi,R_M)\subseteq\mathcal R.

This is an operational inner bound with a common code sequence for both exponents and the required key entropy rate. The printed proof's fixed-bin exact-uniformity assertion is not assumed.

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.6, Theorem 4, (25), using documented C18/C19. No cost constraint.
The operational region retains observationEntropyBits and simultaneous exponents; public
fixed-bin uniformity is not a hypothesis. -/
theorem exponent_inner_bound (W : DMBC S X Y Z) :
    (⋃ (p : S → ℝ) (_ : IsLaw p) (RP : ℝ) (_ : 0 ≤ RP)
      (RM : ℝ) (_ : 0 ≤ RM), innerRegion W p RP RM) ⊆ region W := 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. 6, Theorem 4 (Inner Bound to the Capacity-Reliability-Secrecy Region)

Read-back

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

For finite nonempty sets $S,X,Y,Z$ , let $W_s(x,y,z)\ge0$ satisfy $\sum_{x,y,z}W_s(x,y,z)=1$ for every $s$ . Define $A_s(x,y)=\sum_zW_s(x,y,z)$ , $B_s(y)=\sum_xA_s(x,y)$ , and $C_s(x,z)=\sum_yW_s(x,y,z)$ . For any probability law $p$ on $S$ , meaning $p(s)\ge0$ and $\sum_sp(s)=1$ , and any $R_P,R_M\ge0$ , put $p_Z(z)=\sum_{s,x}p(s)C_s(x,z)$ and

\begin{aligned} F_1(r)&=rR_P-\log_2\!\sum_{s,y}p(s)B_s(y) \left[\sum_x\left(\frac{A_s(x,y)}{B_s(y)}\right)^{1/(1+r)}\right]^{1+r},\\ F_2(r)&=r(R_P-R_M)-\log_2\!\sum_{x,y} \left[\sum_sp(s)A_s(x,y)^{1/(1+r)}\right]^{1+r},\\ F_3(r)&=r(R_P-R_M)-\log_2\!\sum_y \left[\sum_{s,x}p(s)A_s(x,y)^{1/(1+r)}\right]^{1+r},\\ G(\alpha,R)&=-\alpha(R+R_P-R_M)-\log_2\!\sum_z \begin{cases} 0,&p_Z(z)=0,\\ \displaystyle\sum_{s,x}p(s)C_s(x,z) \left(\frac{C_s(x,z)}{p_Z(z)}\right)^\alpha,&p_Z(z)\ne0. \end{cases} \end{aligned}

The theorem says that every real triple $(R,E,F)$ with $R,E,F\ge0$ ,

E\le\min\left\{\sup_{r\in[0,1]}F_1(r), \min\left\{\sup_{r\in[0,1]}F_2(r),\sup_{r\in[0,1]}F_3(r)\right\}\right\}, \qquad F\le\sup_{0<\alpha\le1}G(\alpha,R),

belongs to the ordinary topological closure in $\mathbb R^3$ of the following set of triples. A triple $(R',E',F')$ is in that set when all three coordinates are nonnegative and there is a family of codes, one for every positive blocklength $N$ , with positive integers $M_N,P_N,K_N$ , a probability distribution $a_N(\,\cdot\mid m)$ on $S^N$ for each message $m\in\{0,\ldots,M_N-1\}$ , and deterministic functions $T_N(m,x^N)\in\{0,\ldots,P_N-1\}$ , $K_{A,N}(m,x^N)\in\{0,\ldots,K_N-1\}$ , and $K_{B,N}(y^N,T)\in\{0,\ldots,K_N-1\}$ . Their joint law is

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

For some fixed nonnegative real constants $r_M,r_P,r_K$ , the sizes satisfy $M_N=2^{\lceil Nr_M\rceil}$ , $P_N=2^{\lceil Nr_P\rceil}$ , and $K_N\le2^{Nr_K}$ for every $N$ . Let $e_N=\Pr(K_{A,N}\ne K_{B,N})$ and $\ell_N=I(K_{A,N};(Z^N,T_N))$ , where for any finite observation $U$ , $H(U)=-\sum_o\Pr(o)\log_2\Pr(U=U(o))$ , and $I(U;V)=H(U)+H(V)-H(U,V)$ . The required asymptotic conditions are that $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}

The exponent suprema and inequalities use extended real numbers. Zero exponents are allowed, without a separate requirement in this definition that $e_N$ or $\ell_N$ tend to zero. The auxiliary choices $p,R_P,R_M$ in the inclusion are existential choices for membership in the union; the stated conclusion is membership in the closure, not necessarily membership in the set before closure. Divisions, powers, and logarithms use their total definitions, including division by zero and $\log_2 0$ equal 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