Observation 1: corrected nonnegative-coefficient version

Open

QAlgorithms.Papers.Independent.Intakethird100.P09.private_operator_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. Let X be an operator on a positive finite bipartite shield with full trace norm one. Suppose sqrt(XX^dagger) and sqrt(X^dagger X) are normalized separable shield states. Define gamma_X exactly by Eq.(7), on the physical key-plus-shield ownership cut. For every nonnegative-coefficient Bell expression,

Q_S(\gamma_X)\le C(S)+Q(S)\|X^\Gamma\|_1.

Here Gamma on X acts only on Bob’s shield. The coefficient is one, without an additional half. This corrected version provides a reusable bound for operator-defined private bits.

The fixed private-bit formula used here is

\gamma_X=\frac12\left(|00\rangle\langle00|\otimes\sqrt{XX^\dagger}+|00\rangle\langle11|\otimes X+|11\rangle\langle00|\otimes X^\dagger+|11\rangle\langle11|\otimes\sqrt{X^\dagger X}\right),

with the two key qubits and shields regrouped by owner.

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.7, Observation 1, Eq.(A.3), CORRECTED s>=0 and Q(gamma_X) to Q_S(gamma_X).
Both square-root shield states are normalized SEP; X has full trace norm one. -/
theorem private_operator_bell_bound (a b : ℕ+) (S : BellScenario) (s : BellCoefficients S)
    (hs : ∀ x y i j, 0 ≤ s x y i j) (X : Op (Fin a × Fin b))
    (hX : traceNorm X = 1) (hleft : IsSeparableDensity (cfc Real.sqrt (X * Xᴴ)))
    (hright : IsSeparableDensity (cfc Real.sqrt (Xᴴ * X))) :
    stateValue s (partyCut (xForm X)) ≤
      classicalBound s + quantumBound s * traceNorm (transposeSecond X) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P09

end

Source

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

Read-back

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

Let $a,b$ be positive integers, let a Bell scenario have positive finite input and output sizes, and let $s_{xyij}\ge0$ be real coefficients. Let $X$ be any complex matrix on $\mathbb C^a\otimes\mathbb C^b$ with $\|X\|_1=1$ , and suppose both $\sqrt{XX^\dagger}$ and $\sqrt{X^\dagger X}$ admit finite decompositions $\sum_jw_jA_j\otimes B_j$ with $w_j\ge0$ , $\sum_jw_j=1$ , and positive semidefinite trace- $1$ local matrices $A_j,B_j$ . Form $\Gamma_X$ on local dimensions $2a,2b$ by grouping the two binary indices as a key, with blocks $(\Gamma_X)_{00,00}=\sqrt{XX^\dagger}/2$ , $(\Gamma_X)_{00,11}=X/2$ , $(\Gamma_X)_{11,00}=X^\dagger/2$ , and $(\Gamma_X)_{11,11}=\sqrt{X^\dagger X}/2$ , and all other key blocks zero. Then

V_s(\Gamma_X)\le C_s+Q_s\|T_2(X)\|_1,

where $T_2(X)_{(i,j),(k,l)}=X_{(i,l),(k,j)}$ , $\|Z\|_1=\operatorname{Re}\operatorname{tr}\sqrt{Z^\dagger Z}$ , $V_s$ is the supremum of $\sum s_{xyij}\operatorname{Re}\operatorname{tr}((M_{i|x}\otimes N_{j|y})\Gamma_X)$ over local positive semidefinite measurement effects summing to the identity for each input, $C_s=\sup_{f,g}\sum_{x,y}s_{xy,f(x),g(y)}$ , and $Q_s$ is the supremum of that measured expression over all positive finite local dimensions, density matrices, and local measurements. Matrix square roots use functional calculus; either $a$ or $b$ may equal $1$ , and $X$ itself is not assumed Hermitian or 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