Achievable hybrid rate for the displayed opposite-parity family

Open

QAlgorithms.Papers.Independent.Intakethird100.P11.hybrid_ratePair

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

prove2quantum

Let $p_0,p_1\ge0$ sum to one, and let $\alpha_i,\beta_i\in\mathbb C$ satisfy $|\alpha_i|^2+|\beta_i|^2=1$ . Consider the displayed family

|\phi_0\rangle=\alpha_0|00\rangle+\beta_0|11\rangle,\qquad |\phi_1\rangle=\alpha_1|01\rangle+\beta_1|10\rangle.

Write $\rho=\sum_i p_i|\phi_i\rangle\langle\phi_i|$ and $\rho_B=\operatorname{Tr}_A\rho$ . On measuring Alice in the computational basis, let $q_j$ be the probability of outcome $j$ , and $\omega_j$ Bob's conditional density. Explicitly,

\begin{aligned} q_0&=\sum_i p_i|\alpha_i|^2,&q_1&=\sum_i p_i|\beta_i|^2,\\ \omega_0&=q_0^{-1}\sum_i p_i|\alpha_i|^2|i\rangle\langle i|,& \omega_1&=q_1^{-1}\sum_i p_i|\beta_i|^2|1-i\rangle\langle1-i|. \end{aligned}

At a zero-probability outcome, choose $\omega_j=|0\rangle\langle0|$ ; its weighted contribution vanishes. Define $\chi'=S(\sum_jq_j\omega_j)-\sum_jq_jS(\omega_j)$ , $a=H(q)-\chi'$ , and $b=1+S(\rho_B)-S(\rho)$ , with all entropies in bits and $H(q)$ the classical label entropy. Then

\left(R_A,R_B\right)=\left(\frac{a}{a+b},\ S(\rho_B)\right) \quad\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.

The denominator satisfies $a+b\ge1$ for this family, so no additional nonzero-denominator hypothesis is needed. This hybrid coding rate is restricted to the displayed family and does not assert the false universal local-unitary normal form printed immediately before it.

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.12–14, Section V.B, (37): the displayed-family hybrid rate is achievable
with Bob at S(E_B). The false universal normal-form claim is not a hypothesis.
No free classical side channel is supplied. -/
theorem hybrid_ratePair (p : Bool → ℝ) (hp : ∀ i, 0 ≤ p i)
    (htotal : ∑ i, p i = 1) (alpha beta : Bool → ℂ)
    (hcoeff : ∀ i, Complex.normSq (alpha i) + Complex.normSq (beta i) = 1) :
    FiniteAchievable p (hybridVector alpha beta) (hybridRateA p alpha beta)
      (vnEntropy (traceLeft (sourceMean p (hybridVector alpha beta)))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P11

end

Source

On the distributed compression of quantum information, arXiv:quant-ph/0403042v3, PDF p. 13, Section V.B (37): hybrid achievable rate for the displayed family

Read-back

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

Let $p:\{\mathrm{false},\mathrm{true}\}\to\mathbb R$ satisfy $p_i\ge0$ for each Boolean $i$ and $\sum_i p_i=1$ , and let arbitrary complex coefficient functions $\alpha,\beta$ satisfy $|\alpha_i|^2+|\beta_i|^2=1$ for each $i$ . Define $v_i=\alpha_i|\mathrm{false},i\rangle+\beta_i|\mathrm{true},\neg i\rangle$ and $\rho=\sum_i p_i|v_i\rangle\langle v_i|$ , with kets the coordinate vectors. Set $w_{ji}=p_i|\alpha_i|^2$ for $j=\mathrm{false}$ and $w_{ji}=p_i|\beta_i|^2$ for $j=\mathrm{true}$ , let $q_j=\sum_iw_{ji}$ , and define $C_j=|\mathrm{false}\rangle\langle\mathrm{false}|$ if $q_j=0$ and $C_j=q_j^{-1}\sum_iw_{ji}|j\mathbin{\oplus}i\rangle\langle j\mathbin{\oplus}i|$ otherwise. Write

\begin{gathered} S(X)=-\operatorname{Re}\operatorname{Tr}[\operatorname{cfc}(t\mapsto t\log_2t)(X)], \quad H(q)=-\sum_jq_j\log_2q_j,\quad \chi=S\!\left(\sum_jq_jC_j\right)-\sum_jq_jS(C_j),\\ B=1+S(\rho_B)-S(\rho),\qquad R_A=\frac{H(q)-\chi}{H(q)-\chi+B},\qquad R_B=S(\rho_B), \quad (\rho_B)_{b,b'}=\sum_a\rho_{(a,b),(a,b')}. \end{gathered}

Here continuous functional calculus defines $S$ , logarithms use $\ln0=0$ , and a zero denominator in $R_A$ gives $R_A=0$ . The theorem asserts that for every real $\delta>0$ and $\varepsilon>0$ , there is $N\in\mathbb N$ such that for every integer $n>N$ , there exist positive integers $d_A,d_B$ , separate encoding channels $\mathcal E_A,\mathcal E_B$ from $n$ Boolean coordinates to dimensions $d_A,d_B$ , and a decoding channel $\mathcal D$ back to the joint space, such that

\frac{\log_2d_A}{n}\le R_A+\delta,\qquad \frac{\log_2d_B}{n}\le R_B+\delta,\qquad \sum_{w\in\{\mathrm{false},\mathrm{true}\}^n} \left(\prod_{t=0}^{n-1}p_{w_t}\right) \operatorname{Re}\operatorname{Tr}\!\left[ P_w\,\mathcal D\bigl((\mathcal E_A\otimes\mathcal E_B)(P_w)\bigr) \right]\ge1-\varepsilon,

where $P_w=|V_w\rangle\langle V_w|$ and $V_w(x,y)=\prod_{t=0}^{n-1}v_{w_t}(x_t,y_t)$ . Each channel is required to have a finite Kraus representation $X\mapsto\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ . The hypotheses allow zero label probabilities and zero individual coefficients.

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