Corollary 2: corrected nonnegative-coefficient version

Open

QAlgorithms.Papers.Independent.Intakethird100.P09.nearSep_uniform_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. Fix positive local dimension d, epsilon>0, and nonnegative Bell coefficients. Define D(epsilon) using normalized states with an actual separable witness sigma satisfying the full-norm bound on their partial transposes. Then

\sup_{\rho\in D(\epsilon)}Q_S(\rho)\le C(S)+\epsilon Q(S).

The state supremum has this fixed dimension, while Q(S) remains dimension-unrestricted. This corrected nonnegative-coefficient version gives a uniform bound for the near-separable set.

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 p.3, Corollary 2, Eq.(6), CORRECTED to nonnegative Bell coefficients.
Dimension is fixed before taking the state supremum; Q(S) remains unrestricted. -/
theorem nearSep_uniform_bell_bound (d : ℕ+) (S : BellScenario) (s : BellCoefficients S)
    (hs : ∀ x y a b, 0 ≤ s x y a b) (epsilon : ℝ) (hepsilon : 0 < epsilon) :
    sSup {v : ℝ | ∃ rho : Op (Fin d × Fin d), rho ∈ nearSep epsilon ∧
      v = stateValue s rho} ≤ classicalBound s + epsilon * quantumBound s := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P09

end

Source

Bounds on quantum nonlocality via partial transposition, arXiv:1407.6999v3, PDF p. 3, Corollary 2: 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 input and output sizes, every family of nonnegative real Bell coefficients $s_{xyab}$ , and every real $\epsilon>0$ ,

\sup_{\rho\in\mathcal N_\epsilon}V_s(\rho)\le C_s+\epsilon Q_s.

Here $\mathcal N_\epsilon$ consists of positive semidefinite trace- $1$ matrices $\rho$ on $\mathbb C^d\otimes\mathbb C^d$ admitting a finite separable density matrix $\tau=\sum_jw_jA_j\otimes B_j$ with $\|T_2(\rho)-T_2(\tau)\|_1\le\epsilon$ , where $w_j\ge0$ , $\sum_jw_j=1$ , and $A_j,B_j$ are positive semidefinite of trace $1$ . The transpose is $T_2(Z)_{(i,j),(k,l)}=Z_{(i,l),(k,j)}$ , and $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ . The quantity $V_s(\rho)$ is the supremum over local measurement effects $M_{a|x},N_{b|y}\ge0$ , 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 functions $f,g$ ; and $Q_s$ is the supremum of the measured expression over all positive finite local dimensions, all density matrices, and all such measurements. The supremum on the left is the real supremum specified in the declaration; $d=1$ and identically zero coefficients 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