Unnumbered main result: source resource inequality (36)

Open

QAlgorithms.Papers.Independent.Intakethird100.P42.sourceResourceInequality

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\{p(x),\rho_x^S\}$ be a normalized finite classical–quantum source and $W(y\mid x)$ a finite stochastic channel. The Source distributes $X_S$ to Alice and $S$ to Bob by identity channels. Let $\sigma^{X_A Y_A Y_B B}=\sum_{x,y}p(x)W(y\mid x)|x,y,y\rangle\langle x,y,y|\otimes\rho_x^B$ , with Alice retaining $X_A,Y_A$ and Bob retaining $Y_B,B$ .

In the source-relative IID simulation relation, the direct coding corner is

\big\langle\mathrm{id}^{X_S\to X_A}\otimes\mathrm{id}^{S\to B}:\rho^{X_SS}\big\rangle+(I(X_A;Y_B)_\sigma-I(Y_B;B)_\sigma)[c\to c]+H(Y_B\mid X_A)_\sigma[cc]\ \ge_s\ \big\langle W^{X_S\to Y_A Y_B}\otimes\mathrm{id}^{S\to B}:\rho^{X_SS}\big\rangle.

All entropies are in bits. Operationally, for every positive error and rate slack and all sufficiently large positive blocklengths, this means a code with forward classical rate $I(X;Y)-I(Y;B)$ and shared uniform randomness rate $H(Y\mid X)$ , testing the full Eq.(6) output including both feedback copies and the original source registers.

This is an operational restatement at the direct corner. The relation is defined by physical source simulation codes; it does not assert a universal channel-norm simulation theorem.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P42

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P42

open scoped BigOperators ComplexConjugate ENNReal

open Filter

open QAlgorithms.Papers.Independent.Dependency50.P07

open QAlgorithms.Papers.Independent.Gap48.P20

open QAlgorithms.Papers.Independent.Information100.P27 (IsProbability shannon)

attribute [local instance] Classical.decEq Classical.propDecidable

/-- PDF p.14, Eq.(36): the source-relative resource inequality at the direct
coding corner I(X;Y)-I(Y;B) cbits and H(Y|X) shared random bits per copy. -/
theorem sourceResourceInequality {X B : Type} [Fintype X] [Fintype B]
    [Nonempty X] [Nonempty B] (E : CQData X B) (hE : E.Valid) (V : Auxiliary X) :
    SourceSimulation E V (auxCost E V) (shannon (auxProb E V) - auxIX E V) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P42

end

Source

Channel simulation with quantum side information, arXiv:quant-ph/0611008v1, PDF p. 14, Unnumbered main result: source resource inequality (36)

Read-back

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

Let $X,B$ be nonempty finite types with specified finite enumerations, let $p_x\ge0$ sum to $1$ , and let every complex matrix $\rho_x$ on $B$ be positive semidefinite with trace $1$ , including at labels of probability zero. Let an auxiliary system have positive size $y$ and probabilities $V(u\mid x)\ge0$ summing to $1$ over $u\in[y]$ . Define

\begin{gathered} w_{u,x}=p_xV(u\mid x),\quad q_u=\sum_xw_{u,x},\quad \sigma_u=q_u^{-1}\sum_xw_{u,x}\rho_x,\quad \bar\rho=\sum_xp_x\rho_x,\\ H(a)=-\sum_j a_j\log_2a_j,\quad S(A)=-\operatorname{Re}\operatorname{tr}\operatorname{cfc}(t\mapsto t\log_2t,A),\\ I_X=H(p)+H(q)-H(w),\quad I_B=S(\bar\rho)-\sum_uq_uS(\sigma_u),\\ R_*=I_X-I_B,\qquad C_*=H(q)-I_X, \end{gathered}

where $q_u^{-1}=0$ when $q_u=0$ , giving $\sigma_u=0$ . The declaration asserts $R_*,C_*\ge0$ and that for every $\varepsilon,\delta>0$ , all sufficiently large positive $n$ admit bit counts $c,h,p$ , encoding weights $e(x,\ell,m,s)\ge0$ summing to $1$ over $m,s$ , a decoder $d(\ell,m,s)\in[y]^{[n]}$ , and positive semidefinite matrices $F_{\ell,m,t}$ on $B^{[n]}$ summing to $I$ over $t$ , such that

h\le n(R_*+\delta),\qquad c\le n(C_*+\delta),\qquad \|T-O\|_1\le\varepsilon.

Here $\ell,m,s,t$ are bitstrings of lengths $c,h,p,p$ , with no bound on the private count $p$ . Writing $p_n(x)=\prod_ip_{x_i}$ and $(\rho_x^{(n)})_{b,b'}=\prod_i(\rho_{x_i})_{b_i,b'_i}$ , the target and output entries on tuples $(x,u,v,b)\in X^{[n]}\times[y]^{[n]}\times[y]^{[n]}\times B^{[n]}$ are

\begin{aligned} T_{(x,u,v,b),(x',u',v',b')} &=\mathbf1_{\{x=x',\,u=u',\,v=v',\,u=v\}}\, p_n(x)\prod_iV(u_i\mid x_i)(\rho_x^{(n)})_{b,b'},\\ O_{(x,u,v,b),(x',u',v',b')} &=\mathbf1_{\{x=x',\,u=u',\,v=v'\}} \sum_{\ell,m,s,t}\mathbf1_{\{d(\ell,m,s)=u,\,d(\ell,m,t)=v\}}\, p_n(x)2^{-c}e(x,\ell,m,s) [\mathcal L_{F_{\ell,m,t}}(\rho_x^{(n)})]_{b,b'}. \end{aligned}

The branch $\mathcal L_F(\sigma)$ is defined by relabeling onto a finite ordinal, forming $\operatorname{cfc}(\sqrt{\cdot},F)\sigma\operatorname{cfc}(\sqrt{\cdot},F)$ , and relabeling back; the norm is $\|Z\|_1=\operatorname{Re}\operatorname{tr}\operatorname{cfc}(\sqrt{\cdot},Z^\dagger Z)$ . The assertion includes zero probabilities and permits zero bit counts; its block lengths are positive.

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