Both Rains bounds lie below asymptotic PPT relative entropy

Open

QAlgorithms.Papers.Independent.Intakethird100.P90.rank_two_rains_gap

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 rank-two state supported on the two-qutrit antisymmetric subspace. Let $R(\rho)=\inf\{S(\rho\Vert\sigma):\sigma\ge0,\ \|\sigma^{T_B}\|_1\le1\}$ , $R^\infty(\rho)=\inf_{n\ge1}R(\rho^{\otimes n})/n$ , and let $E_R^\infty$ be the corresponding regularization of relative entropy to normalized PPT states. Then

R(\rho)<E_R^\infty(\rho),\qquad R^\infty(\rho)<E_R^\infty(\rho).

The abstract's byproduct concerns both the single-copy bound and its regularization throughout the rank-two class.

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 pp.1--2,4--5,7: the abstract includes both
single-copy and regularized Rains quantities for every rank-two state in the class. -/
theorem rank_two_rains_gap
    (rho : Matrix (Fin 3 × Fin 3) (Fin 3 × Fin 3) ℂ)
    (hstate : IsDensityMatrix rho) (hrank : stateRank rho = 2)
    (hsupport : antisymmetricSupported rho) :
    rains rho < regularizedPptRelativeEntropy rho ∧
    regularizedRains rho < regularizedPptRelativeEntropy 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. 1, Abstract byproduct: both Rains quantities lie strictly below asymptotic PPT relative entropy

Read-back

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

For every complex matrix $\rho$ indexed by $\{0,1,2\}\times\{0,1,2\}$ , assume that $\rho\ge0$ , $\operatorname{Tr}\rho=1$ , the complex dimension of its column space is exactly $2$ , and $\rho_{(b,a),v}=-\rho_{(a,b),v}$ for every $a,b\in\{0,1,2\}$ and every column index $v$ . Then

R(\rho)<E_{\mathrm{PPT}}^\infty(\rho), \qquad R^\infty(\rho)<E_{\mathrm{PPT}}^\infty(\rho)

in the extended real line. These quantities mean

R(X)=\inf_{\substack{S\ge0\\\|\Gamma S\|_1\le1}}D_2(X\|S),\qquad R^\infty(\rho)=\inf_{n\ge1}\frac{R(\rho^{\otimes n})}{n},\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).

Here $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ , and $D_2(X\|S)=\operatorname{Re}\operatorname{Tr}(X\log X-X\log S)/\log2$ if $\ker S\subseteq\ker X$ , and $+\infty$ otherwise. Matrix logarithms use spectral functional calculus with $\log0=0$ , and grouped tensor powers have entries equal to products of the corresponding single-copy entries. The alternatives $S$ in $R$ have no trace-one requirement.

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