Concatenating a source identity with a relative communication identity

Open

QAlgorithms.Papers.Independent.Intakethird100.P64.sourceIdentityConcatenation

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

prove2quantum

Let $S$ be a finite nonzero source register with density matrix $\rho$ , purified by a unit vector $|\phi\rangle^{RS}$ . The reference $R$ is inaccessible to Alice and Bob. The registers $\widehat A,A',B,\widehat B$ are identified copies of $S$ , so the two occurrences of $\rho$ denote the same density under relabeling. Then

\langle\mathrm{id}^{S\to\widehat A}:\rho\rangle+ \langle\mathrm{id}^{A'\to B}:\rho\rangle \ge\langle\mathrm{id}^{S\to\widehat B}:\rho\rangle.

For every positive error and rate slack, all sufficiently large positive $n$ have local encoding and decoding maps using $n$ supplied identity-channel calls on the $n$ Source-supplied systems. For every positive input-promise tolerance $\eta$ , the actual encoded input marginal is within $\eta$ of $\rho^{\otimes n}$ . The code succeeds jointly with $R^n$ for every physical implementation of the relative identity satisfying its joint error guarantee on inputs with that near-IID marginal. The local maps are chosen before that implementation is supplied. No additional communication or shared state is supplied.

This is direct routing of the specified source, rather than a general transitivity principle for arbitrary resources.

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 display and Fig.3: concatenate the Source-to-Alice
identity with the relative Alice-to-Bob identity for the same rho. The actual
source purification and the encoder's marginal are part of the operational test. -/
theorem sourceIdentityConcatenation {R S : Type} [Fintype R] [Fintype S]
    [Nonempty R] [Nonempty S] (phi : EuclideanSpace ℂ (R × S))
    (hphi : IsState phi) : SourceRoutingAchievable phi := 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/identity concatenation

Read-back

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

For nonempty types $R,S$ equipped with finite enumerations and every vector $\phi\in\mathbb C^{R\times S}$ with $\|\phi\|=1$ , define

\rho_{s,t}=\sum_r\phi(r,s)\overline{\phi(r,t)},\qquad D_n[(r,s),(r',t)] =\prod_{i=0}^{n-1}\phi(r_i,s_i)\, \overline{\prod_{i=0}^{n-1}\phi(r'_i,t_i)},\qquad (\rho^{\otimes n})_{s,t}=\prod_i\rho_{s_i,t_i}.

The theorem asserts that for every $\varepsilon>0,\delta>0$ , there exists $N\in\mathbb N$ such that for every $n\ge N$ with $n\ge1$ , there exist channels $\mathcal E,\mathcal D$ on matrices indexed by $S^n$ satisfying $n\le n(1+\delta)$ and, for every $\eta>0$ ,

\left\|\operatorname{tr}_{R^n}(\operatorname{id}_{R^n}\otimes\mathcal E)(D_n) -\rho^{\otimes n}\right\|_1\le\eta,

and the following statement for every channel $F$ on those matrices: if, for every positive integer $d$ and 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 \ \Longrightarrow\ \|(\operatorname{id}_d\otimes F)(\sigma)-\sigma\|_1\le\varepsilon,

then

\|(\operatorname{id}_{R^n}\otimes(\mathcal D\circ F\circ\mathcal E))(D_n)-D_n\|_1 \le\varepsilon.

A channel here means a matrix function $T(X)=\sum_{j=0}^{a-1}K_jXK_j^\dagger$ for some finite Kraus family with $\sum_jK_j^\dagger K_j=I$ ; partial traces sum diagonal blocks, and tensoring $T$ with an identity applies $T$ to each reference-index block. The trace norm is $\|M\|_1=\operatorname{Re}\operatorname{tr}\sqrt{M^\dagger M}$ . The channels are chosen independently of $\eta$ , so their displayed marginal difference must have norm zero.

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