Fully quantum reverse Shannon with feedback and a relative input promise

Open

QAlgorithms.Papers.Independent.Intakethird100.P64.fullyQuantumReverseShannon

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

prove2quantum

Let $R,S,A,B$ be finite nonzero complex registers. Alice controls $S$ and retains $A$ ; Bob receives $B$ . Let $U:S\to A\otimes B$ be an isometry, let $\rho$ be a density matrix on $S$ , and let $|\phi\rangle^{RS}$ be a unit purification of $\rho$ . Set $|\psi\rangle=(I_R\otimes U)|\phi\rangle$ . Entropies are in bits and $I(X;Y)=H(X)+H(Y)-H(XY)$ .

Then the following asymptotic resource inequality holds:

\tfrac12 I(R;B)_\psi[q\to q]+\tfrac12 I(A;B)_\psi[qq]\ge\langle U:\rho\rangle.

For every error $\varepsilon>0$ and rate slack $\delta>0$ , there are $\eta>0$ and a threshold $N$ such that every $n\ge N$ , $n\ge1$ admits local physical encoding and decoding operations. They consume at most $\lfloor n(I(R;B)_\psi/2+\delta)\rfloor$ forward qubits and $\lfloor n(I(A;B)_\psi/2+\delta)\rfloor$ normalized Bell pairs. These operations are chosen before any test input. For every finite reference $T$ and joint density $\sigma^{TS^n}$ whose $S^n$ marginal is within full trace norm $\eta$ of $\rho^{\otimes n}$ , the complete output on $T,A^n,B^n$ is within full trace norm $\varepsilon$ of $(I_T\otimes U^{\otimes n})\sigma(I_T\otimes U^{\otimes n})^\dagger$ . No nonlocal assistance is left uncounted.

This is the simulation arm of reversible feedback-channel decomposition; the source attributes its coherent construction to [9].

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P64

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P64

open QAlgorithms

open QAlgorithms.Papers.Independent.Gap48.P20
  (Copies redistributionMarginal subsystemEntropy forwardApply)

open QAlgorithms.Papers.Independent.Dependency50.P48 (densityPower)

open scoped Matrix ComplexConjugate

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.2, (5), attributed there to [9]: fully quantum reverse Shannon.
U is a feedback isometry, rho is a density matrix, phi its normalized purification,
and the two coefficients are computed from (id_R tensor U)phi. Simulation includes
Alice's feedback and every allowed reference correlation, under the near-IID promise. -/
theorem fullyQuantumReverseShannon {R S A B : Type}
    [Fintype R] [Fintype S] [Fintype A] [Fintype B]
    [Nonempty R] [Nonempty S] [Nonempty A] [Nonempty B]
    (U : Matrix (A × B) S ℂ) (hU : Uᴴ * U = 1)
    (rho : Matrix S S ℂ) (hrho : IsDensityMatrix rho)
    (phi : EuclideanSpace ℂ (R × S)) (hphi : IsState phi)
    (hpurification : traceLeft (pureDensity phi) = rho) :
    RelativeSimulationAchievable U rho
      (mutualRB (feedbackOutputVector U phi) / 2) (mutualAB (feedbackOutputVector U phi) / 2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P64

end

Source

A triangle of dualities: reversibly decomposable quantum channels, source-channel duality, and time reversal, arXiv:quant-ph/0505138v1, PDF p. 2, Equation (5): fully quantum reverse Shannon inequality

Read-back

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

Let $R,S,A,B$ be nonempty types equipped with finite enumerations, let $U:\mathbb C^S\to\mathbb C^{A\times B}$ satisfy $U^\dagger U=I$ , let $\rho$ be positive semidefinite with $\operatorname{tr}\rho=1$ , and let $\phi\in\mathbb C^{R\times S}$ satisfy $\|\phi\|=1$ and $\sum_r\phi(r,s)\overline{\phi(r,t)}=\rho_{s,t}$ . Put $\psi(r,a,b)=\sum_sU_{(a,b),s}\phi(r,s)$ , form its outer-product matrix, and let $H(T)$ denote the entropy of its reduction to registers $T$ , namely $-\operatorname{Re}\operatorname{tr}f(\omega_T)$ with $f(x)=x\log_2x$ applied by continuous functional calculus. Define

Q_0=\frac{H(R)+H(B)-H(RB)}2,\qquad E_0=\frac{H(A)+H(B)-H(AB)}2.

The theorem asserts that for every $\varepsilon>0,\delta>0$ , there exist $\eta>0$ and $N\in\mathbb N$ such that for every $n\ge N$ with $n\ge1$ , there are natural numbers $q,k,w_A,w_B$ and matrices

V:\mathbb C^{S^n\times\mathcal B_k}\to \mathbb C^{(A^n\times\mathcal B_q)\times\{0,\ldots,w_A\}}, \qquad W:\mathbb C^{\mathcal B_q\times\mathcal B_k}\to \mathbb C^{B^n\times\{0,\ldots,w_B\}},

satisfying $V^\dagger V=I$ , $W^\dagger W=I$ , $q\le\lfloor n(Q_0+\delta)\rfloor_+$ , and $k\le\lfloor n(E_0+\delta)\rfloor_+$ , where $\mathcal B_j=\{0,1\}^j$ and $\lfloor x\rfloor_+=\max(0,\lfloor x\rfloor)$ . Define

\begin{aligned} K_{\alpha\beta}[(a,b),s] &=2^{-k/2}\sum_{u\in\mathcal B_k}\sum_{m\in\mathcal B_q} V_{((a,m),\alpha),(s,u)}W_{(b,\beta),(m,u)},\\ \mathcal C_n(X)&=\sum_{\alpha=0}^{w_A}\sum_{\beta=0}^{w_B} K_{\alpha\beta}XK_{\alpha\beta}^\dagger,\qquad U_n[(a,b),s]=\prod_{i=0}^{n-1}U_{(a_i,b_i),s_i}. \end{aligned}

Then, for every positive integer $d$ and every positive semidefinite trace-one matrix $\sigma$ on $\{0,\ldots,d-1\}\times S^n$ ,

\left\|\operatorname{tr}_{\{0,\ldots,d-1\}}\sigma-\rho^{\otimes n}\right\|_1\le\eta \quad\Longrightarrow\quad \left\|(\operatorname{id}_d\otimes\mathcal C_n)(\sigma) -(\operatorname{id}_d\otimes[X\mapsto U_nXU_n^\dagger])(\sigma)\right\|_1 \le\varepsilon.

Here $(\rho^{\otimes n})_{s,t}=\prod_i\rho_{s_i,t_i}$ , partial traces sum diagonal blocks, tensoring a matrix function with an identity means applying it separately to each reference-index block, and $\|M\|_1=\operatorname{Re}\operatorname{tr}\sqrt{M^\dagger M}$ . The natural code parameters may be zero; the asserted 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