The additive support bound lower-bounds PPT relative entropy and cost

Open

QAlgorithms.Papers.Independent.Intakethird100.P90.eta_lower_bound

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 any bipartite state, and let $P$ be its support projection. Define

\eta(\rho)=\min_{Y=Y^\dagger,\,-Y\le P^{T_B}\le Y}\|Y^{T_B}\|_\infty,\qquad E_\eta(\rho)=-\log_2\eta(\rho).

Let $E_R(\rho)=\inf_{\sigma\in\Gamma}S(\rho\Vert\sigma)$ , where $\Gamma$ is the set of normalized PPT states, and $E_R^\infty(\rho)=\inf_{n\ge1}E_R(\rho^{\otimes n})/n$ . Relative entropy is $+\infty$ when support inclusion fails. Then

E_R^\infty(\rho)\ge E_\eta(\rho),\qquad E_{C,\mathrm{LOCC}}(\rho)\ge E_C(\rho)\ge E_\eta(\rho).

This provides a support-dependent lower bound for both operational formation costs, including singular states.

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.3, Proposition 1, including the complete cost consequence. -/
theorem eta_lower_bound {A B : Type} [Fintype A] [Fintype B]
    [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B]
    (rho : Matrix (A × B) (A × B) ℂ) (hstate : IsDensityMatrix rho) :
    (etaEntanglement rho : EReal) ≤ regularizedPptRelativeEntropy rho ∧
    asymptoticEntanglementCost false rho ≤ asymptoticEntanglementCost true rho ∧
    (etaEntanglement rho : EReal) ≤ asymptoticEntanglementCost false 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. 3, Proposition 1: additive support bound below regularized PPT relative entropy and cost

Read-back

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

For arbitrary finite, nonempty types $A,B$ , each equipped with decidable equality, and every complex matrix $\rho$ indexed by $A\times B$ satisfying $\rho\ge0$ and $\operatorname{Tr}\rho=1$ , the assertion is

\eta(\rho)\le E_{\mathrm{PPT}}^\infty(\rho),\qquad C_{\mathrm{PPT}}(\rho)\le C_{\mathrm{LOCC}}(\rho),\qquad \eta(\rho)\le C_{\mathrm{PPT}}(\rho),

where the real number $\eta(\rho)$ is embedded in the extended real line for these comparisons. To define it, let $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , let $P_\rho$ be the spectral functional calculus of $\rho$ for the function equal to $0$ at $0$ and $1$ elsewhere, and let $\|\cdot\|_{\rm op}$ denote the Euclidean operator norm. Then

\eta(\rho)=-\log_2\inf_{\substack{Y=Y^\dagger\\Y-\Gamma P_\rho\ge0\\Y+\Gamma P_\rho\ge0}}\|\Gamma Y\|_{\rm op}.

The logarithm here is the total real logarithm, with $\log_2 0=0$ . Define

D_2(X\|S)= \begin{cases} \displaystyle\frac{\operatorname{Re}\operatorname{Tr}(X\log X-X\log S)}{\log2}, &\ker S\subseteq\ker X,\\ +\infty,&\text{otherwise}, \end{cases} \qquad E_{\mathrm{PPT}}^\infty(\rho)= \inf_{n\ge1}\frac1n \inf_{\substack{S\ge0,\ \operatorname{Tr}S=1\\\Gamma S\ge0}}D_2(\rho^{\otimes n}\|S),

using spectral functional calculus for matrix logarithms, including the scalar convention $\log0=0$ , and grouped tensor powers with entries given by products of the corresponding entries of $\rho$ . For either operation class $\mathcal C$ , $C_{\mathcal C}(\rho)$ is the extended-real infimum of real $r\ge0$ such that, for every $\varepsilon,\delta>0$ , every sufficiently large positive natural $n$ admits $m\in\mathbb N$ and $\Lambda\in\mathcal C$ with $m\le n(r+\delta)$ and $\|\Lambda(\Phi_{2^m})-\widehat{\rho^{\otimes n}}\|_1\le\varepsilon$ . Here $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ , the hat denotes the fixed relabelling of each party’s basis by a finite initial segment, and $\Phi_k$ has entry $1/k$ when both its row and column have equal party indices, and $0$ otherwise. Channels are finite Kraus sums with $\sum_jK_j^\dagger K_j=I$ ; PPT channels are those whose input-output partial-transpose conjugates are also channels. The LOCC class consists of maps generated by the identity and finite recursive trees of local Kraus instruments on either party, with a subsequent map chosen for each outcome and all branches summed. The resource count $m=0$ and one-dimensional party types are included.

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