Unnumbered result: FQRS-derived redistribution inner bound

Let $A,C,B,R$ be nonempty finite types and let $\psi\in\mathbb C^{R\times(A\times(C\times B))}$ have norm $1$. Define $\rho_{uv}=\psi_u\overline{\psi_v}$, reduce to any register collection $U$ by summing over equal complementary labels, and put $S(U)=-\operatorname{Re}\operatorname{tr}(f(\rho_U))$, where $f(t)=t\log_2t$ is applied by continuous functional calculus and $0\log_20=0$. Set

The theorem asserts $Q_0\ge0$ and the following quantified existence statement: for every $\varepsilon,\delta>0$, some natural $N$ works for every $n\ge N$ with $n\ge1$, so that there exist natural numbers $q,k,l$, an encoder channel $A^nC^n\otimes(\mathbb C^2)^{\otimes k}\to A^n\otimes(\mathbb C^2)^{\otimes l}\otimes(\mathbb C^2)^{\otimes q}$, and a decoder channel $(\mathbb C^2)^{\otimes q}\otimes B^n\otimes(\mathbb C^2)^{\otimes k}\to C^nB^n\otimes(\mathbb C^2)^{\otimes l}$. Here each channel acts on matrices by a finite sum $\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$. On the initial vector $\psi^{\otimes n}\otimes\Phi_k$, where $\Phi_h=2^{-h/2}\sum_{z\in\{0,1\}^h}|z,z\rangle$, the encoder followed by the decoder, with $R^n$ untouched, produces a matrix $\omega_n$ such that

The target retains $A^n$ at the encoder and places $C^nB^n$ at the decoder, and $\|M\|_1=\operatorname{Re}\operatorname{tr}\sqrt{M^\dagger M}$. The natural numbers $q,k,l$ may be zero.