§IV-E-III, source-emulation rate conditions (38)–(40)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.source_emulation

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

For a fixed input law and nonnegative key and public rates, substituting $R_M=H(S)$ into (28) and (29) gives the equivalent conditions

R_\Phi>H(X,S\mid Y),\qquad R_{\rm SK}+R_\Phi<H(X,S\mid Z).

There exists a nonnegative public rate satisfying both if and only if

R_{\rm SK}<H(X,S\mid Z)-H(X,S\mid Y)=I(X,S;Y)-I(X,S;Z).

This describes source emulation at the rate-inequality level without identifying different exponent formulas. Under (38) and (39), the reliability exponent at $R_M=H(S)$ and the secrecy exponent are both strictly positive and the rate is strongly achievable. Every nonnegative rate below the displayed information difference is strongly achievable after choosing a public rate.

Under (38) and (39), the witnessing code sequence has excitation rate exactly $H(S)$ and public rate exactly the specified $R_\Phi$ . The final rate-only consequence still quantifies over a choice of public rate.

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, (38)--(40): substitute R_M=H(S), retain both rate conditions
their exact public-rate elimination, positive exponents and strong achievability
at the specified public rate and excitation rate H(S);
no equality of exponent functions. -/
theorem source_emulation (W : DMBC S X Y Z) (p : S → ℝ) (hp : IsLaw p)
    (RK RP : ℝ) (hK : 0 ≤ RK) (hP : 0 ≤ RP) :
    let q := excitationJointMass W p
    ((condEntropy q obsX (fun o => (obsY o, obsS o)) - observationMutualInfoBits q obsS obsY <
      RP - observationEntropyBits q obsS) ↔ condEntropy q (fun o => (obsX o, obsS o)) obsY < RP) ∧
    ((RK + RP - observationEntropyBits q obsS <
      condEntropy q obsX (fun o => (obsZ o, obsS o)) - observationMutualInfoBits q obsS obsZ) ↔
      RK + RP < condEntropy q (fun o => (obsX o, obsS o)) obsZ) ∧
    ((∃ r : ℝ, 0 ≤ r ∧ condEntropy q (fun o => (obsX o, obsS o)) obsY < r ∧
      RK + r < condEntropy q (fun o => (obsX o, obsS o)) obsZ) ↔
      RK < advantage W p) ∧
    ((condEntropy q (fun o => (obsX o, obsS o)) obsY < RP ∧
      RK + RP < condEntropy q (fun o => (obsX o, obsS o)) obsZ) →
      0 < reliabilityExponent W p RP (observationEntropyBits q obsS) ∧
      0 < secrecyExponent W p RK RP (observationEntropyBits q obsS) ∧
      StrongAchievableAt W RK RP (observationEntropyBits q obsS)) ∧
    (RK < advantage W p → StrongAchievable W RK) := 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-III, source-emulation rate conditions (38)–(40)

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 each $W_s(x,y,z)$ be a probability distribution on $X\times Y\times Z$ , let $p:S\to\mathbb R$ satisfy $p(s)\ge0$ and $\sum_sp(s)=1$ , and let $R_K,R_P\ge0$ . Zero values of $p$ are allowed. Set $q(s,x,y,z)=p(s)W_s(x,y,z)$ , and write $S,X,Y,Z$ for the coordinate observations under this law. With $H(U)=-\sum_u q(U=u)\log_2q(U=u)$ , $H(U\mid V)=H(U,V)-H(V)$ , and $I(U;V)=H(U)+H(V)-H(U,V)$ , using zero for zero-probability summands, define

\mathcal D=I((X,S);Y)-I((X,S);Z).

The declaration asserts all five statements

\begin{gathered} H(X\mid Y,S)-I(S;Y)<R_P-H(S) \iff H((X,S)\mid Y)<R_P,\\ R_K+R_P-H(S)<H(X\mid Z,S)-I(S;Z) \iff R_K+R_P<H((X,S)\mid Z),\\ \bigl(\exists r\in\mathbb R:\ 0\le r,\ H((X,S)\mid Y)<r,\ R_K+r<H((X,S)\mid Z)\bigr) \iff R_K<\mathcal D,\\ \bigl(H((X,S)\mid Y)<R_P\ \land\ R_K+R_P<H((X,S)\mid Z)\bigr) \Longrightarrow \bigl(0<\mathcal R(R_P,H(S))\ \land\ 0<\mathcal S(R_K,R_P,H(S))\ \land\ \mathcal A(R_K,R_P,H(S))\bigr),\\ R_K<\mathcal D\Longrightarrow\mathcal A_{\mathrm{free}}(R_K). \end{gathered}

For completeness, set $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 reliability and secrecy quantities appearing here are the following extended-real expressions:

\begin{aligned} \mathcal R(P,M) =\min\Bigg\{& \sup_{0\le\rho\le1}\left[ \rho P-\log_2\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],\\[-2pt] &\min\Bigg( \sup_{0\le\rho\le1}\left[ \rho(P-M)-\log_2\sum_{x,y} \left(\sum_sp(s)u_s(x,y)^{1/(1+\rho)}\right)^{1+\rho} \right],\\[-2pt] &\hspace{35pt} \sup_{0\le\rho\le1}\left[ \rho(P-M)-\log_2\sum_y \left(\sum_{s,x}p(s)u_s(x,y)^{1/(1+\rho)}\right)^{1+\rho} \right]\Bigg)\Bigg\},\\ \mathcal S(K,P,M) =\sup_{0<\alpha\le1}\Bigg[ &-\alpha(K+P-M) -\log_2\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} \Bigg]. \end{aligned}

Each real expression is embedded into the extended reals before taking its supremum; real divisions by zero equal zero and $\log_2 0=0$ . The property $\mathcal A(K,P,M)$ means $K,P,M\ge0$ and the existence of real $E,F>0$ and a code for 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. Such a code consists of a probability distribution $e_m$ on $S^N$ for each message, deterministic maps $T(m,x^N)$ and $A(m,x^N)$ to the public and key alphabets, and a deterministic map $B(y^N,T)$ to the key alphabet. Under the law $M_n^{-1}e_m(s^N)\prod_iW_{s_i}(x_i,y_i,z_i)$ , every $\varepsilon>0$ eventually satisfies $K-\varepsilon\le H(A)/(n+1)$ , while

E\le\liminf_{n\to\infty}\ell_n\!\left(\Pr\{A\ne B\}\right), \qquad F\le\liminf_{n\to\infty}\ell_n\!\left(I(A;(Z^N,T))\right), \quad \ell_n(t)= \begin{cases} +\infty,&t=0,\\ -\log_2t/(n+1),&t\ne0. \end{cases}

The property $\mathcal A_{\mathrm{free}}(K)$ requires the same code, entropy, and positive-exponent conditions, but existentially chooses nonnegative message and public rates $M,P$ rather than prescribing them. The codes include length one, and none of these achievability properties imposes an input-cost constraint.

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