Example Eq. (8): swap private bit CHSH bound

Open

QAlgorithms.Papers.Independent.Intakethird100.P09.swap_private_chsh

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 d>=1 be the local shield dimension and let X=F/d^2, where F sends |ij> to |ji>. Define gamma_X by Eq.(7), with its diagonal square-root blocks and external factor 1/2, regrouped on AA′:BB′. For CHSH in correlator normalization (classical bound 2 and quantum bound 2 sqrt(2)),

Q_{\mathrm{CHSH}}(\gamma_X)\le2+\frac{\sqrt2+1}{2\sqrt2\,d}.

This bounds CHSH violation for the particular swap private bit.

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.3, Eq.(8): swap private bit, correlator CHSH, denominator 2 sqrt(2) d. -/
theorem swap_private_chsh (d : ℕ+) :
    stateValue chshCoefficients (partyCut (swapPrivate d)) ≤
      2 + (Real.sqrt 2 + 1) / (2 * Real.sqrt 2 * (d : ℝ)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P09

end

Source

Bounds on quantum nonlocality via partial transposition, arXiv:1407.6999v3, PDF p. 3, Example Eq. (8): swap private bit CHSH bound

Read-back

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

For every positive integer $d$ , let $F_d$ be the matrix on $\mathbb C^d\otimes\mathbb C^d$ with entries $(F_d)_{(i,j),(k,l)}=1$ if $i=l$ and $j=k$ , and $0$ otherwise, and let $I$ be the identity on that space. Define a matrix $\Gamma_d$ on $(\mathbb C^2\otimes\mathbb C^d)\otimes(\mathbb C^2\otimes\mathbb C^d)$ by first grouping the two binary indices as a key: its key blocks $00,00$ and $11,11$ are $I/(2d^2)$ , its blocks $00,11$ and $11,00$ are $F_d/(2d^2)$ , and all other key blocks vanish. Equivalently, this is the regrouped matrix obtained from the four-block construction using $X=F_d/d^2$ , diagonal blocks $\sqrt{XX^\dagger}/2,\sqrt{X^\dagger X}/2$ , and off-diagonal blocks $X/2,X^\dagger/2$ . Then the supremum over binary local measurements $M_{a|x},N_{b|y}$ , for $x,y,a,b\in\{0,1\}$ , whose effects are positive semidefinite and sum to the identity for each input, satisfies

\sup_{M,N}\sum_{x,y,a,b} (-1)^{xy}(-1)^{a+b} \operatorname{Re}\operatorname{tr}((M_{a|x}\otimes N_{b|y})\Gamma_d) \le 2+\frac{\sqrt2+1}{2\sqrt2\,d}.

The quantifier includes $d=1$ .

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