Attained independent primal and dual descriptions of eta

Open

QAlgorithms.Papers.Independent.Intakethird100.P90.eta_sdp_duality

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

prove2quantum

All systems are finite-dimensional complex Hilbert spaces with fixed orthonormal product bases and positive local dimensions. A state is a positive semidefinite operator of trace one. All logarithms are base two and all operational rates are measured in standard Bell pairs (ebits) per input copy, with deterministic operations and error tending to zero. Write $E_D,E_C$ for distillable entanglement and entanglement cost under completely PPT-preserving CPTP operations; an explicit LOCC subscript denotes unrestricted two-way local operations and classical communication.

Let $\rho$ be a bipartite state and $P$ its support projection. Define the primal and dual independently by

\eta_p=\inf\{t:\exists Y=Y^\dagger,\ -Y\le P^{T_B}\le Y,\ -tI\le Y^{T_B}\le tI\},

\eta_d=\sup\{\operatorname{Tr}P(V-F)^{T_B}:V,F,W,X\ge0,\ V+F\le(W-X)^{T_B},\ \operatorname{Tr}(W+X)\le1\}.

Both extrema are attained, and

0<\eta(\rho)=\eta_p=\eta_d,\qquad E_\eta(\rho)=-\log_2\eta_p,

where $\eta(\rho)$ is the minimum of $\|Y^{T_B}\|_\infty$ over the support sandwich in Eq. (4). These finite SDPs specify the paper's computable lower bound; no exact real-input bit-complexity claim is added.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P90

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P90

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms

open QAlgorithms.Papers.Independent.Dependency50.P36
  (relativeEntropy rains target canonicalMatrix allowed pptDistillable)

open QAlgorithms.Papers.Independent.Information100.P04 (gamma copies IsPPT)

open QAlgorithms.Papers.Independent.Next46.P42 (regroupProduct)

open QAlgorithms.Papers.Independent.Information100.P06 (supportProjection)

open QAlgorithms.Papers.Independent.Information100.P21 (FiniteLOCC)

open QAlgorithms.Papers.Independent.Gap48.P32 (antisymmetricQutrit)

/-- arXiv:1606.09421v3, PDF p.6, Eqs.(12)--(13): independently defined
primal and dual optima coincide and are attained, and E_eta=-log2 supportEta.
Strict positivity prevents a default logarithm value at zero. -/
theorem eta_sdp_duality {A B : Type} [Fintype A] [Fintype B]
    [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hstate : IsDensityMatrix rho) :
    0 < supportEta rho ∧ etaPrimal rho = supportEta rho ∧ etaDual rho = etaPrimal rho ∧
    (∃ Y, etaPrimalFeasible rho (etaPrimal rho) Y) ∧
    (∃ V F W X : Matrix (A × B) (A × B) ℂ,
      etaDualFeasible V F W X ∧ etaDualObjective rho V F = etaDual rho) ∧
    etaEntanglement rho = -Real.logb 2 (etaPrimal rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P90

end

Source

Irreversibility of Asymptotic Entanglement Manipulation Under Quantum Operations Completely Preserving Positivity of Partial Transpose, arXiv:1606.09421v3, PDF p. 6, Supplemental unnumbered result, Eqs.(12)–(13): attained primal/dual description of eta

Read-back

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

For any nonempty finite types $A,B$ , each equipped with decidable equality, and every complex matrix $\rho$ indexed by $A\times B$ satisfying $\rho\succeq0$ and $\operatorname{Tr}\rho=1$ , define $(\Gamma X)_{(a,b),(c,d)}=X_{(a,d),(c,b)}$ and let $P_\rho$ be the functional-calculus value at $\rho$ of the function that is zero at zero and one elsewhere. Let $\eta(\rho)$ be the infimum of $\|\Gamma Y\|_{\mathrm{op}}$ over Hermitian $Y$ satisfying $Y-\Gamma P_\rho\succeq0$ and $Y+\Gamma P_\rho\succeq0$ . Define the primal value $p_\eta(\rho)$ as the infimum of all real $t$ for which such a $Y$ additionally satisfies $tI-\Gamma Y\succeq0$ and $\Gamma Y+tI\succeq0$ . Define the dual value $d_\eta(\rho)$ as the supremum of $\operatorname{Re}\operatorname{Tr}[P_\rho\Gamma(V-F)]$ over matrices $V,F,W,X$ indexed by $A\times B$ satisfying

V,F,W,X\succeq0,\qquad \Gamma(W-X)-(V+F)\succeq0,\qquad \operatorname{Re}\operatorname{Tr}(W+X)\le1.

Then $\eta(\rho)>0$ , $p_\eta(\rho)=\eta(\rho)$ , and $d_\eta(\rho)=p_\eta(\rho)$ ; there exists a Hermitian $Y$ satisfying all four primal inequalities with $t=p_\eta(\rho)$ , and there exist $V,F,W,X$ satisfying the displayed dual constraints whose objective equals $d_\eta(\rho)$ . Finally, the quantity defined as $E_\eta(\rho)=-\log_2\eta(\rho)$ satisfies $E_\eta(\rho)=-\log_2p_\eta(\rho)$ . No restriction on the real variable $t$ is imposed separately from its matrix inequalities.

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