Complete distributed-compression region for a Bell source

Open

QAlgorithms.Papers.Independent.Intakethird100.P11.bell_rateRegion

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

prove2quantum

Let $p_1,p_2,p_3,p_4\ge0$ sum to one, and consider the ordered ensemble of normalized Bell vectors

|\phi^\pm\rangle=\frac{|00\rangle\pm|11\rangle}{\sqrt2},\qquad |\psi^\pm\rangle=\frac{|01\rangle\pm|10\rangle}{\sqrt2}.

Let $H(p)=-\sum_{i=1}^4p_i\log_2p_i$ , with $0\log_20=0$ . For arbitrary real rates,

(R_A,R_B)\text{ is achievable}\quad\Longleftrightarrow\quad R_A\ge\frac{H(p)}2\quad\text{and}\quad R_B\ge\frac{H(p)}2.

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.

This identifies both individual rate thresholds, including distributions with zero entries and the deterministic case $H(p)=0$ .

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 pp.8–10, Theorem IV.1, (14): both individual inequalities and both
achievability directions, including H=0 and vanishing probabilities. -/
theorem bell_rateRegion (p : Fin 4 → ℝ) (hp : ∀ i, 0 ≤ p i)
    (htotal : ∑ i, p i = 1) (ra rb : ℝ) :
    FiniteAchievable p bellSourceVectors ra rb ↔ shannon p / 2 ≤ ra ∧ shannon p / 2 ≤ rb := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P11

end

Source

On the distributed compression of quantum information, arXiv:quant-ph/0403042v3, PDF p. 8, Theorem IV.1: complete Bell-source rate region

Read-back

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

For any four real weights $p_0,p_1,p_2,p_3\ge0$ summing to $1$ and any real rates $r_A,r_B$ , the following property holds if and only if $H(p)/2\le r_A$ and $H(p)/2\le r_B$ , where $H(p)=-\sum_{i=0}^3p_i\log_2p_i$ , with zero-weight terms equal to zero: for every $\delta,\varepsilon>0$ , there exists a natural number $N$ such that every natural number $n>N$ admits positive dimensions $d_A,d_B$ , separate encoders from matrices on $\{\mathrm{false},\mathrm{true}\}^n$ to dimensions $d_A,d_B$ , and a joint decoder back to the two length- $n$ registers, satisfying

\frac{\log_2d_A}{n}\le r_A+\delta, \qquad \frac{\log_2d_B}{n}\le r_B+\delta, \qquad \sum_{w\in\{0,1,2,3\}^n} \left(\prod_{t=0}^{n-1}p_{w(t)}\right) \operatorname{Re}\operatorname{tr}\!\left( \rho_w\,\mathcal D((\mathcal E_A\otimes\mathcal E_B)(\rho_w)) \right)\ge1-\varepsilon.

Each encoder and the decoder must have a finite Kraus representation $\Phi(X)=\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ , and their tensor action applies the encoders separately to the two registers. Here $V_w(a,b)=\prod_t v_{w(t)}(a(t),b(t))$ , $\rho_w=V_wV_w^\dagger$ , and

(v_0,v_1,v_2,v_3) = \frac1{\sqrt2} \bigl(e_{00}+e_{11},\ e_{00}-e_{11},\ e_{01}+e_{10},\ e_{01}-e_{10}\bigr),

with $0=\mathrm{false}$ , $1=\mathrm{true}$ , and $e_{ab}$ the corresponding coordinate unit vector. Zero probabilities are allowed, and the rate inequalities use non-strict comparison.

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