Isotropic correspondence and complete-positive realization

Open

QAlgorithms.Papers.Independent.Intakethird100.P43.isotropic_correspondence

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

prove2quantum

All operators act on a finite bipartite space $\mathbb C^d\otimes\mathbb C^d$ in a fixed product basis. Write $\Gamma=T_2$ for Bob's partial transpose and $P_m=|\psi_m\rangle\langle\psi_m|$ , where $|\psi_m\rangle=m^{-1/2}\sum_i|ii\rangle$ . A density operator is positive semidefinite with complex trace exactly one. An admissible PPT map is complex-linear, positive and trace preserving, and $\Gamma_{\rm out}T\Gamma_{\rm in}$ is positive on every positive operator. A PPT channel is additionally completely positive; complete positivity of the transpose-conjugated map is not required. Fidelity means the overlap $\operatorname{tr}(P_m T(\rho))$ .

Let $d\ge1$ and $m\ge2$ . For a Hermitian operator $A$ satisfying $0\le A\le I$ and $-I\le mA^\Gamma\le I$ , construct $B=(I-A)/(m^2-1)$ and

T_A(X)=\operatorname{tr}(XB)(I-P_m)+\operatorname{tr}(XA)P_m.

This construction gives a one-to-one correspondence between these operators $A$ and admissible PPT maps of the two-coefficient isotropic form. The maps are channels and obey $\operatorname{tr}(P_mT_A(\rho))=\operatorname{tr}(\rho A)$ for every density operator $\rho$ . More generally, every positive complex-linear map of this isotropic form, even before imposing trace preservation, is completely positive.

This identifies the exact admissible witness operators with realizable channels.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P43

Formal statement

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, discussion after Lemma 1, (3)–(5): exact one-to-one correspondence,
with B=(I-A)/(m^2-1), and complete positivity of positive maps of isotropic form.
The fidelity is an overlap, not root fidelity. -/
theorem isotropic_correspondence (d m : ℕ) (hd : 0 < d) (hm : 2 ≤ m) :
    (∀ T : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ →ₗ[ℂ]
        Matrix (Fin m × Fin m) (Fin m × Fin m) ℂ,
      (IsPPTMap T ∧ HasIsotropicForm T) ↔
        ∃! A : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ,
          RainsFeasibleEffect m A ∧ isotropicPreparation m A = T) ∧
    (∀ A B : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ,
      IsPositiveMap (isotropicRaw m A B) →
        Entanglement.IsCompletelyPositive (isotropicRaw m A B)) ∧
    (∀ A : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ, RainsFeasibleEffect m A →
      IsPositiveConjugatePPTChannel (isotropicPreparation m A) ∧
        ∀ rho : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ,
          IsDensityMatrix rho → effectProb (bellProjector m) (isotropicPreparation m A rho) = effectProb A rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P43

end

Source

Distillability via protocols respecting the positivity of partial transpose, arXiv:quant-ph/0104095v2, PDF p. 2, Unnumbered discussion after Lemma 1, Eqs. (3)–(5)

Read-back

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

For every pair of natural numbers $d>0$ and $m\ge2$ , index the input matrices by $\{0,\ldots,d-1\}^2$ and the output matrices by $\{0,\ldots,m-1\}^2$ . On either space define $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ , and let $P_m$ have entry $1/m$ when both row and column pairs have equal components, and entry zero otherwise. Write

R_{A,B}(X)=\operatorname{tr}(XB)(I-P_m)+\operatorname{tr}(XA)P_m, \qquad \mathcal P_m(A)=R_{A,(I-A)/(m^2-1)}.

Call $A$ feasible when $A=A^\dagger$ and $A$ , $I-A$ , $I-m\Gamma A$ , and $I+m\Gamma A$ are all positive semidefinite. For every complex-linear map $T$ between these matrix spaces, the conjunction that $T$ sends positive semidefinite matrices to positive semidefinite matrices, preserves the trace of every matrix, satisfies $\Gamma T(\Gamma X)\ge0$ for every $X\ge0$ , and equals $R_{A,B}$ for some input matrices $A,B$ , is equivalent to the existence of exactly one feasible input matrix $A$ such that $\mathcal P_m(A)=T$ . Moreover, for every pair of arbitrary complex input matrices $A,B$ , positivity of $R_{A,B}$ implies its complete positivity. Finally, every feasible $A$ gives a map $\mathcal P_m(A)$ that is positive, trace preserving, completely positive, and satisfies $\Gamma\mathcal P_m(A)(\Gamma X)\ge0$ for every $X\ge0$ ; for every positive semidefinite input matrix $\rho$ with $\operatorname{tr}\rho=1$ ,

\operatorname{Re}\operatorname{tr}\!\bigl(P_m\mathcal P_m(A)(\rho)\bigr) =\operatorname{Re}\operatorname{tr}(A\rho).

Here complete positivity means that, for every natural number $r$ , including $r=0$ , applying the map to each matrix block of any positive semidefinite matrix indexed by an $r$ -element auxiliary index and the input index produces a positive semidefinite matrix.

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