Corollary 1: corrected nonnegative-coefficient version

Open

QAlgorithms.Papers.Independent.Intakethird100.P09.separable_distance_bell_bound

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. Assume every coefficient of S is nonnegative and rho has positive equal local dimensions. Let SEP denote the normalized separable states on that same space. Then

Q_S(\rho)\le C(S)+Q(S)\inf_{\sigma\in\mathrm{SEP}}\|\rho^\Gamma-\sigma^\Gamma\|_1=C(S)+Q(S)\inf_{\sigma\in\mathrm{SEP}}\|\rho^\Gamma-\sigma\|_1.

The equality of the two infima is included. This is an explicitly corrected restriction of the printed unrestricted claim; it bounds fixed-state nonlocality by distance to SEP.

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--7, Corollary 1, Eq.(4), CORRECTED domain: all coefficients nonnegative.
Printed unrestricted signed formula is false. Also retains the equivalent untransposed-SEP form. -/
theorem separable_distance_bell_bound (d : ℕ+) (S : BellScenario) (s : BellCoefficients S)
    (hs : ∀ x y a b, 0 ≤ s x y a b) (rho : Op (Fin d × Fin d))
    (hrho : IsDensityMatrix rho) :
    stateValue s rho ≤ classicalBound s + quantumBound s * sepDistance rho ∧
    sepDistance rho = sepDistanceUntransposed rho ∧
    stateValue s rho ≤ classicalBound s + quantumBound s * sepDistanceUntransposed rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P09

end

Source

Bounds on quantum nonlocality via partial transposition, arXiv:1407.6999v3, PDF p. 2, Corollary 1: corrected nonnegative-coefficient version

Read-back

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

For every positive integer $d$ , every Bell scenario with positive finite numbers of inputs and outputs, every family of real coefficients $s_{xyab}\ge0$ , and every positive semidefinite trace- $1$ matrix $\rho$ on $\mathbb C^d\otimes\mathbb C^d$ , the following three assertions hold:

V_s(\rho)\le C_s+Q_sD(\rho),\qquad D(\rho)=D'(\rho),\qquad V_s(\rho)\le C_s+Q_sD'(\rho).

Here $V_s(\rho)$ is the real supremum, over all local positive semidefinite measurement effects summing to the identity for each input, of $\sum_{x,y,a,b}s_{xyab}\operatorname{Re}\operatorname{tr}((M_{a|x}\otimes N_{b|y})\rho)$ ; $C_s$ is the supremum of $\sum_{x,y}s_{xy,f(x),g(y)}$ over deterministic output functions $f,g$ ; and $Q_s$ is the supremum of the same measured Bell expression over all positive finite local dimensions, all positive semidefinite trace- $1$ bipartite matrices, and all such local measurements. With $T_2(Z)_{(i,j),(k,l)}=Z_{(i,l),(k,j)}$ and $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ , the two distances are $D(\rho)=\inf_{\tau\in\mathrm{Sep}_d}\|T_2(\rho)-T_2(\tau)\|_1$ and $D'(\rho)=\inf_{\tau\in\mathrm{Sep}_d}\|T_2(\rho)-\tau\|_1$ . The set $\mathrm{Sep}_d$ consists exactly of finite sums $\tau=\sum_jw_jA_j\otimes B_j$ , where $w_j\ge0$ , $\sum_jw_j=1$ , and all $A_j,B_j$ are positive semidefinite of trace $1$ . The case $d=1$ , zero coefficients, and scenarios with 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