§IV-E-II, source-model rate conditions (36)–(37)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.source_specialization

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

Set $S$ to a singleton and $R_M=0$ . For any nonnegative key and public rates the pair of reliability conditions (27)--(28) is equivalent to

R_\Phi>H(X\mid Y),

and the secrecy condition (29) is equivalent to

R_{\rm SK}+R_\Phi<H(X\mid Z).

These are exactly the paper's rate-condition specializations, rather than a claim about empty alphabets or a new attribution of the background coding theorems. Under both strict conditions, the specialized reliability and secrecy exponents are strictly positive, and the secret-key rate is strongly achievable.

The witnessing code sequence has excitation rate exactly zero and public rate exactly the specified $R_\Phi$ , with the same ceiling convention at every positive blocklength.

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.8, (36)--(37): S is a singleton, not an empty alphabet.
Both specialized rate conditions, positive exponents and strong achievability
at the specified public rate and zero excitation rate
are retained without attributing the cited
background Slepian--Wolf or privacy-amplification theorems to this paper. -/
theorem source_specialization (W : DMBC Unit X Y Z) (RK RP : ℝ)
    (hK : 0 ≤ RK) (hP : 0 ≤ RP) :
    let p : Unit → ℝ := fun _ => 1
    ((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 - 0) ↔
      condEntropy (excitationJointMass W p) obsX obsY < RP) ∧
    ((RK + RP - 0 < condEntropy (excitationJointMass W p) obsX (fun o => (obsZ o, obsS o)) -
      observationMutualInfoBits (excitationJointMass W p) obsS obsZ) ↔ RK + RP < condEntropy (excitationJointMass W p) obsX obsZ) ∧
    ((condEntropy (excitationJointMass W p) obsX obsY < RP ∧
      RK + RP < condEntropy (excitationJointMass W p) obsX obsZ) →
      0 < reliabilityExponent W p RP 0 ∧ 0 < secrecyExponent W p RK RP 0 ∧
      StrongAchievableAt W RK RP 0) := 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. 8, §IV-E-II, source-model rate conditions (36)–(37)

Read-back

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

Let $X,Y,Z$ be finite nonempty alphabets, let $W$ assign a probability distribution on $X\times Y\times Z$ to the unique element of the singleton alphabet $S=\{*\}$ , and let $R_K,R_P\ge0$ . Set $p(*)=1$ and $q(s,x,y,z)=p(s)W_s(x,y,z)$ , and denote its coordinate observations by $S,X,Y,Z$ . Using Shannon entropy $H(U)=-\sum_u q(U=u)\log_2q(U=u)$ , conditional entropy $H(U\mid V)=H(U,V)-H(V)$ , and mutual information $I(U;V)=H(U)+H(V)-H(U,V)$ , with zero-probability summands equal to zero, the declaration asserts the conjunction

\begin{gathered} \bigl(H(X\mid Y,S)<R_P\ \land\ H(X\mid Y,S)-I(S;Y)<R_P-0\bigr) \iff H(X\mid Y)<R_P,\\ \bigl(R_K+R_P-0<H(X\mid Z,S)-I(S;Z)\bigr) \iff R_K+R_P<H(X\mid Z),\\ \bigl(H(X\mid Y)<R_P\ \land\ R_K+R_P<H(X\mid Z)\bigr) \Longrightarrow \bigl(0<\mathcal R(R_P,0)\ \land\ 0<\mathcal S(R_K,R_P,0)\ \land\ \mathcal A(R_K,R_P,0)\bigr). \end{gathered}

Here the constant observation $S$ remains part of the displayed left-hand expressions. To specify the quantities in the conclusion, put $u_s(x,y)=\sum_zW_s(x,y,z)$ , $v_s(y)=\sum_xu_s(x,y)$ , $w_s(x,z)=\sum_yW_s(x,y,z)$ , and $q_Z(z)=\sum_{s,x}p(s)w_s(x,z)$ . The extended-real reliability quantity is

\begin{aligned} A_\rho(P)&=\rho P-\log_2\!\left[ \sum_{s,y}p(s)v_s(y) \left(\sum_x\left(\frac{u_s(x,y)}{v_s(y)}\right)^{1/(1+\rho)}\right)^{1+\rho}\right],\\ B_\rho(P,M)&=\rho(P-M)-\log_2\!\left[ \sum_{x,y}\left(\sum_s p(s)u_s(x,y)^{1/(1+\rho)}\right)^{1+\rho}\right],\\ C_\rho(P,M)&=\rho(P-M)-\log_2\!\left[ \sum_y\left(\sum_{s,x}p(s)u_s(x,y)^{1/(1+\rho)}\right)^{1+\rho}\right],\\ \mathcal R(P,M)&=\min\!\left\{ \sup_{0\le\rho\le1}A_\rho(P),\ \min\!\left(\sup_{0\le\rho\le1}B_\rho(P,M), \sup_{0\le\rho\le1}C_\rho(P,M)\right)\right\}. \end{aligned}

The extended-real secrecy quantity is

\mathcal S(K,P,M)= \sup_{0<\alpha\le1} \left[ -\alpha(K+P-M)- \log_2\!\left( \sum_z \begin{cases} 0,&q_Z(z)=0,\\ \displaystyle\sum_{s,x}p(s)w_s(x,z) \left(\frac{w_s(x,z)}{q_Z(z)}\right)^\alpha,&q_Z(z)\ne0 \end{cases}\right) \right].

The suprema here are taken after viewing each real expression as an extended real; divisions by zero and logarithms at zero use the formal real conventions $a/0=0$ and $\log_2 0=0$ . Finally, $\mathcal A(K,P,M)$ means that $K,P,M\ge0$ and there exist real $E,F>0$ and codes of every length $N=n+1$ with exactly $2^{\lceil NM\rceil_+}$ messages, $2^{\lceil NP\rceil_+}$ public symbols, and $2^{\lceil NK\rceil_+}$ key symbols. Each code has a stochastic encoder $e_m(s^N)$ , deterministic public and Alice-key maps $T(m,x^N)$ and $A(m,x^N)$ , and a deterministic Bob-key map $B(y^N,T)$ . Under the law $M_n^{-1}e_m(s^N)\prod_iW_{s_i}(x_i,y_i,z_i)$ , for every $\varepsilon>0$ eventually $K-\varepsilon\le H(A)/(n+1)$ , and the lower limits of $-\log_2\Pr\{A\ne B\}/(n+1)$ and $-\log_2 I(A;(Z^N,T))/(n+1)$ are at least $E$ and $F$ , respectively, assigning $+\infty$ whenever the probability or leakage is zero. In this declaration $M=0$ , so every such code has exactly one message; no input-cost constraint is included.

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