Exact entanglement-assisted isotropic-qubit curve

Open

QAlgorithms.Papers.Independent.Intakethird100.P27.isotropic_entanglement_assisted

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

prove2quantum

Consider the memoryless maximally mixed qubit source $I/2$ , with the Bell purification $\Phi_{RA}$ and fidelity-distortion observable $I-\Phi_{RA}$ . Let $R^q_{\mathrm{ea}}(D)$ be its operational quantum rate-distortion function with unlimited prior entanglement and no free classical side channel. For $0\le D\le1$ ,

R^q_{\mathrm{ea}}(D)=\begin{cases}1-\tfrac12 H(1-D,D/3,D/3,D/3),&D\le3/4,\\0,&D>3/4.\end{cases}

Here $H(p)=-\sum_i p_i\log_2p_i$ , with $0\log_2 0=0$ . The branches agree at $D=3/4$ .

This gives an exact assisted curve, with rate one at zero distortion and zero from distortion $3/4$ onward.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P27

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P27

open Filter

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P19
  (first marginalRB mutualInformation bipartiteBlock epr)

open QAlgorithms.Papers.Independent.Information100.P08 (formation)

open QAlgorithms.Papers.Independent.Gap48.P20 (redistributionMarginal)

open QAlgorithms.Papers.Independent.Bridge50.P37 (isotropicState normalizedEntangledProjection)

/-- PDF pp.8--9, Theorem 11: exact isotropic-qubit assisted curve. The Bell
purification and fidelity observable are pinned by equalities, not postulated
entropy values. The two branches agree at D=3/4. The p.9 proof's 'fidelity p'
is a typo; for its Pauli channel fidelity is 1-p and distortion is p. -/
theorem isotropic_entanglement_assisted
    (S : DistortionSource (Fin 2) (Fin 2))
    (hsource : pureDensity S.psi = epr 2)
    (hdelta : S.delta = 1 - epr 2)
    (D : ℝ) (hD0 : 0 ≤ D) (hD1 : D ≤ 1) :
    rateDistortion S .entanglement D =
      ENNReal.ofReal (if D ≤ 3 / 4 then 1 - isotropicEntropy D / 2 else 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P27

end

Source

Quantum rate distortion coding with auxiliary resources, arXiv:1212.5316v3, PDF p. 8, Theorem 11

Read-back

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

Let $S$ be a source on $A=B=\operatorname{Fin}(2)$ , consisting of a unit vector $\psi\in\mathbb C^{A\times A}$ and a positive semidefinite distortion matrix $\Delta$ . Assume

\psi\psi^\dagger=P,\qquad \Delta=I-P, \qquad P((i,j),(i',j'))= \begin{cases} \frac12,&i=j\ \text{and }i'=j',\\ 0,&\text{otherwise}. \end{cases}

For every real $D$ with $0\le D\le1$ , the rate defined below equals

\max\!\left( \begin{cases} 1-\frac12H_4(D),&D\le\frac34,\\ 0,&D>\frac34, \end{cases} 0\right), \qquad H_4(D)=-(1-D)\log_2(1-D)-3\frac D3\log_2\frac D3,

viewed in $[0,\infty]$ , with zero logarithmic terms taken as zero. The rate is the infimum in $[0,\infty]$ of all nonnegative real $r$ such that, for every $\varepsilon,s>0$ , every sufficiently large positive $n$ admits positive integers $q,h$ , a positive semidefinite trace-one shared matrix $\tau$ on $\operatorname{Fin}(h)\times\operatorname{Fin}(h)$ , an encoder from $A^n\times\operatorname{Fin}(h)$ to $\operatorname{Fin}(q)$ , and a decoder from $\operatorname{Fin}(q)\times\operatorname{Fin}(h)$ to $B^n$ . Both maps must have finite Kraus representations with Kraus adjoint-products summing to the identity; the classical register has dimension $1$ . Apply these maps to the second halves of $n$ copies of $\psi$ and the shared matrix, leaving the reference halves unchanged, to obtain $X$ on $A^n\times B^n$ . The bounds required are

\log_2q\le n(r+s), \qquad \frac1n\sum_{i<n}\operatorname{Re}\operatorname{Tr}((I-P)X_i)\le D+\varepsilon,

where $X_i$ sums over equal row and column indices outside position $i$ . The shared dimension is unrestricted. The stated formula includes $D=0$ , $D=3/4$ , and $D=1$ .

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