Explicit alpha-family estimates and the strict irreversibility chain

Open

QAlgorithms.Papers.Independent.Intakethird100.P90.alpha_family_irreversibility

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 $21/50\le\alpha\le1/2$ , $\psi_1=\sqrt\alpha|01\rangle-\sqrt{1-\alpha}|10\rangle$ , $\psi_2=\sqrt\alpha|02\rangle-\sqrt{1-\alpha}|20\rangle$ , and $\rho^{(\alpha)}=(|\psi_1\rangle\langle\psi_1|+|\psi_2\rangle\langle\psi_2|)/2$ . With $E_W$ the infimum of $\log_2\|X^{T_B}\|_1$ over Hermitian $X\ge\rho$ , and $E_\eta$ the support-sandwich lower bound, the explicit estimates are

E_W(\rho^{(\alpha)})\le\log_2\|(\rho^{(\alpha)})^{T_B}\|_1=\log_2(1+\sqrt{2\alpha(1-\alpha)}),\qquad E_\eta(\rho^{(\alpha)})\ge-\log_2(1-\alpha).

Moreover,

\log_2(1+\sqrt{2\alpha(1-\alpha)})<-\log_2(1-\alpha),\qquad E_D(\rho^{(\alpha)})\le E_W(\rho^{(\alpha)})<E_\eta(\rho^{(\alpha)})\le E_C(\rho^{(\alpha)}).

The decimal endpoints are exact rationals. Below $\alpha=1/2$ this family need not be antisymmetric.

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.4--5: exact rational parameter interval,
both explicit estimates, the trace-norm evaluation, and the full irreversibility chain. -/
theorem alpha_family_irreversibility (alpha : ℝ)
    (hlower : (21/50 : ℝ) ≤ alpha) (hupper : alpha ≤ (1/2 : ℝ)) :
    wangDuanBound (alphaState alpha) ≤ Real.logb 2 (1 + Real.sqrt (2*alpha*(1-alpha))) ∧
    traceNorm (gamma (alphaState alpha)) = 1 + Real.sqrt (2*alpha*(1-alpha)) ∧
    -Real.logb 2 (1-alpha) ≤ etaEntanglement (alphaState alpha) ∧
    Real.logb 2 (1 + Real.sqrt (2*alpha*(1-alpha))) < -Real.logb 2 (1-alpha) ∧
    pptDistillable (alphaState alpha) ≤ (wangDuanBound (alphaState alpha) : EReal) ∧
    wangDuanBound (alphaState alpha) < etaEntanglement (alphaState alpha) ∧
    (etaEntanglement (alphaState alpha) : EReal) ≤ asymptoticEntanglementCost false (alphaState alpha) := 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. 5, Unnumbered family result: explicit irreversibility for 0.42<=alpha<=0.5

Read-back

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

For every real $\alpha$ with $\frac{21}{50}\le\alpha\le\frac12$ , let $\rho_\alpha=\frac12(v_1v_1^\dagger+v_2v_2^\dagger)$ on $\mathbb C^3\otimes\mathbb C^3$ , where $v_j=\sqrt{\alpha}\,|0,j\rangle-\sqrt{1-\alpha}\,|j,0\rangle$ for $j=1,2$ . Write $\Gamma X$ for the partial transpose with entries $(\Gamma X)_{(a,b),(c,d)}=X_{(a,d),(c,b)}$ , and $\|X\|_1=\operatorname{Re}\operatorname{Tr}\sqrt{X^\dagger X}$ . Define $W(\rho)$ as the infimum of $\log_2\|\Gamma X\|_1$ over Hermitian $X$ satisfying $X-\rho\succeq0$ . Let $P_\rho$ be the matrix obtained by applying the scalar function $t\mapsto0$ if $t=0$ , and $t\mapsto1$ otherwise, to $\rho$ by continuous functional calculus; define $\eta(\rho)$ as the infimum of $\|\Gamma Y\|_{\mathrm{op}}$ over Hermitian $Y$ with $Y-\Gamma P_\rho\succeq0$ and $Y+\Gamma P_\rho\succeq0$ , and define $E_\eta(\rho)=-\log_2\eta(\rho)$ . Here a PPT channel is a map $\Phi$ such that both $\Phi$ and $\Gamma\circ\Phi\circ\Gamma$ admit finite Kraus representations $\Phi(X)=\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ . Let $D_{\mathrm{PPT}}(\rho)$ be the supremum, in the extended real numbers, of nonnegative real rates $r$ such that, for every tolerance $\tau>0$ , all sufficiently large natural $n$ admit a PPT channel taking $\rho^{\otimes n}$ within trace norm $\tau$ of $\Omega_{\lceil2^{nr}\rceil}$ ; let $C_{\mathrm{PPT}}(\rho)$ be the extended-real infimum of nonnegative real rates $r$ such that, for every $\varepsilon,\delta>0$ , all sufficiently large positive $n$ admit a natural $m\le n(r+\delta)$ and a PPT channel taking $\Omega_{2^m}$ within trace norm $\varepsilon$ of $\rho^{\otimes n}$ . Tensor-power basis indices are relabelled by the specified finite-set bijections, and $(\Omega_k)_{(a,b),(c,d)}=1/k$ when $a=b$ and $c=d$ , and is zero otherwise; $m=0$ and rate $r=0$ are allowed. The assertion is

\begin{aligned} W(\rho_\alpha)&\le \log_2\!\left(1+\sqrt{2\alpha(1-\alpha)}\right),\\ \|\Gamma\rho_\alpha\|_1&=1+\sqrt{2\alpha(1-\alpha)},\\ -\log_2(1-\alpha)&\le E_\eta(\rho_\alpha),\\ \log_2\!\left(1+\sqrt{2\alpha(1-\alpha)}\right)&<-\log_2(1-\alpha),\\ D_{\mathrm{PPT}}(\rho_\alpha)&\le W(\rho_\alpha),\\ W(\rho_\alpha)&<E_\eta(\rho_\alpha),\\ E_\eta(\rho_\alpha)&\le C_{\mathrm{PPT}}(\rho_\alpha), \end{aligned}

where real quantities in extended-real inequalities are embedded into the extended real numbers.

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