The Exercise

Two qubits sit in separate labs. On the first one measures the spin along $\hat q$ or along $\hat r$, on the second along $\hat s$ or along $\hat t$, where $\hat q$, $\hat r$, $\hat s$ and $\hat t$ are real unit vectors in three dimensions. With $\vec\sigma$ the vector of Pauli matrices, the four observables are $Q = \hat q \cdot \vec\sigma$ and $R = \hat r \cdot \vec\sigma$ on the first qubit, $S = \hat s \cdot \vec\sigma$ and $T = \hat t \cdot \vec\sigma$ on the second. Each of them squares to the identity.

The exercise asks for the square of the operator $Q \otimes S + R \otimes S + R \otimes T - Q \otimes T$, the operator of the inequality of Clauser, Horne, Shimony and Holt (CHSH), and for an upper bound on its expectation value in a state of the two qubits. The bound is $2\sqrt{2}$, Tsirelson’s bound.

Systems and Observables

A quantum system $A$ is given by its state space, a finite dimensional complex Hilbert space.^✦ The composite system $A \otimes B$ of two quantum systems $A$ and $B$ is the quantum system whose state space is the tensor product of the state spaces of $A$ and $B$.^✦ The qubit is the quantum system whose state space is $\mathbb{C}^2$, and a pair of qubits is the composite system of a qubit with a qubit.

An observable $M$ on a quantum system $A$ is a self adjoint operator on the state space of $A$, $M^\dagger = M$.^✦ The tensor product $M \otimes N$ of an observable $M$ on $A$ and an observable $N$ on $B$ is the observable on $A \otimes B$ whose operator is the tensor product of the operators $M$ and $N$.^✦

A pure state $|\psi\rangle$ of a quantum system $A$ is a vector of unit norm in the state space of $A$, $\lVert \psi \rVert = 1$.^✦ The expectation value of an observable $M$ on $A$ in a pure state $|\psi\rangle$ of $A$ is the real number $$\langle M \rangle_\psi = \operatorname{Re}\, \langle \psi | M | \psi \rangle .$$(1)^✦

Pauli Observables

The Pauli matrices are the complex $2 \times 2$ matrices $$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}.$$(2) For a real vector $\vec n$ in three dimensions with components $n_1$, $n_2$ and $n_3$, the matrix $\vec n \cdot \vec\sigma$ is the complex $2 \times 2$ matrix $$\vec n \cdot \vec\sigma = n_1 X + n_2 Y + n_3 Z .$$(3)^✦ The Pauli observable along $\vec n$ is the observable on the qubit whose operator is the matrix (3), acting on $\mathbb{C}^2$.^✦

The Claim

The library states an identity for the square of the CHSH operator, on any two quantum systems and for observables that square to the identity operator. In it $[M, N] = MN - NM$ is the commutator of two observables on one system.

For Pauli observables along unit vectors it states the bound, in any pure state of a pair of qubits.

What Is Checked

The first claim is stated over observables on two quantum systems and their tensor products, observables on the composite system. The second is stated over the Pauli observables on the qubit, built from the Pauli matrices (2), and over the expectation values (1) of their tensor products in a pure state of a pair of qubits.

About these constructions the library proves two facts. The tensor product of two self adjoint operators is self adjoint, so that $M \otimes N$ is an observable on $A \otimes B$. The matrix $\vec n \cdot \vec\sigma$ is Hermitian for every real vector $\vec n$, so that the Pauli observable along $\vec n$ is an observable on the qubit.