A corrected explicit matrix witness for irreversibility

Open

QAlgorithms.Papers.Independent.Intakethird100.P90.matrix_irreversibility_criterion

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. Suppose a Hermitian matrix $Y$ satisfies $Y-P^{T_B}\ge0$ , $Y+P^{T_B}\ge0$ , and $\|Y^{T_B}\|_\infty>0$ . If

\|\rho^{T_B}\|_1<\|Y^{T_B}\|_\infty^{-1},

then

E_D(\rho)<E_C(\rho).

Source correction. The printed pair is $P^{T_B}\pm Y\ge0$ ; it is corrected to $Y\pm P^{T_B}\ge0$ , in agreement with Eqs. (4), (12) and the constructed witness on p. 5. The printed pair forces $P^{T_B}\ge0$ . The norm guard is automatic for a feasible normalized-state support and excludes inverse-at-zero defaults.

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.4: corrected matrix-witness criterion.
PRINTED: P^TB plus or minus Y >= 0. CHANGED: Y plus or minus P^TB >= 0. WHY: Eqs.(4),(12)
and the p.5 witness require -Y<=P^TB<=Y; the printed pair instead forces
P^TB>=0. Independent moderation must confirm this recorded source correction.
The positive norm guard is automatic for a feasible normalized-state support. -/
theorem matrix_irreversibility_criterion {A B : Type} [Fintype A] [Fintype B]
    [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B]
    (rho Y : Matrix (A × B) (A × B) ℂ) (hstate : IsDensityMatrix rho)
    (hY : etaFeasible rho Y) (hnorm : 0 < specNorm (gamma Y))
    (hgap : traceNorm (gamma rho) < (specNorm (gamma Y))⁻¹) :
    pptDistillable rho < 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. 4, Unnumbered explicit matrix witness sufficient condition, with recorded source sign correction

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 complex matrices $\rho,Y$ on $A\times B$ , assume that $\rho\ge0$ , $\operatorname{Tr}\rho=1$ , and, on writing $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ and letting $P_\rho$ be the spectral functional calculus of $\rho$ for the function equal to $0$ at $0$ and $1$ elsewhere, that

Y=Y^\dagger,\qquad Y-\Gamma P_\rho\ge0,\qquad Y+\Gamma P_\rho\ge0,\qquad 0<\|\Gamma Y\|_{\rm op},\qquad \|\Gamma\rho\|_1<\frac1{\|\Gamma Y\|_{\rm op}}.

The matrix $Y$ has no trace-one hypothesis. Here $\|\cdot\|_{\rm op}$ is the Euclidean operator norm and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . The conclusion is $D_{\mathrm{PPT}}(\rho)<C_{\mathrm{PPT}}(\rho)$ in the extended real line. A channel means a finite Kraus sum $X\mapsto\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ , and it is PPT when $X\mapsto\Gamma_{\rm out}\Lambda(\Gamma_{\rm in}X)$ is also a channel. Let $\Phi_k$ have entry $1/k$ if its row and column each have equal party indices, and $0$ otherwise. The quantity $D_{\mathrm{PPT}}(\rho)$ is the supremum of real $r\ge0$ such that, for every $\varepsilon>0$ , all sufficiently large natural $n$ admit a PPT channel taking $\rho^{\otimes n}$ within trace norm $\varepsilon$ of $\Phi_{\lceil2^{nr}\rceil}$ . The quantity $C_{\mathrm{PPT}}(\rho)$ is the infimum of real $r\ge0$ such that, for every $\varepsilon,\delta>0$ , all sufficiently large positive natural $n$ admit $m\in\mathbb N$ and a PPT channel taking $\Phi_{2^m}$ within trace norm $\varepsilon$ of $\rho^{\otimes n}$ , with $m\le n(r+\delta)$ . Tensor-power entries are products of the single-copy entries, party registers are grouped and relabelled by fixed finite-index bijections, and the preparation definition permits $m=0$ .

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