Theorem 3.1: channel simulation with quantum side information

Open

QAlgorithms.Papers.Independent.Intakethird100.P42.channelSimulation

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

prove2quantum

Let $X$ be a finite nonempty alphabet, $B$ a finite nonzero quantum register, and $\{p(x),\rho_x^B\}$ a normalized classical–quantum source. Every $\rho_x^B$ is a density operator, including when $p(x)=0$ . Let $W(y\mid x)$ be a stochastic channel on a finite nonempty output alphabet $Y$ . All information quantities below are in bits in the state $\rho^{XYB}=\sum_{x,y}p(x)W(y\mid x)|x,y\rangle\langle x,y|\otimes\rho_x^B$ .

For nonnegative rates $R,C$ , a pair is achievable exactly when

R\ge I(X;Y)-I(Y;B),\qquad R+C\ge H(Y\mid B).

Achievability means that for every error $\epsilon>0$ and rate slack $\delta>0$ , every sufficiently large positive blocklength $n$ admits a code with at most $n(R+\delta)$ forward classical bits and $n(C+\delta)$ independent uniform shared bits. Alice uses private stochastic encoding, Bob uses a coin/message-controlled POVM with its square-root instrument, and both retain their output $Y^n$ . The full trace-norm error on the original $X^n$ , both output copies, and postmeasurement $B^n$ is at most $\epsilon$ , with no factor $1/2$ .

This gives the complete source-relative classical communication–common randomness trade-off while preserving quantum side information.

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.5, Theorem 3.1: exact rate region, with preservation of Bob's quantum
source and both feedback outputs. All information is computed in Eq.(2). -/
theorem channelSimulation {X B : Type} [Fintype X] [Fintype B]
    [Nonempty X] [Nonempty B] (E : CQData X B) (hE : E.Valid)
    (V : Auxiliary X) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) :
    SimulationAchievable E V R C ↔
      auxCost E V ≤ R ∧ shannon (auxProb E V) - auxIQ E V ≤ R + C := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P42

end

Source

Channel simulation with quantum side information, arXiv:quant-ph/0611008v1, PDF p. 5, Theorem 3.1: channel simulation with quantum side information

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$ satisfy $\sum_xp_x=1$ , and let every $\rho_x$ be a positive semidefinite complex matrix on $B$ with trace $1$ , including for labels with $p_x=0$ . Let $y>0$ and $V(u\mid x)\ge0$ satisfy $\sum_{u\in[y]}V(u\mid x)=1$ , and let $R,C\ge0$ be real. Define

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

The reciprocal at $q_u=0$ is defined to be zero, so $\sigma_u=0$ in that case. The assertion is that $I_X-I_B\le R$ and $H(q)-I_B\le R+C$ hold if and only if the following operational condition holds: for every $\varepsilon,\delta>0$ , all sufficiently large positive $n$ admit bit counts $c,h,p$ , nonnegative weights $e(x,\ell,m,s)$ summing to $1$ over $m,s$ , decoded words $d(\ell,m,s)\in[y]^{[n]}$ , and matrices $F_{\ell,m,t}\succeq0$ on $B^{[n]}$ summing to $I$ over $t$ , with

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$ , the private count $p$ is unrestricted, $p_n(x)=\prod_ip_{x_i}$ , $(\rho_x^{(n)})_{b,b'}=\prod_i(\rho_{x_i})_{b_i,b'_i}$ , and the matrices indexed by $(x,u,v,b)$ 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}

In these formulas $x\in X^{[n]}$ , $u,v\in[y]^{[n]}$ , $b\in B^{[n]}$ , $\mathcal L_F(\sigma)$ relabels onto a finite ordinal, forms $\operatorname{cfc}(\sqrt{\cdot},F)\sigma\operatorname{cfc}(\sqrt{\cdot},F)$ , and relabels back, and $\|Z\|_1=\operatorname{Re}\operatorname{tr}\operatorname{cfc}(\sqrt{\cdot},Z^\dagger Z)$ . Zero individual probabilities and zero bit counts are 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