Schumacher compression as source transfer

Open

QAlgorithms.Papers.Independent.Intakethird100.P64.sourceSchumacher

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

prove2quantum

Let $|\phi\rangle^{RS}$ be a unit purification of a density matrix $\rho^S$ on a finite nonzero register $S$ . A separate Source delivers $S$ to Alice and retains its inaccessible purifying reference $R$ . All target registers are identified copies of $S$ . With entropy measured in bits,

\langle\mathrm{id}^{S\to\widehat A}:\rho^S\rangle+ H(S)_\rho[q\to q]\ge \langle\mathrm{id}^{S\to\widehat B}:\rho^S\rangle.

For every $\varepsilon,\delta>0$ and every sufficiently large positive $n$ , physical local encoding and decoding maps transfer the purification to Bob, with joint full trace-norm error at most $\varepsilon$ , using at most $\lfloor n(H(S)_\rho+\delta)\rfloor$ forward qubits. No Bell pairs or other nonlocal assistance are supplied. Local isometric dilations may retain work registers. Any additional generated Bell output may be discarded.

This expresses compression as preserving a Source-controlled quantum system. At entropy zero it permits sublinear communication; it does not assert a nontrivial zero-message finite-block channel.

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, unnumbered compression display: the Source supplies rho at Alice;
H(S)_rho forward qubits per source copy suffice to transfer its full purification
to Bob. Rate zero permits sublinear communication. No input ebits are supplied. -/
theorem sourceSchumacher {R S : Type} [Fintype R] [Fintype S]
    [Nonempty R] [Nonempty S] (phi : EuclideanSpace ℂ (R × S))
    (hphi : IsState phi) :
    SourceTransferAchievable (sourceToAlice S) phi
      (vnEntropy (traceLeft (pureDensity phi))) 0 := 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, Fully quantum Slepian-Wolf preamble: source formulation of compression

Read-back

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

For any finite, nonempty types $R,S$ and vector $\phi\in\mathbb C^{R\times S}$ with $\|\phi\|=1$ , put $\rho_S(s,t)=\sum_{r\in R}\phi(r,s)\overline{\phi(r,t)}$ and $H(\rho)=-\operatorname{Re}\operatorname{Tr}(f(\rho))$ , where $f(x)=x\log_2x$ is applied by continuous functional calculus. 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^{S^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\{\ast\}^n}\longrightarrow \mathbb C^{(\{0,1\}^l\times S^n)\times\{0,\ldots,w_B\}},

satisfying $V_A^\dagger V_A=I$ , $V_B^\dagger V_B=I$ , and $q\le\lfloor n(H(\rho_S)+\delta)\rfloor_+$ , with the following error bound. Start with the vector on $R^n\times(S^n\times\{\ast\}^n)$ having amplitude $\prod_{i=0}^{n-1}\phi(r_i,s_i)$ ; apply $V_A$ to $S^n$ , send its $q$ -bit register to the input of $V_B$ , apply $V_B$ together with the singleton register, and discard both work registers. If $\Omega$ is the resulting matrix, retaining $R^n$ , then $\|\Omega-|\tau\rangle\langle\tau|\|_1\le\varepsilon$ , where the target vector on $R^n\times(\{0,1\}^l\times(\{0,1\}^l\times S^n))$ has amplitudes

\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}$ , and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ , with the square root defined by continuous functional calculus. The additional required inequality is $\lfloor n(0-\delta)\rfloor_+\le l$ ; since $\lfloor x\rfloor_+=\max(0,\lfloor x\rfloor)$ , this is simply $0\le l$ . Thus no upper bound on $l$ is asserted. The numbers $q,l,w_A,w_B$ may be zero; a zero-bit register is a singleton, while each work register has respectively $w_A+1$ or $w_B+1$ basis elements.

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