Deterministic entanglement depends only on support

Open

QAlgorithms.Papers.Independent.Intakethird100.P83.deterministicSupportInvariance

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

prove2quantum

Let $\rho,\sigma$ be normalized states on the same arbitrary finite nonzero bipartite spaces with $\operatorname{supp}\rho=\operatorname{supp}\sigma$ . Let $E_1$ be the one-copy exact positive-real-target PPT rate, and let $E_{\Gamma,0}(\rho)=\sup_{n\ge1}E_1(\rho^{\otimes n})/n$ . Then

E_1(\rho)=E_1(\sigma),\qquad E_{\Gamma,0}(\rho)=E_{\Gamma,0}(\sigma).

Equal supports persist under tensor powers. The invariance applies to these exact deterministic quantities; no full-support assumption is imposed.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P83

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P83

open QAlgorithms.Papers.Independent.Support50.P11 (Loewner)

open QAlgorithms.Papers.Independent.Dependency50.P32 (partialTranspose)

open QAlgorithms.Papers.Independent.Information100.P34 (supportProjector)

variable {A B C D : Type*}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

/-- Support dependence announced on PDF p.4 and established by (15) on p.5.
Both one-copy and regularized deterministic values are invariant; no full-rank
assumption and no invariance of E_Gamma or E_W is asserted. -/
theorem deterministicSupportInvariance [Nonempty A] [Nonempty B]
    (rho sigma : Matrix (A × B) (A × B) ℂ)
    (hrho : IsDensityMatrix rho) (hsigma : IsDensityMatrix sigma)
    (hsupport : supportSpace rho = supportSpace sigma) :
    oneCopyExact rho = oneCopyExact sigma ∧ exactRegularized rho = exactRegularized sigma := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P83

end

Source

Improved Semidefinite Programming Upper Bound on Distillable Entanglement, arXiv:1601.07940v4, PDF p. 4, Unnumbered main result: deterministic entanglement depends only on support

Read-back

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

For any finite nonempty types $A,B$ , each with decidable equality, let $\rho,\sigma$ be complex matrices indexed by $A\times B$ , both positive semidefinite with trace $1$ , and suppose their ranges as linear maps on complex coordinate functions are equal. For any bipartite matrix $X$ , put $X^\Gamma_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , and define $F_X(k)$ as the real supremum of $\operatorname{Re}\operatorname{tr}(XQ)$ over $Q$ with $k>0$ , $0\preceq Q\preceq I$ , and $-k^{-1}I\preceq Q^\Gamma\preceq k^{-1}I$ , where $\preceq$ denotes positive semidefinite difference. Set $D(X)=\sup\{\log_2 k:k\in\mathbb R,\ k>0,\ F_X(k)=1\}$ , and set

D_{\mathrm{reg}}(X)=\sup_{m\ge1}\frac{D(X^{\otimes m})}{m}, \qquad (X^{\otimes m})_{(a,b),(a',b')}=\prod_{i=0}^{m-1}X_{(a_i,b_i),(a'_i,b'_i)}.

These are real-valued suprema, and the regularization uses only positive tensor powers. Then $D(\rho)=D(\sigma)$ and $D_{\mathrm{reg}}(\rho)=D_{\mathrm{reg}}(\sigma)$ .

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