Isotropic entanglement is the scalar convex envelope

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.convex_envelope_reduction

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

prove2quantum

Let $d\ge2$ and $D=[1/d,1]$ . Define $q_d(x)$ as the minimum of $2(1-\sum_k\mu_k^2)$ over probabilities $\mu_k\ge0$ , $\sum_k\mu_k=1$ , satisfying $\sum_k\sqrt{\mu_k}=\sqrt{dx}$ , and set $c_d=\sqrt{q_d}$ . For $g=q_d$ or $c_d$ define

H_g(F)=\min\left\{\sum_jp_jg(x_j):\ p_j\ge0,\ \sum_jp_j=1,\ x_j\in D,\ \sum_jp_jx_j=F\right\}.

Each minimum is over all finite ensembles and is attained. The function $H_g$ is the greatest convex function on $D$ bounded above by $g$ . For the explicit isotropic density $\rho_{d,F}=FP_d+(1-F)(I-P_d)/(d^2-1)$ , where $P_d=|\Phi_d\rangle\langle\Phi_d|$ ,

\tau(\rho_{d,F})=H_{q_d}(F),\qquad C(\rho_{d,F})=H_{c_d}(F)\quad(F\in D).

For each cost there is a normalized finite pure ensemble with average cost equal to this value whose density twirls to $\rho_{d,F}$ . The twirl integrates conjugation by $U\otimes\overline U$ against probability Haar measure. For $0\le F\le1/d$ , both roofs vanish.

This is the complete reduction from isotropic mixed states to one scalar profile and its convex envelope.

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.7, (3.14)--(3.17): isotropic roofs equal the full scalar convex
envelopes; scalar ensemble minima attain. Below separability both roofs vanish.
The input state is the explicit isotropicDensityAtFidelity matrix, not a hypothesized twirl. -/
theorem convex_envelope_reduction (d : ℕ) (hd : 2 ≤ d) :
    IsConvexEnvelope (Set.Icc (1 / (d : ℝ)) 1) (constrainedSchmidtTangle d) (scalarConvexRoofAtFidelity d (constrainedSchmidtTangle d)) ∧
    IsConvexEnvelope (Set.Icc (1 / (d : ℝ)) 1) (rawC d) (scalarConvexRoofAtFidelity d (rawC d)) ∧
    (∀ F ∈ Set.Icc (1 / (d : ℝ)) 1,
      tangle (isotropicDensityAtFidelity d F) = scalarConvexRoofAtFidelity d (constrainedSchmidtTangle d) F ∧
      concurrence (isotropicDensityAtFidelity d F) = scalarConvexRoofAtFidelity d (rawC d) F ∧
      IsLeast (hullValues d (constrainedSchmidtTangle d) F) (scalarConvexRoofAtFidelity d (constrainedSchmidtTangle d) F) ∧
      IsLeast (hullValues d (rawC d) F) (scalarConvexRoofAtFidelity d (rawC d) F) ∧
      (∃ e : PureEnsemble (Fin d × Fin d),
        (∑ k, e.weight k * pureTangle (e.vector k)) = scalarConvexRoofAtFidelity d (constrainedSchmidtTangle d) F ∧
        Bridge50.P37.bipartiteHaarTwirl d true (ensembleDensity e.weight e.vector) = isotropicDensityAtFidelity d F) ∧
      (∃ e : PureEnsemble (Fin d × Fin d),
        (∑ k, e.weight k * pureConcurrence (e.vector k)) = scalarConvexRoofAtFidelity d (rawC d) F ∧
        Bridge50.P37.bipartiteHaarTwirl d true (ensembleDensity e.weight e.vector) = isotropicDensityAtFidelity d F)) ∧
    (∀ F ∈ Set.Icc (0 : ℝ) (1 / (d : ℝ)),
      tangle (isotropicDensityAtFidelity d F) = 0 ∧ concurrence (isotropicDensityAtFidelity d F) = 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 7, §3.2, (3.14)–(3.17): isotropic convex-envelope reduction

Read-back

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

For every natural number $d\ge2$ , define $P_d(t)$ as the infimum of $2(1-\sum_i\mu_i^2)$ over vectors $(\mu_i)_{i=0}^{d-1}$ satisfying $\mu_i\ge0$ , $\sum_i\mu_i=1$ , and $\sum_i\sqrt{\mu_i}=\sqrt{dt}$ , and put $r_d(t)=\sqrt{P_d(t)}$ . For a real function $f$ , let $V_{d,f}(F)$ consist of all $\sum_kw_kf(t_k)$ from finite mixtures with $w_k\ge0$ , $\sum_kw_k=1$ , $t_k\in[1/d,1]$ , and $\sum_kw_kt_k=F$ , and set $H_df(F)=\inf V_{d,f}(F)$ . The functions $H_dP_d$ and $H_dr_d$ are respectively convex on $[1/d,1]$ , lie below $P_d$ and $r_d$ there, and dominate every other convex function on that interval that lies below the corresponding function. To state the remaining assertions, set $\Phi_d=|\Omega_d\rangle\langle\Omega_d|$ , where $\Omega_d=d^{-1/2}\sum_i|i,i\rangle$ , and

\rho_{d,F}=F\Phi_d+\frac{1-F}{d^2-1}(I-\Phi_d).

For a unit vector $\psi$ , let $(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)}$ ; let $T(\sigma)$ and $C(\sigma)$ be the infima of the average costs $\tau$ and $c$ , respectively, over finite ensembles of unit vectors with nonnegative weights summing to $1$ and average matrix $\sigma$ , where $|\psi\rangle\langle\psi|$ has entries $\psi(u)\overline{\psi(v)}$ . For every $F\in[1/d,1]$ , including both endpoints, $T(\rho_{d,F})=H_dP_d(F)$ and $C(\rho_{d,F})=H_dr_d(F)$ , and each scalar infimum is attained and is least in its corresponding set $V_{d,f}(F)$ . There also exists a finite ensemble with average $\tau$ -cost $H_dP_d(F)$ whose average matrix $\sigma$ satisfies $\int(U\otimes\overline U)\sigma(U\otimes\overline U)^\dagger\,dU=\rho_{d,F}$ , and there exists, separately, such an ensemble with average $c$ -cost $H_dr_d(F)$ ; here $dU$ is normalized Haar measure on the unitary group and the integral is taken entry by entry. Finally, for every $F\in[0,1/d]$ , $T(\rho_{d,F})=C(\rho_{d,F})=0$ . Ensemble weights may be zero, but normalization excludes an empty ensemble.

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