PPT support-overlap weak duality with one-sided constraints

Open

QAlgorithms.Papers.Independent.Intakethird100.P90.ppt_support_weak_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, $P$ its support projection, and $\Gamma$ the normalized PPT states. Define the two optimization values independently. Then

\max_{\sigma\in\Gamma}\operatorname{Tr}(P\sigma)\le\min\{t:\exists Y=Y^\dagger,\ P^{T_B}\le Y,\ Y^{T_B}\le tI\}.

The maximum and minimum are attained. The dual has only the displayed one-sided inequalities. The result asserts weak duality and does not identify the values by an additional equality.

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.7, Eq.(16): weak duality with exactly the
two ONE-SIDED constraints. The source's maximum and minimum are attained;
no equality of these independently defined values is claimed here. -/
theorem ppt_support_weak_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) :
    supportOverlap rho ≤ supportDual rho ∧
    (∃ sigma : Matrix (A × B) (A × B) ℂ, IsPPT sigma ∧
      (supportProjection rho * sigma).trace.re = supportOverlap rho) ∧
    (∃ Y, supportDualFeasible rho (supportDual rho) Y) := 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. 7, Supplemental unnumbered result, Eq.(16): PPT-support overlap weak duality

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$ with $\rho\succeq0$ and $\operatorname{Tr}\rho=1$ , write $(\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. Define

s(\rho)=\sup_{\substack{\sigma\succeq0,\ \operatorname{Tr}\sigma=1\\ \Gamma\sigma\succeq0}} \operatorname{Re}\operatorname{Tr}(P_\rho\sigma), \qquad d(\rho)=\inf\left\{t\in\mathbb R: \begin{array}{l} \exists\,Y=Y^\dagger,\quad Y-\Gamma P_\rho\succeq0,\\ tI-\Gamma Y\succeq0 \end{array}\right\}.

Then $s(\rho)\le d(\rho)$ ; there exists a matrix $\sigma$ satisfying $\sigma\succeq0$ , $\operatorname{Tr}\sigma=1$ , and $\Gamma\sigma\succeq0$ for which $\operatorname{Re}\operatorname{Tr}(P_\rho\sigma)=s(\rho)$ ; and there exists a Hermitian $Y$ with $Y-\Gamma P_\rho\succeq0$ and $d(\rho)I-\Gamma Y\succeq0$ . The infimum ranges over all real $t$ , with no separate sign restriction.

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