Closest separable states need not be unique

Open

QAlgorithms.Papers.Independent.Intakethird100.P100.separable_minimizers_need_not_be_unique

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

prove2quantum

There exist positive finite local dimensions and a bipartite density matrix $\sigma$ having two distinct separable minimizers $\rho_1,\rho_2$ . Here separable means a finite convex combination of product density matrices, and $E_r$ is the infimum of support-aware Umegaki relative entropy in natural logarithms over exactly those normalized states. More precisely,

\rho_1\neq\rho_2,\qquad E_r(\sigma)<\infty,\qquad S(\sigma\Vert\rho_1)=S(\sigma\Vert\rho_2)=E_r(\sigma).

This shows why a closest separable state cannot in general be treated as a uniquely defined state.

Formalization Note The accepted infimum and its attaining comparisons are stored in bits. Multiplication by the positive constant $\log 2$ gives the natural-logarithm values and preserves finiteness and every minimizing equality.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P100

Formal statement

noncomputable section

open Filter

open scoped ENNReal Topology ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P100

open QAlgorithms.Papers.Independent.Dependency50.P15
  (relativeDistance relativeDistanceValue positiveOperatorRelativeEntropyBits groupedTensorPower)

open QAlgorithms.Papers.Independent.Information100.P54
  (relativeEntropyBits relativeEntanglement)

/-- Final discussion, PDF p.3: some bipartite state has two distinct closest
separable states. The positive finite local dimensions are existential, with
no unsupported assertion that this occurs for every state or every dimension. -/
theorem separable_minimizers_need_not_be_unique :
    ∃ a b : ℕ,
      ∃ sigma rhoOne rhoTwo :
        Matrix (Fin (a + 1) × Fin (b + 1)) (Fin (a + 1) × Fin (b + 1)) ℂ,
      IsDensityMatrix sigma ∧
      rhoOne ∈ separableStates ∧ rhoTwo ∈ separableStates ∧ rhoOne ≠ rhoTwo ∧
      relativeEntanglement sigma < ⊤ ∧
      relativeEntropyBits sigma rhoOne = relativeEntanglement sigma ∧
      relativeEntropyBits sigma rhoTwo = relativeEntanglement sigma := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P100

end

Source

Continuity of Relative Entropy of Entanglement, arXiv:quant-ph/9910002v1, PDF p. 3, Final discussion before the Corollary

Read-back

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

There exist natural numbers $a,b$ and complex matrices $\sigma,\rho_1,\rho_2$ on $\{0,\ldots,a\}\times\{0,\ldots,b\}$ such that $\sigma$ is positive semidefinite with trace $1$ , $\rho_1\ne\rho_2$ , both $\rho_1,\rho_2$ are finite mixtures of product density matrices, and

E_{\mathrm{sep}}(\sigma)<+\infty,\qquad R(\sigma\Vert\rho_1)=E_{\mathrm{sep}}(\sigma),\qquad R(\sigma\Vert\rho_2)=E_{\mathrm{sep}}(\sigma).

A finite mixture of product density matrices means a sum $\sum_{j<q}w_j(R_j\otimes S_j)$ , with $q\in\mathbb N$ , $w_j\ge0$ , $\sum_jw_j=1$ , and local matrices $R_j,S_j$ positive semidefinite with trace $1$ . The quantity $E_{\mathrm{sep}}(X)$ is the extended-nonnegative-real infimum of $R(X\Vert Y)$ over all such mixtures $Y$ . For density matrices $X,Y$ , $R(X\Vert Y)$ equals $\max\{\operatorname{Re}\operatorname{tr}(f(X)-X\log Y),0\}/\ln2$ when $\ker Y\subseteq\ker X$ , and $+\infty$ otherwise; it is also $+\infty$ outside density matrices. Here $f(x)=x\ln x$ , with matrix functions defined by functional calculus and $\ln0=0$ . The quantified $a,b$ may be zero, so the stated dimensions $a+1,b+1$ are required only to be positive.

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