Proposition 5 (Positivity of Error Exponents)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.exponent_positivity

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 fixed normalized input law and nonnegative rates,

R_\Phi>H(X\mid Y,S),\quad R_\Phi-R_M>H(X\mid Y,S)-I(S;Y)\quad\Longrightarrow\quad E_o>0.

Independently,

R_{\rm SK}+R_\Phi-R_M<H(X\mid Z,S)-I(S;Z)\quad\Longrightarrow\quad F_o>0.

The two implications characterize sufficient strict rate conditions, retaining the secrecy clause continued on the next page.

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.6--7, Proposition 5, (27)--(29), with corrected C19.
Both implications are retained, including secrecy on the following page. -/
theorem exponent_positivity (W : DMBC S X Y Z) (p : S → ℝ) (hp : IsLaw p)
    (RK RP RM : ℝ) (hK : 0 ≤ RK) (hP : 0 ≤ RP) (hM : 0 ≤ RM) :
    ((condEntropy (excitationJointMass W p) obsX (fun o => (obsY o, obsS o)) < RP ∧
      condEntropy (excitationJointMass W p) obsX (fun o => (obsY o, obsS o)) -
        observationMutualInfoBits (excitationJointMass W p) obsS obsY < RP - RM) →
      0 < reliabilityExponent W p RP RM) ∧
    ((RK + RP - RM < condEntropy (excitationJointMass W p) obsX (fun o => (obsZ o, obsS o)) -
      observationMutualInfoBits (excitationJointMass W p) obsS obsZ) → 0 < secrecyExponent W p RK RP RM) := 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, Proposition 5 (Positivity of Error Exponents)

Read-back

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

Let $S,X,Y,Z$ be finite nonempty sets, let each $W_s$ be a probability distribution on $X\times Y\times Z$ , let $p(s)\ge0$ with $\sum_sp(s)=1$ , and let $R_K,R_P,R_M\ge0$ . Use the joint law $q(s,x,y,z)=p(s)W_s(x,y,z)$ , with $S,X,Y,Z$ denoting its coordinate observations. For any observation $U$ , define $H_q(U)=-\sum_o q(o)\log_2\sum_{o':U(o')=U(o)}q(o')$ , $H_q(U\mid V)=H_q(U,V)-H_q(V)$ , and $I_q(U;V)=H_q(U)+H_q(V)-H_q(U,V)$ . Put $A_s(x,y)=\sum_zW_s(x,y,z)$ , $B_s(y)=\sum_xA_s(x,y)$ , $C_s(x,z)=\sum_yW_s(x,y,z)$ , $p_Z(z)=\sum_{s,x}p(s)C_s(x,z)$ , and define

\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)&=-\alpha(R_K+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 asserts the conjunction of two implications:

\begin{gathered} H_q(X\mid Y,S)<R_P \quad\text{and}\quad H_q(X\mid Y,S)-I_q(S;Y)<R_P-R_M\\ \Longrightarrow\ 0<\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\}, \\[3pt] R_K+R_P-R_M<H_q(X\mid Z,S)-I_q(S;Z) \quad\Longrightarrow\quad 0<\sup_{0<\alpha\le1}G(\alpha). \end{gathered}

The two conclusions are separately conditional; neither converse is asserted. The suprema and their positivity comparisons are in the extended real line. Zero probabilities and zero rates are permitted, and division by zero and $\log_2 0$ are evaluated as 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