§IV-E-III, unnumbered reduction in required public discussion

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.public_discussion_reduction

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, the public-rate thresholds of source emulation and the hybrid reliability construction satisfy

H(X,S\mid Y)-H(X\mid Y,S)=H(S\mid Y)\ge0.

For every $R_\Phi>H(X\mid Y,S)$ there is a nonnegative $R_M$ with $R_\Phi-R_M>H(X\mid Y,S)-I(S;Y)$ , so both hybrid reliability conditions hold. The threshold reduction is strict only if $H(S\mid Y)>0$ .

This compares sufficient thresholds of two constructions and asserts no universal public-discussion converse. More precisely, for every $R_K\ge0$ below $I(X,S;Y)-I(X,S;Z)$ and every $R_\Phi>H(X\mid Y,S)$ , there is $R_M\ge0$ such that

R_K+R_\Phi-H(X\mid Z,S)+I(S;Z)<R_M<R_\Phi-H(X\mid Y,S)+I(S;Y).

Both exponents at these rates are positive, and $R_K$ is strongly achievable.

The witnessing code sequence uses exactly the specified public rate $R_\Phi$ and the very same nonnegative message rate $R_M$ chosen in the displayed interval, so its public-discussion budget is retained in the operational conclusion.

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.9: construction-specific thresholds differ by H(S|Y). The smaller
threshold admits a nonnegative excitation-rate choice meeting reliability AND
secrecy for each nonnegative key rate strictly below the information advantage.
The witnessing codes use this very public rate and chosen excitation rate;
this is not a converse against all protocols below that threshold. -/
theorem public_discussion_reduction (W : DMBC S X Y Z) (p : S → ℝ) (hp : IsLaw p) :
    let q := excitationJointMass W p
    condEntropy q (fun o => (obsX o, obsS o)) obsY -
      condEntropy q obsX (fun o => (obsY o, obsS o)) = condEntropy q obsS obsY ∧
    condEntropy q obsX (fun o => (obsY o, obsS o)) ≤
      condEntropy q (fun o => (obsX o, obsS o)) obsY ∧
    (∀ RK RP : ℝ, 0 ≤ RK → RK < advantage W p →
      condEntropy q obsX (fun o => (obsY o, obsS o)) < RP →
      ∃ RM : ℝ, 0 ≤ RM ∧
        RK + RP - condEntropy q obsX (fun o => (obsZ o, obsS o)) +
          observationMutualInfoBits q obsS obsZ < RM ∧
        RM < RP - condEntropy q obsX (fun o => (obsY o, obsS o)) +
          observationMutualInfoBits q obsS obsY ∧
        0 < reliabilityExponent W p RP RM ∧
        0 < secrecyExponent W p RK RP RM ∧ StrongAchievableAt W 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. 9, §IV-E-III, unnumbered reduction in required public discussion

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 $W_s(x,y,z)$ be a probability distribution on $X\times Y\times Z$ for every $s$ , and let $p(s)\ge0$ with $\sum_sp(s)=1$ , allowing zero probabilities. Put $q(s,x,y,z)=p(s)W_s(x,y,z)$ , and denote the coordinate observations by $S,X,Y,Z$ . Define $H(U)=-\sum_uq(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)$ , with zero-probability summands equal to zero, and set $\mathcal D=I((X,S);Y)-I((X,S);Z)$ . The declaration asserts

H((X,S)\mid Y)-H(X\mid Y,S)=H(S\mid Y), \qquad H(X\mid Y,S)\le H((X,S)\mid Y),

and, for every pair of real numbers $R_K,R_P$ , if $0\le R_K<\mathcal D$ and $H(X\mid Y,S)<R_P$ , then there exists a real number $R_M\ge0$ such that

\begin{gathered} R_K+R_P-H(X\mid Z,S)+I(S;Z)<R_M,\\ R_M<R_P-H(X\mid Y,S)+I(S;Y),\\ 0<\mathcal R(R_P,R_M),\qquad 0<\mathcal S(R_K,R_P,R_M),\qquad \mathcal A(R_K,R_P,R_M). \end{gathered}

Here the strict lower and upper bounds on $R_M$ are both required. To define the last three quantities explicitly, 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)$ . In the extended reals,

\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}

The real expressions are embedded into the extended reals before taking suprema, and use total real division and logarithms, in particular $a/0=0$ and $\log_2 0=0$ . The property $\mathcal A(K,P,M)$ means that $K,P,M\ge0$ and there exist real $E,F>0$ and codes for every length $N=n+1$ , including length one, 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 $P_n(m,s^N,x^N,y^N,z^N)=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)$ , and the lower limits of the logarithmic rates of the disagreement probability $\Pr\{A\ne B\}$ and leakage $I(A;(Z^N,T))$ are at least $E$ and $F$ , respectively, where the logarithmic rate of $t\ne0$ is $-\log_2t/(n+1)$ and that of $t=0$ is $+\infty$ . No input-cost restriction is part of this conclusion.

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