Sufficient condition for attaining the trace-norm fidelity bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P43.trace_norm_bound_attainment

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$ , $m\ge2$ , and let $\rho$ be any density operator. Let $P_{\rm neg}$ be the negative spectral projector of $\rho^\Gamma$ . If $\|P_{\rm neg}^\Gamma\|_\infty\le1/2$ , then $A=(I-2P_{\rm neg}^\Gamma)/m$ is admissible and its isotropic PPT channel attains the optimal overlap:

\operatorname{tr}(P_mT_A(\rho))=F_m(\rho)=\frac{\|\rho^\Gamma\|_1}{m}.

The optimum is over admissible positive PPT maps. This is a sufficient condition only and includes PPT states, for which $P_{\rm neg}=0$ and $A=I/m$ .

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.3, last sentence before Section III: sufficient condition for attaining
(10), with the explicit epsilon=2 channel. Includes PPT states, where P_neg=0.
The nontrivial target restriction m>=2 is inherited from (6); no converse is asserted. -/
theorem trace_norm_bound_attainment (d m : ℕ) (hd : 0 < d) (hm : 2 ≤ m)
    (rho : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ)
    (hrho : IsDensityMatrix rho)
    (hsmall : specNorm (gamma (negativeProjector rho)) ≤ 1/2) :
    let A := negativeSpaceWitness rho m 2
    RainsFeasibleEffect m A ∧ IsPositiveConjugatePPTChannel (isotropicPreparation m A) ∧
      effectProb (bellProjector m) (isotropicPreparation m A rho) = traceNorm (gamma rho) / (m : ℝ) ∧
      IsGreatest (positivePPTFidelityValues rho m) (traceNorm (gamma rho) / (m : ℝ)) := 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. 3, Sentence immediately after Eq. (10)

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$ and every positive semidefinite complex matrix $\rho$ of trace one indexed by $\{0,\ldots,d-1\}^2$ , define $(\Gamma X)_{(a,b),(a',b')}=X_{(a,b'),(a',b)}$ and $Q=\mathbf1_{(-\infty,0)}(\Gamma\rho)$ , using functional calculus with the function that is one on strictly negative eigenvalues and zero elsewhere. Suppose that the Euclidean operator norm satisfies $\|\Gamma Q\|_{\mathrm{op}}\le1/2$ , with no assumption that $\Gamma\rho$ has a negative eigenvalue. Set $A=(I-2\Gamma Q)/m$ , let $P_m$ have entry $1/m$ when both row and column pairs have equal components and zero otherwise, and define

\mathcal P_m(A)(X) =\frac{\operatorname{tr}(X(I-A))}{m^2-1}(I-P_m)+\operatorname{tr}(XA)P_m.

Then $A$ is Hermitian and $A$ , $I-A$ , $I-m\Gamma A$ , and $I+m\Gamma A$ are positive semidefinite. The map $\mathcal P_m(A)$ is positive, trace preserving, completely positive, and satisfies $\Gamma\mathcal P_m(A)(\Gamma X)\ge0$ for every $X\ge0$ ; complete positivity means positivity of its blockwise extension by every finite identity map, including auxiliary size zero. Its overlap satisfies

\operatorname{Re}\operatorname{tr}\!\bigl(P_m\mathcal P_m(A)(\rho)\bigr) =\frac{\|\Gamma\rho\|_1}{m}, \qquad \|Y\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Y^\dagger Y}.

This number is the greatest element of the set of overlaps $\operatorname{Re}\operatorname{tr}(P_mT(\rho))$ over all complex-linear maps $T$ to the $m^2$ -dimensional output matrix space that are positive, preserve every matrix’s trace, and satisfy $\Gamma T(\Gamma X)\ge0$ for every $X\ge0$ : it is itself attained and is at least every other value in that set, whose defining maps need not be completely positive.

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