Fully quantum Slepian-Wolf with joint source and Bell output

Open

QAlgorithms.Papers.Independent.Intakethird100.P64.fullyQuantumSlepianWolf

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

prove2quantum

Let $R,S,A,B$ be finite nonzero registers, let $|\phi\rangle^{RS}$ be a unit vector supplied by a separate Source, and let $U:S\to A\otimes B$ be an isometry. Set $|\psi\rangle^{RAB}=(I_R\otimes U)|\phi\rangle$ and $\rho^S=\operatorname{Tr}_R|\phi\rangle\langle\phi|$ . Alice receives $A$ and Bob receives $B$ ; neither controls the Source input. Entropies and mutual informations are in bits. Then

\langle U^{S\to AB}:\rho^S\rangle+ \tfrac12 I(R;A)_\psi[q\to q] \ge\tfrac12 I(A;B)_\psi[qq]+ \langle\mathrm{id}^{S\to\widehat B}:\rho^S\rangle.

For every $\varepsilon,\delta>0$ , all sufficiently large positive $n$ admit local isometric encoding and decoding dilations with retained local work. Alice sends a $q$ -qubit register to Bob and keeps one half of each of $l$ generated Bell pairs. Bob receives the other halves and a copy $\widehat B^n$ of $S^n$ , where

q\le\lfloor n(I(R;A)_\psi/2+\delta)\rfloor,\qquad l\ge\max\{0,\lfloor n(I(A;B)_\psi/2-\delta)\rfloor\}.

After tracing local work, the complete output on $R^n,\widehat B^n$ and both Bell registers is within full trace norm $\varepsilon$ of $|\phi\rangle\langle\phi|^{\otimes n}\otimes\Phi^{\otimes l}$ . The protocol uses no input Bell pairs or other nonlocal assistance and never acts on $R$ .

This transfers the source and generates entanglement simultaneously. The paper attributes the FQSW inequality to [11]; the statement does not claim that arbitrary discarded-work protocols can be reversed.

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.3, (12), and p.4, Fig.4; attributed there to [11]: fully quantum
Slepian-Wolf. Source-controlled phi is distributed only by U. The fixed code
transfers the original S to Bob and produces independent Bell pairs, jointly
with untouched R, at the displayed two rates. Isometric dilations retain work. -/
theorem fullyQuantumSlepianWolf {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)
    (phi : EuclideanSpace ℂ (R × S)) (hphi : IsState phi) :
    SourceTransferAchievable U phi
      (mutualRA (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. 3, Equation (12) and Figure 4: fully quantum Slepian-Wolf

Read-back

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

For any finite, nonempty types $R,S,A,B$ , any complex matrix $U:\mathbb C^S\to\mathbb C^{A\times B}$ satisfying $U^\dagger U=I$ , and any $\phi\in\mathbb C^{R\times S}$ with $\|\phi\|=1$ , define $\psi(r,a,b)=\sum_{s\in S}U((a,b),s)\phi(r,s)$ . For each collection $J$ of these registers, let $\rho_J$ be the matrix obtained from $|\psi\rangle\langle\psi|$ by summing over equal row and column indices in the omitted registers, and write $H(\rho)=-\operatorname{Re}\operatorname{Tr}(f(\rho))$ , where $f(x)=x\log_2x$ is applied by continuous functional calculus. Put

Q=\frac{H(\rho_R)+H(\rho_A)-H(\rho_{RA})}{2}, \qquad E=\frac{H(\rho_A)+H(\rho_B)-H(\rho_{AB})}{2}.

For every pair of real numbers $\varepsilon>0$ and $\delta>0$ , there is a natural number $N$ such that, for every natural number $n\ge N$ with $n\ge1$ , there exist natural numbers $q,l,w_A,w_B$ and complex matrices

V_A:\mathbb C^{A^n}\longrightarrow \mathbb C^{(\{0,1\}^l\times\{0,1\}^q)\times\{0,\ldots,w_A\}}, \qquad V_B:\mathbb C^{\{0,1\}^q\times B^n}\longrightarrow \mathbb C^{(\{0,1\}^l\times S^n)\times\{0,\ldots,w_B\}},

such that $V_A^\dagger V_A=I$ , $V_B^\dagger V_B=I$ , $q\le\lfloor n(Q+\delta)\rfloor_+$ , and $\lfloor n(E-\delta)\rfloor_+\le l$ . Start with the vector on $R^n\times(A^n\times B^n)$ having amplitude $\prod_{i=0}^{n-1}\psi(r_i,a_i,b_i)$ ; apply $V_A$ to $A^n$ , send its $q$ -bit register to $V_B$ , apply $V_B$ together with $B^n$ , and discard both work registers. The resulting matrix $\Omega$ , retaining $R^n$ , satisfies $\|\Omega-|\tau\rangle\langle\tau|\|_1\le\varepsilon$ , where

\tau(r,u,v,s)= \left(\prod_{i=0}^{n-1}\phi(r_i,s_i)\right) \begin{cases}2^{-l/2},&u=v,\\0,&u\ne v.\end{cases}

Here $(|v\rangle\langle v|)_{ab}=v_a\overline{v_b}$ , $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ , and $\lfloor x\rfloor_+=\max(0,\lfloor x\rfloor)$ . In particular, when $E-\delta\le0$ , the lower bound on $l$ is zero. All four code parameters may be zero, zero-bit registers are singletons, and the work-register dimensions are $w_A+1,w_B+1$ ; block length zero is excluded by the explicit condition $n\ge1$ .

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