Hidden orthogonality permits a smaller sum rate

Open

QAlgorithms.Papers.Independent.Intakethird100.P11.hiddenOrthogonality

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

prove2quantum

For $0<\alpha,\beta<1$ , take three equiprobable product letters $|\phi_i\rangle_A|\psi_i\rangle_B$ in $\mathbb C^2\otimes\mathbb C^3$ , where

\begin{aligned} \phi_1&=|0\rangle,&\phi_2&=\sqrt\alpha|0\rangle+\sqrt{1-\alpha}|1\rangle,&\phi_3&=|1\rangle,\\ \psi_1&=\sqrt{1-\beta}|0\rangle+\sqrt\beta|1\rangle,&\psi_2&=|1\rangle,& \psi_3&=\sqrt{1-\beta}|2\rangle+\sqrt\beta|0\rangle. \end{aligned}

Let $\mathcal E_{AB}$ be this source and $\mathcal E_A,\mathcal E_B$ its marginals. Set $\psi'_1=\psi_1$ , $\psi'_2=\psi_2$ , $\psi'_3=|0\rangle$ , and let $\mathcal E'_B$ be the corresponding equiprobable ensemble. Define the exact rates $r_A(\alpha)=S(\mathcal E_A)$ , $r_B(\beta)=S(\mathcal E'_B)$ and the comparison expression $L(\alpha,\beta)=[S(\mathcal E_A)+S(\mathcal E_B)+S(\mathcal E_{AB})]/2$ . Both local ensembles are irreducible, the joint ensemble is reducible, and $(r_A(\alpha),r_B(\beta))$ is achievable. Moreover, with $h=H_2(2/3)$ denoting binary entropy in bits,

\begin{aligned} (r_A(\alpha),r_B(\beta))&\longrightarrow(h,h),\\ r_A(\alpha)+r_B(\beta)&\longrightarrow 2h,\\ L(\alpha,\beta)&\longrightarrow h/2+\log_23 \end{aligned} \qquad\text{as }(\alpha,\beta)\to(0,0)\text{ through positive values}.

There is $\eta\in(0,1)$ such that $0<\alpha,\beta<\eta$ implies $r_A(\alpha)+r_B(\beta)<L(\alpha,\beta)$ .

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 example shows why the converse needs global irreducibility. Its approximate numbers describe limits, not exact finite-parameter rates.

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.11, Section V.A, (23)–(30): local irreducibility does not imply the
rate-sum converse. Approximation is stated as positive-parameter limits and a
uniform sufficiently-small threshold, never as equality at positive parameters. -/
theorem hiddenOrthogonality :
    (∀ alpha beta : ℝ, 0 < alpha → alpha < 1 → 0 < beta → beta < 1 →
      EnsembleIrreducible (fun _ : Fin 3 => (1 / 3 : ℝ)) (hiddenAlice alpha) ∧
      EnsembleIrreducible (fun _ : Fin 3 => (1 / 3 : ℝ)) (hiddenBob beta) ∧
      ¬ EnsembleIrreducible (fun _ : Fin 3 => (1 / 3 : ℝ)) (hiddenJoint alpha beta) ∧
      FiniteAchievable (fun _ : Fin 3 => (1 / 3 : ℝ)) (hiddenJoint alpha beta)
        (hiddenRateA alpha) (hiddenRateB beta)) ∧
    Tendsto (fun x : ℝ × ℝ => (hiddenRateA x.1, hiddenRateB x.2))
      (nhdsWithin (0, 0) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ)))
      (nhds (binEntropy2 (2 / 3), binEntropy2 (2 / 3))) ∧
    Tendsto (fun x : ℝ × ℝ => hiddenRateA x.1 + hiddenRateB x.2)
      (nhdsWithin (0, 0) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ)))
      (nhds (2 * binEntropy2 (2 / 3))) ∧
    Tendsto (fun x : ℝ × ℝ => hiddenComparison x.1 x.2)
      (nhdsWithin (0, 0) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ)))
      (nhds (binEntropy2 (2 / 3) / 2 + Real.logb 2 3)) ∧
    ∃ eta : ℝ, 0 < eta ∧ eta < 1 ∧ ∀ alpha beta : ℝ,
      0 < alpha → alpha < eta → 0 < beta → beta < eta →
      hiddenRateA alpha + hiddenRateB beta < hiddenComparison 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. 11, Section V.A: hidden orthogonality beats the global-irreducibility bound

Read-back

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

Write $|j\rangle$ for the coordinate vector with entry $1$ at $j$ and $0$ elsewhere, and write $|v\rangle\langle v|$ for the matrix with entries $v_a\overline{v_b}$ . For a matrix $X$ , put $S(X)=-\operatorname{Re}\operatorname{Tr}(f(X))$ , where $f(t)=t\log_2t$ is applied by continuous functional calculus. Define the three families

\begin{aligned} a_\alpha&=\bigl(|0\rangle,\ \sqrt{\alpha}|0\rangle+\sqrt{1-\alpha}|1\rangle,\ |1\rangle\bigr),\\ b_\beta&=\bigl(\sqrt{1-\beta}|0\rangle+\sqrt{\beta}|1\rangle,\ |1\rangle,\ \sqrt{1-\beta}|2\rangle+\sqrt{\beta}|0\rangle\bigr),\\ \widetilde b_\beta&=\bigl(\sqrt{1-\beta}|0\rangle+\sqrt{\beta}|1\rangle,\ |1\rangle,\ |0\rangle\bigr), \qquad v_{\alpha,\beta,i}=a_{\alpha,i}\otimes b_{\beta,i}. \end{aligned}

Let $\rho_A=\frac13\sum_{i=0}^2|a_{\alpha,i}\rangle\langle a_{\alpha,i}|$ , $\rho_B=\frac13\sum_{i=0}^2|b_{\beta,i}\rangle\langle b_{\beta,i}|$ , $\widetilde\rho_B=\frac13\sum_{i=0}^2|\widetilde b_{\beta,i}\rangle\langle\widetilde b_{\beta,i}|$ , and $\rho_{AB}=\frac13\sum_{i=0}^2|v_{\alpha,\beta,i}\rangle\langle v_{\alpha,\beta,i}|$ , and set $R_A(\alpha)=S(\rho_A)$ , $R_B(\beta)=S(\widetilde\rho_B)$ , and $C(\alpha,\beta)=\bigl(S(\rho_A)+S(\rho_B)+S(\rho_{AB})\bigr)/2$ . The theorem asserts that, for every pair of real numbers $0<\alpha<1$ and $0<\beta<1$ , each of the families $a_\alpha$ and $b_\beta$ , with all three labels having probability $1/3$ , has the following property: every nonempty proper subset of labels has a pair of vectors on opposite sides with nonzero inner product; the joint family $v_{\alpha,\beta}$ does not have this property. It also asserts the following achievability at rates $(R_A(\alpha),R_B(\beta))$ : for every $\delta>0$ and $\varepsilon>0$ , there is $N\in\mathbb N$ such that every integer $n>N$ admits positive integers $d_A,d_B$ , separate encoding channels from the $n$ copies of Alice’s and Bob’s spaces into dimensions $d_A,d_B$ , and a decoding channel back to their joint $n$ -copy space, satisfying

\frac{\log_2d_A}{n}\le R_A(\alpha)+\delta,\qquad \frac{\log_2d_B}{n}\le R_B(\beta)+\delta,\qquad 3^{-n}\sum_{w\in\{0,1,2\}^n} \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_{\alpha,\beta,w_t}(x_t,y_t)$ . Here every channel means a map of the form $X\mapsto\sum_jK_jXK_j^\dagger$ for a finite family of matrices satisfying $\sum_jK_j^\dagger K_j=I$ . Furthermore, as $(\alpha,\beta)\to(0,0)$ through the strictly positive quadrant,

\begin{aligned} (R_A(\alpha),R_B(\beta))&\longrightarrow(h_2(2/3),h_2(2/3)),\\ R_A(\alpha)+R_B(\beta)&\longrightarrow2h_2(2/3),\\ C(\alpha,\beta)&\longrightarrow\tfrac12h_2(2/3)+\log_2 3, \end{aligned}

where $h_2(u)=[-u\ln u-(1-u)\ln(1-u)]/\ln2$ . Finally, there exists a real $0<\eta<1$ such that $R_A(\alpha)+R_B(\beta)<C(\alpha,\beta)$ whenever $0<\alpha<\eta$ and $0<\beta<\eta$ .

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