The uniform four-qubit erasure-code source admits (2,1)

Open

QAlgorithms.Papers.Independent.Intakethird100.P11.erasure_ratePair

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

prove2quantum

Let $\mathcal C\subset(\mathbb C^2)^{\otimes4}$ be the span of the following orthonormal vectors:

\frac{|0000\rangle+|1111\rangle}{\sqrt2},\quad \frac{|0011\rangle+|1100\rangle}{\sqrt2},\quad \frac{|0101\rangle+|1010\rangle}{\sqrt2},\quad \frac{|1001\rangle+|0110\rangle}{\sqrt2}.

The source draws a Haar-uniform unit vector from the whole four-dimensional subspace $\mathcal C$ , gives Alice its first two qubits and Bob its last two, and repeats this independently at each position. Then

(R_A,R_B)=(2,1)\text{ is achievable}.

An achievable pair uses independent blind local CPTP encoders, one noiseless quantum link from each sender, and a joint CPTP decoder, without supplied shared entanglement or side messages. For every $\delta,\epsilon>0$ , every sufficiently large positive integer blocklength $n$ admits positive compressed dimensions $d_A,d_B$ with $\log_2(d_A)/n\le R_A+\delta$ , $\log_2(d_B)/n\le R_B+\delta$ , and ensemble-average pure-input overlap with the reconstructed density operator at least $1-\epsilon$ . Draws are independent and identically distributed; this is squared fidelity, without a purifying reference.

Uniformity includes all superpositions in $\mathcal C$ , and is realized by the first column of normalized Haar $U(4)$ followed by the displayed code-space isometry. This gives an achievable point; optimality is left open.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P11

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P11

open MeasureTheory Filter

open scoped BigOperators ComplexConjugate Matrix

open QAlgorithms.Papers.Independent.Dependency50.P19 (both)

open QAlgorithms.Papers.Independent.Information100.P27 (shannon)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.5, Erasure codes example: the full continuous uniform source admits (2,1).
No claim of optimality or restriction to a finite codeword ensemble is made. -/
theorem erasure_ratePair : DistributedAchievable (fun c => erasureFidelity c) 2 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P11

end

Source

On the distributed compression of quantum information, arXiv:quant-ph/0403042v3, PDF p. 5, Section II: erasure-code example admits (2,1)

Read-back

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

For every $\delta>0$ and every $\varepsilon>0$ , there exists a natural number $N$ such that, for every natural number $n>N$ , there are positive natural numbers $d_A,d_B$ and a distributed block code consisting of separate encoding channels $E_A,E_B$ from two length- $n$ four-dimensional registers to dimensions $d_A,d_B$ , followed by a decoding channel $D$ back to the original registers, such that

\frac{\log_2d_A}{n}\le2+\delta,\qquad \frac{\log_2d_B}{n}\le1+\delta,\qquad 1-\varepsilon\le \int_{U(4)^n} \operatorname{Re}\operatorname{tr}\!\left(P_w\, D\bigl((E_A\otimes E_B)(P_w)\bigr)\right)\,dH^{\otimes n}(w).

Here every channel admits a finite Kraus representation $X\mapsto\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=1$ , and $H$ is normalized Haar measure. For $w=(U_0,\ldots,U_{n-1})$ , the matrix $P_w$ is $V_wV_w^\dagger$ , where $V_w(a,b)=\prod_t v(U_t)(a_t,b_t)$ and

v(U)=\frac{ U_{00}(e_{00}+e_{33})+U_{10}(e_{03}+e_{30}) +U_{20}(e_{11}+e_{22})+U_{30}(e_{21}+e_{12}) }{\sqrt2};

the $e_{ab}$ are coordinate unit vectors.

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