Definitions for Distillability via protocols respecting the positivity of partial transpose

Definition

QAlgorithms_Papers_Independent_Intakethird100_P43

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

prove2quantum

The objects the formalized statements of Distillability via protocols respecting the positivity of partial transpose (arXiv:quant-ph/0104095) are stated in. Each was checked against the paper by a blind read-back and a moderator.

IsPPTMap: PDF p.2, opening of Section II: positive, trace-preserving, and Gamma T Gamma positive on every positive operator. The last condition has no CP amplification.
IsPositiveConjugatePPTChannel: PDF pp.1–2: an admissible channel is additionally completely positive. The frozen CP predicate tests id_r tensor T for every finite ancillary dimension r. This differs from Information100.P04.IsPPTChannel, which also requires CP of Gamma T Gamma; that stronger class is deliberately not substituted here.
IsPositiveConjugatePPTDistillable: PDF pp.1,3 and Theorem 1 p.2: qualitative distillability means that arbitrarily small singlet error is possible from finitely many identical copies. No rate is prescribed. The channels may depend on the known state and accuracy; they act linearly on all inputs.
RainsFeasibleEffect: PDF p.2, (2): the Hermitian effect A and the two Loewner bounds on m Gamma(A). All inequalities are expressed as positivity of the corresponding differences.
linearTracePair: PDF p.2, (3): the complex-linear functional X |-> Tr(X A).
isotropicRaw: PDF p.2, (3): the two-coefficient isotropic map, on every complex operator X.
complementaryCoefficient: PDF p.2, trace equation after (3): B is computed from A, not independent. Used at m>=2, where m^2-1 is nonzero.
isotropicPreparation: PDF p.2, (3) with its trace constraint imposed.
HasIsotropicForm: PDF p.2: maps of the precise form (3), independently of positivity or trace constraints.
negativeSpaceWitness: PDF p.2, (6): the constructed A. Also used at epsilon=2 in the attainment result. In the PPT case P_neg=0 and this is I/m without taking an inverse of its norm.
positivePPTFidelityValues: PDF p.2, (1): the operational set of attainable fidelities, over the positive trace-preserving PPT maps of this paper. IsGreatest records both optimality and attainment, so no real supremum default on an empty or unbounded set is used.

Definition code

import Mathlib
import Definitions.Def_QAlgorithms_Defs_EntanglementNegativity
import Definitions.Def_QAlgorithms_Defs_MatrixMapPositivity
import Definitions.Def_QAlgorithms_Papers_Independent_Information100_P04
import Definitions.Def_QAlgorithms_Papers_Independent_Information100_P30

/-!
Statements from Eggeling, Vollbrecht, Werner and Wolf, arXiv:quant-ph/0104095v2.
All page numbers are PDF pages. Accepted imports supply Bob transpose, copies,
Bell and negative spectral projectors, Werner states, and positive complex-linear maps.
Paper-specific definitions implement only the finite-dimensional
model of this paper. In particular PPT preservation below means POSITIVITY of the
transpose-conjugated map, not complete positivity of that map.
Compilation is pending the separate mechanical handoff.
-/

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P43

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Information100.P04
  (gamma copies bellProjector negativeProjector werner)
open QAlgorithms.Papers.Independent.Information100.P30 (IsPositiveMap)

/-- PDF p.2, opening of Section II: positive, trace-preserving, and Gamma T Gamma
positive on every positive operator. The last condition has no CP amplification. -/
def IsPPTMap {I J K L : Type*} [Fintype I] [Fintype J] [Fintype K] [Fintype L]
    (T : Matrix (I × J) (I × J) ℂ →ₗ[ℂ] Matrix (K × L) (K × L) ℂ) : Prop :=
  IsPositiveMap T ∧ (∀ X, (T X).trace = X.trace) ∧
    ∀ X, X.PosSemidef → (gamma (T (gamma X))).PosSemidef

/-- PDF pp.1–2: an admissible channel is additionally completely positive.
The frozen CP predicate tests id_r tensor T for every finite ancillary dimension r.
This differs from Information100.P04.IsPPTChannel, which also requires CP of
Gamma T Gamma; that stronger class is deliberately not substituted here. -/
def IsPositiveConjugatePPTChannel {I J K L : Type*} [Fintype I] [Fintype J] [Fintype K] [Fintype L]
    (T : Matrix (I × J) (I × J) ℂ →ₗ[ℂ] Matrix (K × L) (K × L) ℂ) : Prop :=
  IsPPTMap T ∧ Entanglement.IsCompletelyPositive T

/-- PDF pp.1,3 and Theorem 1 p.2: qualitative distillability means that arbitrarily
small singlet error is possible from finitely many identical copies. No rate is prescribed.
The channels may depend on the known state and accuracy; they act linearly on all inputs. -/
def IsPositiveConjugatePPTDistillable {I J : Type*} [Fintype I] [Fintype J]
    (rho : Matrix (I × J) (I × J) ℂ) : Prop :=
  ∀ eta : ℝ, 0 < eta → eta < 1 → ∃ n : ℕ, 0 < n ∧
    ∃ T : Matrix ((Fin n → I) × (Fin n → J))
        ((Fin n → I) × (Fin n → J)) ℂ →ₗ[ℂ]
        Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ,
      IsPositiveConjugatePPTChannel T ∧ 1 - eta ≤ effectProb (bellProjector 2) (T (copies rho n))

/-- PDF p.2, (2): the Hermitian effect A and the two Loewner bounds on m Gamma(A).
All inequalities are expressed as positivity of the corresponding differences. -/
def RainsFeasibleEffect {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    (m : ℕ) (A : Matrix (I × J) (I × J) ℂ) : Prop :=
  A.IsHermitian ∧ IsEffect A ∧
    (1 - (m : ℂ) • gamma A).PosSemidef ∧
    (1 + (m : ℂ) • gamma A).PosSemidef

/-- PDF p.2, (3): the complex-linear functional X |-> Tr(X A). -/
def linearTracePair {I : Type*} [Fintype I] (A : Matrix I I ℂ) : Matrix I I ℂ →ₗ[ℂ] ℂ where
  toFun X := (X * A).trace
  map_add' X Y := by simp [Matrix.add_mul]
  map_smul' c X := by simp [Matrix.smul_mul]

/-- PDF p.2, (3): the two-coefficient isotropic map, on every complex operator X. -/
def isotropicRaw {I J : Type*} [Fintype I] [Fintype J]
    (m : ℕ) (A B : Matrix (I × J) (I × J) ℂ) :
    Matrix (I × J) (I × J) ℂ →ₗ[ℂ] Matrix (Fin m × Fin m) (Fin m × Fin m) ℂ :=
  (linearTracePair B).smulRight (1 - bellProjector m) +
    (linearTracePair A).smulRight (bellProjector m)

/-- PDF p.2, trace equation after (3): B is computed from A, not independent.
Used at m>=2, where m^2-1 is nonzero. -/
def complementaryCoefficient {I J : Type*} [DecidableEq I] [DecidableEq J]
    (m : ℕ) (A : Matrix (I × J) (I × J) ℂ) : Matrix (I × J) (I × J) ℂ :=
  (((m : ℂ)^2 - 1)⁻¹) • (1 - A)

/-- PDF p.2, (3) with its trace constraint imposed. -/
def isotropicPreparation {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    (m : ℕ) (A : Matrix (I × J) (I × J) ℂ) :=
  isotropicRaw m A (complementaryCoefficient m A)

/-- PDF p.2: maps of the precise form (3), independently of positivity or trace constraints. -/
def HasIsotropicForm {I J : Type*} [Fintype I] [Fintype J] {m : ℕ}
    (T : Matrix (I × J) (I × J) ℂ →ₗ[ℂ] Matrix (Fin m × Fin m) (Fin m × Fin m) ℂ) : Prop :=
  ∃ A B, T = isotropicRaw m A B

/-- PDF p.2, (6): the constructed A. Also used at epsilon=2 in the attainment result.
In the PPT case P_neg=0 and this is I/m without taking an inverse of its norm. -/
def negativeSpaceWitness {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    (rho : Matrix (I × J) (I × J) ℂ) (m : ℕ) (epsilon : ℝ) :
    Matrix (I × J) (I × J) ℂ :=
  ((m : ℂ)⁻¹) • (1 - (epsilon : ℂ) • gamma (negativeProjector rho))

/-- PDF p.2, (1): the operational set of attainable fidelities, over the positive
trace-preserving PPT maps of this paper. IsGreatest records both optimality and attainment,
so no real supremum default on an empty or unbounded set is used. -/
def positivePPTFidelityValues {I J : Type*} [Fintype I] [Fintype J]
    (rho : Matrix (I × J) (I × J) ℂ) (m : ℕ) : Set ℝ :=
  {v | ∃ T : Matrix (I × J) (I × J) ℂ →ₗ[ℂ]
      Matrix (Fin m × Fin m) (Fin m × Fin m) ℂ,
    IsPPTMap T ∧ v = effectProb (bellProjector m) (T rho)}

/-- Sanity check: the identity satisfies the paper's channel convention. -/
example {I J : Type*} [Fintype I] [Fintype J] :
    IsPositiveConjugatePPTChannel (LinearMap.id : Matrix (I × J) (I × J) ℂ →ₗ[ℂ]
      Matrix (I × J) (I × J) ℂ) := by
  constructor
  · refine ⟨?_, ?_, ?_⟩
    · intro X hX; exact hX
    · intro X; rfl
    · intro X hX; exact hX
  · intro r X hX
    exact hX

example {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    (m : ℕ) : RainsFeasibleEffect m (0 : Matrix (I × J) (I × J) ℂ) := by
  have hg : gamma (0 : Matrix (I × J) (I × J) ℂ) = 0 := rfl
  refine ⟨Matrix.PosSemidef.zero.isHermitian, ⟨Matrix.PosSemidef.zero, ?_⟩, ?_, ?_⟩
  · simpa only [sub_zero] using (Matrix.PosSemidef.one :
      (1 : Matrix (I × J) (I × J) ℂ).PosSemidef)
  · simpa only [hg, smul_zero, sub_zero] using (Matrix.PosSemidef.one :
      (1 : Matrix (I × J) (I × J) ℂ).PosSemidef)
  · simpa only [hg, smul_zero, add_zero] using (Matrix.PosSemidef.one :
      (1 : Matrix (I × J) (I × J) ℂ).PosSemidef)

example {I J : Type*} (X : Matrix (I × J) (I × J) ℂ) : gamma (gamma X) = X := rfl

example {I J : Type*} (X : Matrix (I × J) (I × J) ℂ) :
    gamma X = (Entanglement.partialTransposeFirst X).transpose := rfl

example (m : ℕ) :
    bellProjector (m+1) ((0 : Fin (m+1)), 0) (0, 0) = ((m+1 : ℕ) : ℂ)⁻¹ := by
  simp [bellProjector]

example : bellProjector 1 = (1 : Matrix (Fin 1 × Fin 1) (Fin 1 × Fin 1) ℂ) := by
  ext i j
  simp [bellProjector, Matrix.one_apply, Subsingleton.elim i j, Subsingleton.elim i.1 i.2,
    Subsingleton.elim j.1 j.2]

example {I J : Type*} (rho : Matrix (I × J) (I × J) ℂ) : copies rho 0 = 1 := by
  ext i j
  simp [copies, Matrix.one_apply, Subsingleton.elim i j]

example {I : Type*} [Fintype I] (A X : Matrix I I ℂ) :
    linearTracePair A X = (X * A).trace := rfl

example {I J : Type*} [Fintype I] [Fintype J] (m : ℕ)
    (A B X : Matrix (I × J) (I × J) ℂ) :
    isotropicRaw m A B X = (X*B).trace • (1-bellProjector m) +
      (X*A).trace • bellProjector m := rfl

example {I J : Type*} [DecidableEq I] [DecidableEq J]
    (A : Matrix (I × J) (I × J) ℂ) : complementaryCoefficient 2 A = (1/3 : ℂ) • (1-A) := by
  norm_num [complementaryCoefficient]

example {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] :
    negativeProjector (0 : Matrix (I × J) (I × J) ℂ) = 0 := by
  have hz : gamma (0 : Matrix (I × J) (I × J) ℂ) = 0 := rfl
  simp [negativeProjector, hz, cfc_apply_zero]

example {I J : Type*} [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J]
    (rho : Matrix (I × J) (I × J) ℂ) (m : ℕ) :
    negativeSpaceWitness rho m 0 = ((m : ℂ)⁻¹) • 1 := by simp [negativeSpaceWitness]

example (d : ℕ) : werner d 0 =
    (((2 / ((d : ℝ)*(d+1)) : ℝ) : ℂ)) •
      QAlgorithms.Papers.Independent.Information100.P04.wernerP0 d := by simp [werner]

end QAlgorithms.Papers.Independent.Intakethird100.P43

Source

Distillability via protocols respecting the positivity of partial transpose, arXiv:quant-ph/0104095v2, https://arxiv.org/abs/quant-ph/0104095v2

Read-back

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

`QAlgorithms.Papers.Independent.Intakethird100.P43.HasIsotropicForm`

For finite types $I,J$ , a natural number $m$ , and a complex-linear map $T$ from matrices on $I\times J$ to matrices on $\{0,\ldots,m-1\}^2$ , this predicate says that there exist complex matrices $A,B$ on $I\times J$ such that, for every input matrix $X$ ,

T(X)=\operatorname{tr}(XB)(\mathbf1-B_m)+\operatorname{tr}(XA)B_m,

where $(B_m)_{(u,v),(u',v')}=1/m$ if $u=v$ and $u'=v'$ , and is zero otherwise. The witnesses $A,B$ need not be unique, Hermitian, positive, or normalized. Empty index types and $m=0$ are included, with the output matrix space having an empty index set at $m=0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P43.IsPPTMap`

For arbitrary finite types $I,J,K,L$ , which may be empty, and a complex-linear map $T$ from complex matrices indexed by $I\times J$ to those indexed by $K\times L$ , this predicate requires three properties: $T(X)$ is positive semidefinite whenever $X$ is positive semidefinite; $\operatorname{tr}(T(X))=\operatorname{tr}(X)$ for every matrix $X$ ; and $\Gamma(T(\Gamma(X)))$ is positive semidefinite whenever $X$ is positive semidefinite. On any product index set, $\Gamma$ is the operation defined entrywise by

(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}.

The inner and outer occurrences of $\Gamma$ use the input and output product index sets, respectively.

`QAlgorithms.Papers.Independent.Intakethird100.P43.IsPositiveConjugatePPTChannel`

For arbitrary finite types $I,J,K,L$ , including empty types, and a complex-linear map $T$ from matrices on $I\times J$ to matrices on $K\times L$ , this predicate requires that $T$ preserve positive semidefiniteness, preserve the complex trace of every matrix, and satisfy $\Gamma(T(\Gamma(X)))\succeq0$ for every $X\succeq0$ , where $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ on each relevant product index set. It additionally requires complete positivity: for every natural number $r$ , including $r=0$ , and every positive semidefinite matrix $X$ indexed by $\{0,\ldots,r-1\}\times(I\times J)$ , the matrix $Y$ with entries

Y_{(u,c),(v,c')}= \left[T\!\left((X_{(u,a),(v,a')})_{a,a'\in I\times J}\right)\right]_{c,c'}

is positive semidefinite, where $u,v<r$ and $c,c'\in K\times L$ .

`QAlgorithms.Papers.Independent.Intakethird100.P43.IsPositiveConjugatePPTDistillable`

For finite types $I,J$ and any complex matrix $\rho$ indexed by $I\times J$ , this predicate says that for every real $\eta$ with $0<\eta<1$ , there exist a positive natural number $n$ and a complex-linear map $T$ from matrices on $I^n\times J^n$ to matrices on $\{0,1\}\times\{0,1\}$ such that $T$ preserves positive semidefiniteness and the trace of every matrix, $\Gamma(T(\Gamma(X)))\succeq0$ whenever $X\succeq0$ , and every finite amplification of $T$ is positive: for every natural number $r$ , applying $T$ separately to each matrix block of any positive semidefinite matrix indexed by $\{0,\ldots,r-1\}\times(I^n\times J^n)$ yields a positive semidefinite matrix. Here $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ . These choices must satisfy

1-\eta\le \operatorname{Re}\operatorname{tr}\!\left(B_2\,T(\rho^{[n]})\right), \qquad (\rho^{[n]})_{(a,b),(a',b')}= \prod_{t=0}^{n-1}\rho_{(a_t,b_t),(a'_t,b'_t)},

where $(B_2)_{(u,v),(u',v')}=\tfrac12$ if $u=v$ and $u'=v'$ , and is zero otherwise. No density-matrix assumption is imposed on $\rho$ . Empty $I$ or $J$ are allowed as parameters, but then this predicate cannot hold, since $n>0$ makes the input matrix space zero and the displayed overlap zero.

`QAlgorithms.Papers.Independent.Intakethird100.P43.RainsFeasibleEffect`

For finite types $I,J$ with decidable equality, any natural number $m$ , and any complex matrix $A$ indexed by $I\times J$ , this predicate says that $A$ is Hermitian and that all four matrices

A,\qquad \mathbf1-A,\qquad \mathbf1-m\Gamma(A),\qquad \mathbf1+m\Gamma(A)

are positive semidefinite, where $\mathbf1$ is the identity matrix and $(\Gamma A)_{(i,j),(i',j')}=A_{(i,j'),(i',j)}$ . The index types may be empty, and $m=0$ is included; at $m=0$ , the last two matrices are both the identity.

`QAlgorithms.Papers.Independent.Intakethird100.P43.complementaryCoefficient`

For types $I,J$ with decidable equality, without any finiteness or nonemptiness assumption, a natural number $m$ , and any complex matrix $A$ indexed by $I\times J$ , this defines the matrix

\bigl(m^2-1\bigr)^{-1}(\mathbf1-A),

where the inverse is taken in $\mathbb C$ and $\mathbf1$ is the identity matrix. All natural values of $m$ are included: at $m=1$ , the inverse of zero is defined to be zero, so the result is the zero matrix; at $m=0$ , the result is $A-\mathbf1$ .

`QAlgorithms.Papers.Independent.Intakethird100.P43.isotropicPreparation`

For finite types $I,J$ with decidable equality, any natural number $m$ , and any complex matrix $A$ indexed by $I\times J$ , this defines the complex-linear map

X\longmapsto (m^2-1)^{-1}\operatorname{tr}\!\left(X(\mathbf1-A)\right)(\mathbf1-B_m) +\operatorname{tr}(XA)B_m.

Here $B_m$ , indexed by pairs of integers less than $m$ , has entry $1/m$ when both its row pair and its column pair have equal components, and zero otherwise; all scalars and inverses in the formula are complex. No positivity, Hermiticity, or normalization condition is imposed on $A$ . Empty input types and $m=0$ are permitted; for $m=0$ the output index set is empty, and for $m=1$ the zero-inverse convention gives the map $X\mapsto\operatorname{tr}(XA)\mathbf1$ .

`QAlgorithms.Papers.Independent.Intakethird100.P43.isotropicRaw`

For finite types $I,J$ , any natural number $m$ , and arbitrary complex matrices $A,B$ indexed by $I\times J$ , this defines the complex-linear map

X\longmapsto \operatorname{tr}(XB)(\mathbf1-B_m)+\operatorname{tr}(XA)B_m

into matrices indexed by $\{0,\ldots,m-1\}\times\{0,\ldots,m-1\}$ , where $(B_m)_{(u,v),(u',v')}=1/m$ if $u=v$ and $u'=v'$ , and is zero otherwise, with the scalar interpreted in $\mathbb C$ . No positivity or trace-preservation condition is imposed on this map or on $A,B$ . Empty input types and $m=0$ are included; when $m=0$ , the output index set is empty. When $m=1$ , $B_m=\mathbf1$ , so the map is $X\mapsto\operatorname{tr}(XA)\mathbf1$ .

`QAlgorithms.Papers.Independent.Intakethird100.P43.linearTracePair`

For any finite type $I$ , possibly empty, and any complex matrix $A$ indexed by $I$ , this defines the complex-linear functional

X\longmapsto \operatorname{tr}(XA) =\sum_{i\in I}\sum_{j\in I}X_{ij}A_{ji}.

There are no Hermiticity, positivity, or normalization assumptions on $A$ or $X$ , and the value is complex. If $I$ is empty, the functional is zero.

`QAlgorithms.Papers.Independent.Intakethird100.P43.negativeSpaceWitness`

For finite types $I,J$ with decidable equality, any complex matrix $\rho$ indexed by $I\times J$ , any natural number $m$ , and any real $\epsilon$ , this defines

m^{-1}\bigl(\mathbf1-\epsilon\,\Gamma(P_-)\bigr), \qquad P_-=\operatorname{cfc}\!\left(t\mapsto \begin{cases}1,&t<0,\\0,&t\ge0,\end{cases}\right)(\Gamma(\rho)),

where $(\Gamma X)_{(i,j),(i',j')}=X_{(i,j'),(i',j)}$ , and $\operatorname{cfc}$ is the functional-calculus operation on matrices. For Hermitian $\Gamma(\rho)$ , $P_-$ is its spectral projection onto the strictly negative eigenvalues. The definition itself assumes neither Hermiticity nor positivity nor trace one for $\rho$ , and allows every real $\epsilon$ , empty index types, and $m=0$ . The scalar inverse is taken in $\mathbb C$ , so the result at $m=0$ is zero.

`QAlgorithms.Papers.Independent.Intakethird100.P43.positivePPTFidelityValues`

For finite types $I,J$ , any complex matrix $\rho$ indexed by $I\times J$ , and any natural number $m$ , this defines the set of real numbers $v$ for which there exists a complex-linear map $T$ from matrices on $I\times J$ to matrices on $\{0,\ldots,m-1\}^2$ satisfying

v=\operatorname{Re}\operatorname{tr}(B_mT(\rho)).

The required conditions on $T$ are that it preserve positive semidefiniteness, preserve the complex trace of every matrix, and satisfy $\Gamma(T(\Gamma(X)))\succeq0$ for every $X\succeq0$ . Here $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , and $(B_m)_{(u,v),(u',v')}=1/m$ when $u=v$ and $u'=v'$ , and zero otherwise. No density-matrix assumption is imposed on $\rho$ , and no complete-positivity condition is imposed on $T$ . Empty input types and $m=0$ are included; at $m=0$ , every possible overlap is zero, and if $I,J$ are both nonempty, trace preservation makes the set empty.

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