Unnumbered result: FQSW-derived redistribution inner bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P42.fqswInnerBound

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

prove2quantum

Let $|\psi\rangle^{R\widehat A\widehat B B}$ be a normalized pure state on finite nonzero registers. Initially Alice holds $\widehat A\widehat B$ , Bob holds $B$ , and $R$ is inaccessible. Alice must transfer $\widehat B$ to Bob while retaining $\widehat A$ and preserving the complete source and reference.

With one-way qubit communication and arbitrary local CPTP maps, the FQSW construction achieves the rate pair

(Q_1,E_1)=\left(\tfrac12 I(\widehat B;R\widehat A)_\psi,-\tfrac12 I(B;\widehat B)_\psi\right).

Here rates and entropies are in bits; $E$ is signed Bell consumption, with distinct natural input and output Bell counts and $E<0$ denoting generation. For every positive error and rate slack, all sufficiently large positive IID blocks have a protocol with full joint source/reference and final Bell-pair trace-norm error within the error tolerance.

This gives the source's merging-based inner bound. Treating $\widehat A$ as reference in the construction does not remove it from Alice's final output.

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 pp.17--18: FQSW-derived achievable pair. Ahat remains Alice's final
register although this construction treats it as reference. E is NEGATIVE. -/
theorem fqswInnerBound {A C B R : Type}
    [Fintype A] [Fintype C] [Fintype B] [Fintype R]
    [Nonempty A] [Nonempty C] [Nonempty B] [Nonempty R]
    (psi : EuclideanSpace ℂ (RedistributionSource A C B R)) (hpsi : IsState psi) :
    RedistributionAchievable psi (mergingClassicalCost psi / 2) (-redistributionReceiverInformation psi / 2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P42

end

Source

Channel simulation with quantum side information, arXiv:quant-ph/0611008v1, PDF p. 18, Unnumbered result: FQSW-derived redistribution inner bound

Read-back

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

Let $A,C,B,R$ be nonempty finite types and let $\psi\in\mathbb C^{R\times(A\times(C\times B))}$ satisfy $\|\psi\|=1$ . For each collection $U$ of registers, obtain $\rho_U$ from $\rho_{uv}=\psi_u\overline{\psi_v}$ by summing entries over equal complementary labels, and write $S(U)=-\operatorname{Re}\operatorname{tr}(f(\rho_U))$ , where $f(t)=t\log_2t$ is applied by continuous functional calculus, with $0\log_20=0$ . Set

Q_0=\frac{S(RA)+S(C)-S(RAC)}2, \qquad E_0=-\frac{S(C)+S(B)-S(CB)}2.

The assertion is that $Q_0\ge0$ and that, for every $\varepsilon>0$ and $\delta>0$ , there is a natural number $N$ such that every $n\ge N$ with $n\ge1$ admits natural numbers $q,k,l$ and two channels: an encoder from $A^nC^n$ together with $k$ qubits to $A^n$ , $l$ qubits, and a $q$ -qubit message, and a decoder from that message together with $B^n$ and $k$ qubits to $C^nB^n$ and $l$ qubits. Each channel has a finite Kraus representation $\Phi(X)=\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ . Starting from $\psi^{\otimes n}$ and the shared vector $\Phi_k=2^{-k/2}\sum_{z\in\{0,1\}^k}|z,z\rangle$ , applying the encoder and then the decoder while leaving $R^n$ unchanged produces a matrix $\omega_n$ satisfying

\left\|\omega_n-\bigl|\psi^{\otimes n}\otimes\Phi_l\bigr\rangle \bigl\langle\psi^{\otimes n}\otimes\Phi_l\bigr|\right\|_1\le\varepsilon, \qquad q\le n(Q_0+\delta),\qquad k-l\le n(E_0+\delta).

The target coordinates place $A^n$ with the encoder and $C^nB^n$ with the decoder; $\|M\|_1=\operatorname{Re}\operatorname{tr}\sqrt{M^\dagger M}$ . Zero values of $q,k,l$ are permitted, and $E_0$ is not required to be nonnegative.

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