Structure and weights of attaining isotropic decompositions

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.optimal_ensembles

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

prove2quantum

Let $d\ge3$ , $F\in[0,1]$ , $a=4(d-1)/d^2$ , $t=2(2d-3)/(d(d-1))$ , and $M=2(d-1)/d$ . For the isotropic density $\rho_{d,F}$ , an attaining finite normalized tangle ensemble exists whose positive-weight pure states all have tangle $\tau(\rho_{d,F})$ when $F\le a$ , and have tangles in $\{t,M\}$ when $F>a$ . In the latter case the total weights of these two tangle classes are respectively

w_t=\frac{1-F}{1-a},\qquad w_M=\frac{F-a}{1-a}.

There is also an attaining concurrence ensemble using only normalized product states or maximally entangled states at positive weights. Its total maximally entangled weight is

w_{\max}=\begin{cases}0&F\le1/d,\\(dF-1)/(d-1)&F>1/d.\end{cases}

Zero-weight members impose no type restriction. At $F=1$ only maximal entanglement need have positive weight; below the separability threshold common tangle is zero.

These are existence statements about constructed optimizers, rather than claims about every optimal ensemble.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P21

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P21

open scoped Matrix ComplexConjugate

open Filter

open QAlgorithms

open QAlgorithms.Papers.Independent.Information100.P03
  (PureEnsemble convexRoof pureConcurrence concurrence SchmidtData schmidtVector)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.13: existence of attaining isotropic decompositions with common
tangle below the breakpoint, two allowed tangle values above, and product/maximal
concurrence components. No universal classification of optimal ensembles is claimed. -/
theorem optimal_ensembles (d : ℕ) (hd : 3 ≤ d) (F : ℝ) (hF : F ∈ Set.Icc (0 : ℝ) 1) :
    (∃ e : PureEnsemble (Fin d × Fin d), IsOptimalPureEnsemble pureTangle (isotropicDensityAtFidelity d F) e ∧
      (∀ k, 0 < e.weight k →
        if F ≤ tangentPoint d then pureTangle (e.vector k) = tangle (isotropicDensityAtFidelity d F)
        else pureTangle (e.vector k) = 2*(2*(d : ℝ)-3)/((d : ℝ)*((d : ℝ)-1)) ∨
          pureTangle (e.vector k) = 2*((d : ℝ)-1)/d) ∧
      (tangentPoint d < F →
        (∑ k, if pureTangle (e.vector k) = 2*(2*(d : ℝ)-3)/((d : ℝ)*((d : ℝ)-1))
          then e.weight k else 0) = (1-F)/(1-tangentPoint d) ∧
        (∑ k, if pureTangle (e.vector k) = 2*((d : ℝ)-1)/d then e.weight k else 0) =
          (F-tangentPoint d)/(1-tangentPoint d))) ∧
    (∃ e : PureEnsemble (Fin d × Fin d), IsOptimalPureEnsemble pureConcurrence (isotropicDensityAtFidelity d F) e ∧
      (∀ k, 0 < e.weight k → IsPureProductState (e.vector k) ∨ IsMaximallyEntangled (e.vector k)) ∧
      (∑ k, if IsMaximallyEntangled (e.vector k) then e.weight k else 0) =
        (if F ≤ 1/(d : ℝ) then 0 else ((d : ℝ)*F-1)/((d : ℝ)-1))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 13, §3.4.3: structure of optimal isotropic decompositions

Read-back

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

For every natural number $d\ge3$ and every real $F\in[0,1]$ , let $\Omega_d=d^{-1/2}\sum_{i=0}^{d-1}|i,i\rangle$ , $\Phi_d=|\Omega_d\rangle\langle\Omega_d|$ , and $\rho_F=F\Phi_d+(1-F)(I-\Phi_d)/(d^2-1)$ . For a unit vector $\psi$ , define $(A_\psi)_{ij}=\sum_b\psi(i,b)\overline{\psi(j,b)}$ , $\tau(\psi)=2(1-\operatorname{Re}\operatorname{tr}(A_\psi^2))$ , and $c(\psi)=\sqrt{\tau(\psi)}$ . Define $T(\sigma)$ and $C(\sigma)$ as the infima of the respective average costs over finite ensembles of unit vectors with nonnegative weights summing to $1$ and average matrix $\sigma$ , where $(|\psi\rangle\langle\psi|)_{uv}=\psi(u)\overline{\psi(v)}$ . Put

t_d=\frac{4(d-1)}{d^2},\qquad u_d=\frac{2(2d-3)}{d(d-1)},\qquad v_d=\frac{2(d-1)}d.

There exists a finite ensemble $(w_k,\psi_k)$ averaging to $\rho_F$ and attaining $T(\rho_F)$ , such that every positive-weight component has $\tau(\psi_k)=T(\rho_F)$ if $F\le t_d$ , and has $\tau(\psi_k)=u_d$ or $\tau(\psi_k)=v_d$ if $F>t_d$ . In the latter case, the sums of the weights over all components with these respective costs are exactly

\sum_{\tau(\psi_k)=u_d}w_k=\frac{1-F}{1-t_d}, \qquad \sum_{\tau(\psi_k)=v_d}w_k=\frac{F-t_d}{1-t_d}.

Separately, there exists a finite ensemble averaging to $\rho_F$ and attaining $C(\rho_F)$ , every positive-weight component of which is either a tensor product of two unit vectors or a vector $d^{-1/2}\sum_{i=0}^{d-1}a_i\otimes b_i$ for orthonormal families $(a_i)$ and $(b_i)$ in $\mathbb C^d$ . The total weight of components having the latter form is $0$ if $F\le1/d$ , and $(dF-1)/(d-1)$ otherwise. Zero weights are allowed; the component restrictions apply only to strictly positive weights, while the displayed weight sums range over all components.

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