The steering-ellipsoid CHSH bound

Abstract

Every two-qubit density matrix with steering-ellipsoid centre of length c has CHSH nonlocality at most max(2 sqrt(2(1 - c)), 2). At every c in [0, 1] this is the supremum over states with that centre length, proving Conjecture 1 of Milne, Jennings, Jevtic and Rudolph.

Definition 1.1 (The CHSH operator).

$$\forall a\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\forall aPrime\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\forall b\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\forall bPrime\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\mathrm{bell}\left(a,aPrime,b,bPrime\right)=\mathrm{Matrix}.\mathrm{kronecker}\left(D5.S3.\mathrm{QuantumChannels}.\mathrm{PauliThreeWeightBayesianInverseUniqueness}.\mathrm{spin}\left(a\right),D5.S3.\mathrm{QuantumChannels}.\mathrm{PauliThreeWeightBayesianInverseUniqueness}.\mathrm{spin}\left(b+bPrime\right)\right)+\mathrm{Matrix}.\mathrm{kronecker}\left(D5.S3.\mathrm{QuantumChannels}.\mathrm{PauliThreeWeightBayesianInverseUniqueness}.\mathrm{spin}\left(aPrime\right),D5.S3.\mathrm{QuantumChannels}.\mathrm{PauliThreeWeightBayesianInverseUniqueness}.\mathrm{spin}\left(b-bPrime\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.bell (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Section II defines B = alpha dot sigma tensor (beta + beta prime) dot sigma + alpha prime dot sigma tensor (beta - beta prime) dot sigma. The displayed variables aPrime and bPrime denote the primed directions. Matrix.kronecker is Mathlib’s Kronecker product, the alias of Matrix.kroneckerMap with multiplication of complex entries. The four vectors here are arbitrary; unit lengths are required in the value set.

Definition 1.2 (CHSH expectation values).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{chshValues}\left(rho\right)=\{r:\mathbb{R}\mid \exists a\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\exists aPrime\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\exists b\in \mathrm{Fin}\left(3\right)\to \mathbb{R},\exists bPrime\in \mathrm{Fin}\left(3\right)\to \mathbb{R},(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(a\right)=1)\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(aPrime\right)=1)\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(b\right)=1)\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(bPrime\right)=1)\wedge (r=\Vert \mathrm{Matrix}.\mathrm{trace}\left(rho\cdot \mathrm{bell}\left(a,aPrime,b,bPrime\right)\right)\Vert ))))\}$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.chshValues (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Section II maximizes the absolute value of tr(rho B) over four measurement directions. The set contains precisely these complex norms for unit directions, with Euclidean length D5.S3.Quantum.Entanglement.SteeringEllipsoidFullyEntangledFraction.vlen. Its definition permits any two-qubit operator rho.

Definition 1.3 (CHSH nonlocality).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{chsh}\left(rho\right)=\mathrm{sSup}\left(\mathrm{chshValues}\left(rho\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.chsh (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Section II: the maximal CHSH violation is beta(rho) = max_B |tr(rho B)|, where the maximization is over all four directions. The definition uses sSup of the real value set. This set is nonempty and bounded above for every two-qubit operator, and the proof uses no attainment assumption.

Definition 1.4 (The centre bound).

$$\forall t\in \mathbb{R},\mathrm{bound}\left(t\right)=\max \left(2\cdot \mathrm{Real}.\mathrm{sqrt}\left(2\cdot \left(1-t\right)\right),2\right)$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.bound (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Section V, Conjecture 1, gives the maximum of 2 sqrt(2(1 - t)) and 2. The function is defined for every real t with Mathlib’s Real.sqrt; the tightness statement restricts t to [0, 1].

Definition 1.5 (Conjecture 1).

$$(claim)\iff ((\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(rho\right))\Rightarrow ((\mathrm{Matrix}.\mathrm{trace}\left(rho\right)=1)\Rightarrow (\mathrm{chsh}\left(rho\right)\le \mathrm{bound}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{centre}\left(rho\right)\right)\right))))\wedge (\forall t\in \mathbb{R},(0\le t)\Rightarrow ((t\le 1)\Rightarrow (\forall epsilon\in \mathbb{R},(0<epsilon)\Rightarrow (\exists rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(rho\right))\wedge ((\mathrm{Matrix}.\mathrm{trace}\left(rho\right)=1)\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{centre}\left(rho\right)\right)=t)\wedge (\mathrm{bound}\left(t\right)-epsilon<\mathrm{chsh}\left(rho\right)))))))))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.claim (✓ std3).

Citation. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Section V, Conjecture 1: Let rho be a general two-qubit state with its steering ellipsoid centred at c. The CHSH nonlocality is tightly bounded as beta(rho) <= max[2 sqrt(2(1 - c)), 2]. Here c is the Euclidean length of D5.S3.Quantum.Entanglement.SteeringEllipsoidFullyEntangledFraction.centre. The first clause gives the inequality for every positive semidefinite matrix of trace one. The second expresses tightness as a supremum: for each t in [0, 1] and each epsilon > 0 there is a positive semidefinite trace-one matrix with centre length exactly t and CHSH value strictly greater than bound(t) - epsilon.

Theorem 1.6 (Agreement of Pauli indexing).

$$\forall i\in \mathrm{Fin}\left(3\right),D5.S3.\mathrm{QuantumChannels}.\mathrm{PauliThreeWeightBayesianInverseUniqueness}.\mathrm{sigma}\left(\mathrm{Fin}.\mathrm{succ}\left(i\right)\right)=D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(i\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.sigma_succ (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For every index i in Fin 3, the Pauli operator sigma at the successor index in Fin 4 equals pauli i.

Theorem 1.7 (Squared Euclidean length).

$$\forall u\in \mathrm{Fin}\left(3\right)\to \mathbb{R},(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(u\right){)}^2=\mathrm{dotProduct}\left(u,u\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.vlen_sq (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For every real three-vector, the square of its Euclidean length equals its dot product with itself.

Theorem 1.8 (Unit normalization).

$$\forall u\in \mathrm{Fin}\left(3\right)\to \mathbb{R},(u\ne 0)\Rightarrow ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left((\mathrm{inv}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(u\right)\right))\cdot (u)\right)=1)\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(u\right))\cdot ((\mathrm{inv}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(u\right)\right))\cdot (u))=u))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.normalized_unit (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Every nonzero real three-vector becomes unit length after division by its Euclidean length, and rescaling the normalized vector recovers the original vector.

Theorem 1.9 (Pauli expectations equal the correlations).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{Matrix}.\mathrm{IsHermitian}\left(rho\right))\Rightarrow (\forall i\in \mathrm{Fin}\left(3\right),\forall j\in \mathrm{Fin}\left(3\right),\mathrm{Matrix}.\mathrm{trace}\left(rho\cdot \mathrm{Matrix}.\mathrm{kronecker}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(i\right),D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left(j\right)\right)\right)=\mathrm{Complex}.\mathrm{ofReal}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{corr}\left(rho,i,j\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.trace_pauli_kronecker_eq_corr (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For every Hermitian complex two-qubit operator rho and every pair of Pauli indices i and j in Fin 3, the trace of rho times the corresponding Kronecker product equals its real correlation entry embedded in the complex numbers. Hermiticity makes this trace real.

Definition 1.10 (The difference of global and marginal purities).

$$\forall (X:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)),(\mathrm{delta}\left(X\right)=\mathrm{Complex}.\mathrm{re}\left(\mathrm{Matrix}.\mathrm{trace}\left(X\cdot X\right)\right)-\mathrm{Complex}.\mathrm{re}\left(\mathrm{Matrix}.\mathrm{trace}\left(D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}\left(X\right)\cdot D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{PartialTraceMutualInformation}.\mathrm{partialTraceRight}\left(X\right)\right)\right))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.delta (✓ std3).

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Delta(X) is the real trace of X squared minus the real trace of its Alice marginal squared. The partial trace is over Bob’s factor. This real-valued definition applies to every complex two-qubit matrix X.

Definition 1.11 (A direction-dependent spin flip).

$$\forall (n:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\mathrm{flipMatrix}\left(n\right)=\mathrm{Matrix}.\mathrm{kronecker}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left((1:\mathrm{Fin}\left(3\right))\right),D5.S3.\mathrm{QuantumChannels}.\mathrm{PauliThreeWeightBayesianInverseUniqueness}.\mathrm{spin}\left(n\right)\cdot D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{pauli}\left((1:\mathrm{Fin}\left(3\right))\right)\right))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.flipMatrix (✓ std3).

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For a real three-vector n, the conjugating matrix is the tensor product of the second Pauli matrix with spin(n) times that Pauli matrix. No unit-length condition is imposed in this definition.

Definition 1.12 (The flipped matrix).

$$\forall (X:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)),(\forall (n:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\mathrm{flipped}\left(X,n\right)=\mathrm{flipMatrix}\left(n\right)\cdot \mathrm{Matrix}.\mathrm{transpose}\left(X\right)\cdot \mathrm{Matrix}.\mathrm{conjTranspose}\left(\mathrm{flipMatrix}\left(n\right)\right)))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.flipped (✓ std3).

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Transpose X in the product basis and multiply it on the left by flipMatrix(n) and on the right by its adjoint. This construction preserves positive semidefiniteness because transposition and conjugation preserve it.

Lemma 1.13 (The directional flip identity).

$$\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)),((\mathrm{Matrix}.\mathrm{IsHermitian}\left(\rho \right))\Rightarrow ((\mathrm{Matrix}.\mathrm{trace}\left(\rho \right)=(1:\mathbb{C}))\Rightarrow (\forall (n:\mathrm{Fin}\left(3\right)\to \mathbb{R}),((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(n\right)=1)\Rightarrow (2\cdot \mathrm{Complex}.\mathrm{re}\left(\mathrm{Matrix}.\mathrm{trace}\left(\rho \cdot \mathrm{flipped}\left(\rho ,n\right)\right)\right)+\sum _{(i:\mathrm{Fin}\left(3\right))}(\sum _{(j:\mathrm{Fin}\left(3\right))}((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{corr}\left(\rho ,i,j\right){)}^2))-(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(\mathrm{Matrix}.\mathrm{mulVec}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{corr}\left(\rho \right),n\right)\right){)}^2+(\mathrm{dotProduct}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochB}\left(\rho \right),n\right){)}^2=1+2\cdot \mathrm{delta}\left(\rho \right))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.flip_purity_identity (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For a Hermitian trace-one matrix and a unit direction n, the real trace pairing with the flipped matrix, the squared Frobenius sum of the correlations, the squared length of Tn and Bob’s squared component along n satisfy this identity. Expanding the Pauli matrices gives its homogeneous form; trace one and the unit length of n give the displayed normalization.

Lemma 1.14 (A unit direction bounds a component).

$$\forall (a:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\forall (x:\mathrm{Fin}\left(3\right)\to \mathbb{R}),((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(a\right)=1)\Rightarrow (\left|\mathrm{dotProduct}\left(a,x\right)\right|\le D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(x\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.unit_dot_le (✓ std3). ∎

Citation. Sheldon Axler (2024). Linear Algebra Done Right, fourth edition. URL: https://linear.axler.net/.

Commentary.

The absolute component of a real three-vector x along a unit vector a is at most the Euclidean length of x. This is the real inner-product Cauchy-Schwarz inequality.

Lemma 1.15 (Bob’s Bloch vector lies in the unit ball).

$$\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)),((\mathrm{Matrix}.\mathrm{PosSemidef}\left(\rho \right))\Rightarrow ((\mathrm{Matrix}.\mathrm{trace}\left(\rho \right)=(1:\mathbb{C}))\Rightarrow (D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochB}\left(\rho \right)\right)\le 1)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.bob_radius_le (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

A positive semidefinite trace-one two-qubit matrix has a positive semidefinite trace-one Bob marginal. The norm of that marginal’s Bloch vector is at most its trace, hence at most one.

Lemma 1.16 (Purity difference bounded by the ellipsoid centre).

$$\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)),((\mathrm{Matrix}.\mathrm{PosSemidef}\left(\rho \right))\Rightarrow ((\mathrm{Matrix}.\mathrm{trace}\left(\rho \right)=(1:\mathbb{C}))\Rightarrow (\mathrm{delta}\left(\rho \right)\le \left(1-(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochB}\left(\rho \right)\right){)}^2\right)\cdot \left(\frac{1}{2}-D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{centre}\left(\rho \right)\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.delta_le_centre (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The purity difference is at most (1 - |b| squared)(1/2 - |centre(rho)|). When |b| < 1 an invertible filter makes Bob’s marginal maximally mixed; determinant scaling of Delta and the canonical state’s eigenvalue bound give the inequality. When |b| = 1, support on Bob’s pure marginal makes Delta zero, giving the boundary case.

Lemma 1.17 (The real correlation form of a CHSH expectation).

$$\forall (\rho :\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right)),((\mathrm{Matrix}.\mathrm{IsHermitian}\left(\rho \right))\Rightarrow (\forall (a:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\forall (a^{\prime }:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\forall (b:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\forall (b^{\prime }:\mathrm{Fin}\left(3\right)\to \mathbb{R}),(\mathrm{Matrix}.\mathrm{trace}\left(\rho \cdot \mathrm{bell}\left(a,a^{\prime },b,b^{\prime }\right)\right)=\mathrm{Complex}.\mathrm{ofReal}\left(\mathrm{dotProduct}\left(a,\mathrm{Matrix}.\mathrm{mulVec}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{corr}\left(\rho \right),b+b^{\prime }\right)\right)+\mathrm{dotProduct}\left(a^{\prime },\mathrm{Matrix}.\mathrm{mulVec}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{corr}\left(\rho \right),b-b^{\prime }\right)\right)\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.bell_trace_real_expansion (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For a Hermitian two-qubit matrix, the CHSH expectation equals the sum of the two real correlation dot products embedded in the complex numbers. Expanding the two Pauli observables and using real Pauli expectations gives the equality for arbitrary directions.

Definition 1.18 (The vector supported on the two equal-bit basis states).

$$\forall (t:\mathbb{R}),(\forall (s:\mathbb{R}),(\mathrm{tightVector}\left(t,s\right)=\lambda (k:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)))\mapsto (![![\mathrm{Complex}.\mathrm{ofReal}\left(\mathrm{Real}.\mathrm{sqrt}\left(1+s\right)\right),(0:\mathbb{C})],![(0:\mathbb{C}),\mathrm{Complex}.\mathrm{ofReal}\left(\mathrm{Real}.\mathrm{sqrt}\left(\left(1-t\right)\cdot \left(1-s\right)\right)\right)]]\left(\mathrm{Prod}.\mathrm{fst}\left(k\right),\mathrm{Prod}.\mathrm{snd}\left(k\right)\right))))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tightVector (✓ std3).

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

The vector has amplitudes sqrt(1+s) at (0,0), sqrt((1-t)(1-s)) at (1,1), and zero at the other two product indices. The real amplitudes are explicitly embedded in the complex numbers. The definition permits arbitrary real t and s.

Definition 1.19 (A two-term family of matrices).

$$\forall (t:\mathbb{R}),(\forall (s:\mathbb{R}),(\mathrm{tightState}\left(t,s\right)=\mathrm{HSMul}.\mathrm{hSMul}\left((\frac{1}{2}:\mathbb{C}),\mathrm{Matrix}.\mathrm{vecMulVec}\left(\mathrm{tightVector}\left(t,s\right),\mathrm{Star}.\mathrm{star}\left(\mathrm{tightVector}\left(t,s\right)\right)\right)\right)+\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{Complex}.\mathrm{ofReal}\left(\frac{t\cdot \left(1-s\right)}{2}\right),\mathrm{Matrix}.\mathrm{vecMulVec}\left(\lambda (k:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)))\mapsto (\mathrm{Complex}.\mathrm{ofReal}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{ev}\left(k\right)\right)),\mathrm{Star}.\mathrm{star}\left(\lambda (k:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)))\mapsto (\mathrm{Complex}.\mathrm{ofReal}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{ev}\left(k\right)\right))\right)\right)\right)))$$

Formalization. D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tightState (✓ std3).

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Take half the outer product of tightVector with its adjoint and add t(1-s)/2 times the projector onto the product basis vector (0,1). The latter vector is the real vector ev embedded coordinatewise in the complex numbers. The formula defines the family for all real parameters.

Lemma 1.20 (Positivity of the two-term family).

$$\forall (t:\mathbb{R}),(\forall (s:\mathbb{R}),((0\le t)\Rightarrow ((s\le 1)\Rightarrow (\mathrm{Matrix}.\mathrm{PosSemidef}\left(\mathrm{tightState}\left(t,s\right)\right)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tight_psd (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

If t is nonnegative and s is at most one, both coefficients in tightState are nonnegative. Each outer product is positive semidefinite, so their sum is positive semidefinite.

Lemma 1.21 (Trace, Bloch vectors and correlations of the family).

$$\forall (t:\mathbb{R}),(\forall (s:\mathbb{R}),((t\le 1)\Rightarrow ((0\le s)\Rightarrow ((s\le 1)\Rightarrow ((\mathrm{Matrix}.\mathrm{trace}\left(\mathrm{tightState}\left(t,s\right)\right)=(1:\mathbb{C}))\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochA}\left(\mathrm{tightState}\left(t,s\right)\right)=![0,0,t+\left(1-t\right)\cdot s])\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{blochB}\left(\mathrm{tightState}\left(t,s\right)\right)=![0,0,s])\wedge (D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{corr}\left(\mathrm{tightState}\left(t,s\right)\right)=\mathrm{Matrix}.\mathrm{diagonal}\left(![\mathrm{Real}.\mathrm{sqrt}\left(1+s\right)\cdot \mathrm{Real}.\mathrm{sqrt}\left(\left(1-t\right)\cdot \left(1-s\right)\right),-(\mathrm{Real}.\mathrm{sqrt}\left(1+s\right)\cdot \mathrm{Real}.\mathrm{sqrt}\left(\left(1-t\right)\cdot \left(1-s\right)\right)),1-t+t\cdot s]\right)))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tight_readouts (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For t <= 1 and 0 <= s <= 1, the matrix has trace one, both Bloch vectors lie on the third axis, and its correlation matrix is diagonal. The first two diagonal entries are opposite and equal in magnitude to sqrt(1+s) sqrt((1-t)(1-s)); the third is 1-t+ts. These equalities follow by evaluating the four product-basis entries and the Pauli traces.

Lemma 1.22 (The centre length of the family).

$$\forall (t:\mathbb{R}),(\forall (s:\mathbb{R}),((0\le t)\Rightarrow ((t\le 1)\Rightarrow ((0\le s)\Rightarrow ((s<1)\Rightarrow (D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{centre}\left(\mathrm{tightState}\left(t,s\right)\right)\right)=t))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tight_centre (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

For 0 <= t <= 1 and 0 <= s < 1, Bob’s Bloch length is s, so the centre denominator, one minus s squared, is nonzero. Substituting the Bloch vectors and diagonal correlations gives Alice’s centre (0,0,t), whose length is t.

Theorem 1.23 (The centre bound holds).

$$(\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(rho\right))\Rightarrow ((\mathrm{Matrix}.\mathrm{trace}\left(rho\right)=1)\Rightarrow (\mathrm{chsh}\left(rho\right)\le \mathrm{bound}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{centre}\left(rho\right)\right)\right))))\wedge (\forall t\in \mathbb{R},(0\le t)\Rightarrow ((t\le 1)\Rightarrow (\forall epsilon\in \mathbb{R},(0<epsilon)\Rightarrow (\exists rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(rho\right))\wedge ((\mathrm{Matrix}.\mathrm{trace}\left(rho\right)=1)\wedge ((D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{vlen}\left(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{SteeringEllipsoidFullyEntangledFraction}.\mathrm{centre}\left(rho\right)\right)=t)\wedge (\mathrm{bound}\left(t\right)-epsilon<\mathrm{chsh}\left(rho\right))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.result (✓ std3). ∎

Resolves. Problems/milne-jennings-jevtic-rudolph-2014-chsh-centre-bound (proved) by D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.result.

Source. Repository-derived.

Acknowledgement. Antony Milne; David Jennings; Sania Jevtic; Terry Rudolph (2014). Quantum correlations of two-qubit states with one maximally mixed marginal. DOI: 10.1103/PhysRevA.90.024302. URL: https://arxiv.org/abs/1404.3951v2.

Commentary.

Write T for the correlation matrix, b for Bob’s Bloch vector and Delta(X) = Re tr(X squared) - Re tr((tr_B X) squared). For orthonormal u, v and their normal n, conjugate the full transpose of rho by sigma_y tensor ((n dot sigma) sigma_y). The sum |Tu| squared + |Tv| squared plus (b dot n) squared plus twice the real trace of rho times this flipped state equals 1 + 2 Delta(rho). The flipped state is positive semidefinite, so the plane sum is at most 1 + 2 Delta(rho). The sum and difference of Bob’s two unit measurement directions are orthogonal; decomposing them and applying Cauchy-Schwarz reduces each CHSH expectation to twice the square root of such a plane sum.

The two-by-two determinant polarization identity gives Delta((I tensor F)X(I tensor F) adjoint) = |det F| squared Delta(X). For a state sigma with Bob marginal I/2 and Alice Bloch length c, the canonical bound sigma <= (1 - c/2)I bounds its eigenvalues and yields Delta(sigma) <= 1/2 - c. An explicit invertible filter makes Bob’s marginal maximally mixed when |b| < 1, giving Delta(rho) <= (1 - |b| squared)(1/2 - c). When |b| = 1, Bob’s marginal is a projector; filtering by this projector leaves rho fixed and has determinant zero, so Delta(rho) = 0. Thus every plane sum is at most max(2(1 - c), 1), giving the stated CHSH bound.

For tightness, let R(t, s) = |v><v|/2 + t(1 - s)|01><01|/2, where v = sqrt(1 + s)|00> + sqrt((1 - t)(1 - s))|11>. For 0 <= t <= 1 and 0 <= s < 1 this is a density matrix with centre (0, 0, t). At s = 0, CHSH settings in the xy plane attain 2 sqrt(2(1 - t)), proving tightness when t <= 1/2. For 1/2 < t < 1, the four z directions give 2(1 - t + ts); choosing s = 2/(2 + epsilon) makes this strictly greater than 2 - epsilon. At t = s = 1 the product state |00><00| has centre length one and CHSH value two.

References

• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.bell
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.bell_trace_real_expansion
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.bob_radius_le
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.bound
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.chsh
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.chshValues
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.claim
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.delta
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.delta_le_centre
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.flipMatrix
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.flip_purity_identity
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.flipped
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.normalized_unit
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.result
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.sigma_succ
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tightState
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tightVector
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tight_centre
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tight_psd
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.tight_readouts
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.trace_pauli_kronecker_eq_corr
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.unit_dot_le
• Truth anchor: D5/S3/Quantum/Entanglement/SteeringEllipsoidCHSH.vlen_sq
• Dependency: D5/S3/Quantum/Entanglement/SteeringEllipsoidFullyEntangledFraction
• Dependency: D5/S3/Quantum/Information/ActualPureQubitCostInfimum
• Dependency: D5/S3/Quantum/Information/ActualQubitChordObstruction
• Dependency: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation
• Dependency: D5/S3/Quantum/QuantumChannels/QubitWassersteinCouplings
• Dependency: D5/S3/QuantumChannels/PauliThreeWeightBayesianInverseUniqueness