Theorem 1, Eq. (1): partial-transpose Bell-value difference

Open

QAlgorithms.Papers.Independent.Intakethird100.P09.partialTranspose_bell_difference

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

prove2quantum

All states are normalized finite-dimensional bipartite density matrices. Gamma denotes transposition of Bob in the fixed product basis. The trace norm is the full trace norm. For a finite Bell expression S with real coefficients, C(S) and Q(S) are its largest signed classical value and its supremal signed quantum value over arbitrary finite local dimensions; Q_S(rho) optimizes complete local POVMs on the fixed state. Let rho and sigma have the same positive local dimension d, and fix the same local POVMs for both. Write S_M for the resulting Bell operator and S_M(rho) for its expectation. Then

|S_M(\rho)-S_M(\sigma)|\le\|S_M^\Gamma\|_\infty\,\|\rho^\Gamma-\sigma^\Gamma\|_1.

The coefficients may be signed, and neither state needs to be PPT. This relates a fixed Bell-value difference to distinguishability after transposition.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P09

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P09

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

open Filter

open QAlgorithms.Entanglement (IsSeparableDensity)

open QAlgorithms.Papers.Independent.Dependency50.P24
  (transposeSecond partyCut xForm swapPrivate hidingOne hidingTwo)

open QAlgorithms.Papers.Independent.Dependency50.P42 (dimensionedPower)

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Advance50.P47 (Box)

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntanglement)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- PDF pp.2,6, Theorem 1, Eq.(1): general real Bell coefficients, fixed common POVMs.
Neither state is assumed PPT; the full trace norm is used. -/
theorem partialTranspose_bell_difference (d : ℕ+) (S : BellScenario) (s : BellCoefficients S)
    (rho sigma : Op (Fin d × Fin d)) (hrho : IsDensityMatrix rho)
    (hsigma : IsDensityMatrix sigma) (M : Measurements S (Fin d) (Fin d)) :
    |bellValue s (measuredBox M rho) - bellValue s (measuredBox M sigma)| ≤
      bellOperatorNorm (transposeSecond (bellOperator s M)) *
        traceNorm (transposeSecond rho - transposeSecond sigma) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P09

end

Source

Bounds on quantum nonlocality via partial transposition, arXiv:1407.6999v3, PDF p. 2, Theorem 1, Eq. (1): partial-transpose Bell-value difference

Read-back

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

Let $d$ be any positive integer, let $X,Y,A,B$ be finite index sets of specified positive sizes forming a Bell scenario, and let $s_{xyab}$ be arbitrary real coefficients. Let $\rho,\sigma$ be positive semidefinite complex matrices of trace $1$ on $\mathbb C^d\otimes\mathbb C^d$ . For every pair of measurement families $M_{a|x},N_{b|y}$ on $\mathbb C^d$ , with every effect positive semidefinite and $\sum_aM_{a|x}=I$ , $\sum_bN_{b|y}=I$ , define $P_\omega(a,b|x,y)=\operatorname{Re}\operatorname{tr}((M_{a|x}\otimes N_{b|y})\omega)$ , $B_s(P)=\sum_{x,y,a,b}s_{xyab}P(a,b|x,y)$ , and $B_{s,M,N}=\sum_{x,y,a,b}s_{xyab}M_{a|x}\otimes N_{b|y}$ . If $T_2(Z)_{(i,j),(k,l)}=Z_{(i,l),(k,j)}$ denotes transpose on the second factor, then

|B_s(P_\rho)-B_s(P_\sigma)| \le \|T_2(B_{s,M,N})\|\;\|T_2(\rho)-T_2(\sigma)\|_1.

Here the first norm is the ambient matrix norm appearing in the definition of bellOperatorNorm, and $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ . There is no sign restriction on the coefficients, and $d=1$ and one-element input or output sets are included.

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