The Exercise

In BB84, the key distribution protocol of Bennett and Brassard, Alice encodes a bit $a$ in a qubit, in one of two bases chosen by a second bit $b$: the computational basis $\{\lvert 0\rangle, \lvert 1\rangle\}$ for $b = 0$, and for $b = 1$ the basis $\{\lvert +\rangle, \lvert -\rangle\}$ of eigenvectors of the Pauli operator $X$. Bob, who does not know $b$, measures the qubit in a basis $b'$ of his own choosing and obtains a bit $a'$. The exercise asks what $a'$ says about $a$ when the qubit reaches him unchanged. If $b' = b$, then $a' = a$ with certainty.^✦ If $b' \neq b$, then $a'$ is equally likely to be $0$ or $1$^✦, and it is uncorrelated with $a$.^✦

A Qubit and Its Measurements

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ Every finite dimensional complex Hilbert space is the state space of a system^✦, and the qubit is the system whose state space is $\mathbb{C}^2$.^✦

A state $\rho$ of $S$ is a positive operator of unit trace on the state space of $S$.^✦ A pure state $\psi$ of $S$ is a unit vector $\lvert\psi\rangle$ in the state space of $S$^✦; it determines the state $\lvert\psi\rangle\langle\psi\rvert$ of $S$, the projector onto $\lvert\psi\rangle$.^✦

A measurement $M$ on $S$ with a finite set of outcomes is a family of operators $M_i$ on the state space of $S$, one for each outcome $i$, satisfying the completeness relation $$\sum_i M_i^\dagger M_i = 1 .$$(1)^✦ The operators $E_i = M_i^\dagger M_i$ are the effects of the positive operator valued measure (POVM) of $M$.^✦ When $M$ is performed on a state $\rho$, the outcome $i$ occurs with the probability given by the Born rule, $$p_M(i \mid \rho) = \operatorname{Tr}(M_i \rho M_i^\dagger) = \operatorname{Tr}(E_i \rho) .$$(2)^✦

An observable $A$ on $S$ is a self adjoint operator on the state space of $S$.^✦ From it come the operators $$P_\pm = \tfrac{1}{2}(1 \pm A) ,$$(3) which, when $A^2 = 1$, are the projectors onto the eigenspaces of $A$ for the eigenvalues $+1$ and $-1$. For such an $A$, the sign measurement of $A$ is the measurement with two outcomes whose operators are $M_0 = P_+$ and $M_1 = P_-$, the outcome $0$ standing for the eigenvalue $+1$ and the outcome $1$ for $-1$: the projective measurement of $A$.^✦

The Pauli matrices are $$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \quad Y = \begin{pmatrix} 0 & -i \\ i & 0 \end{pmatrix}, \quad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix},$$(4) and for a real vector $\vec{n} = (n_x, n_y, n_z)$ in three dimensions, with the Pauli vector $\vec{\sigma} = (X, Y, Z)$, we write $\vec{n} \cdot \vec{\sigma} = n_x X + n_y Y + n_z Z$. The Pauli observable $\vec{n} \cdot \vec{\sigma}$ is this operator regarded as an observable on the qubit.^✦ The unit vectors $\hat{x} = (1, 0, 0)$ and $\hat{z} = (0, 0, 1)$ give the observables $X$ and $Z$.

The basis kets of $\mathbb{C}^2$ are the columns $\lvert 0\rangle = (1, 0)$ and $\lvert 1\rangle = (0, 1)$^✦, and the eigenvectors of $X$ for the eigenvalues $+1$ and $-1$ are $$\lvert\pm\rangle = \Bigl(\tfrac{1}{\sqrt{2}}, \pm\tfrac{1}{\sqrt{2}}\Bigr) = \tfrac{1}{\sqrt{2}}\bigl(\lvert 0\rangle \pm \lvert 1\rangle\bigr) .$$(5) For a bit $i$, the basis state $\lvert i\rangle$ of the qubit is the pure state whose vector is the ket $\lvert i\rangle$^✦, and the states $\lvert +\rangle$ and $\lvert -\rangle$ are the pure states whose vectors are (5).

Alice’s States and Bob’s Measurements

For bits $a$ and $b$, Alice’s state $\lvert\psi_{ab}\rangle$ is the pure state of the qubit given by $$\lvert\psi_{00}\rangle = \lvert 0\rangle, \quad \lvert\psi_{10}\rangle = \lvert 1\rangle, \quad \lvert\psi_{01}\rangle = \lvert +\rangle, \quad \lvert\psi_{11}\rangle = \lvert -\rangle .$$(6)^✦

Bob’s basis observable $O_{b'}$ is $Z$ for $b' = 0$ and $X$ for $b' = 1$.^✦ His measurement $M^{(b')}$ in the basis $b'$ is the sign measurement of $O_{b'}$, and its outcome is his bit $a'$.^✦ We write $$p_{b'}(j \mid a, b) = p_{M^{(b')}}\bigl(j \mid \lvert\psi_{ab}\rangle\langle\psi_{ab}\rvert\bigr)$$(7) for the probability that Bob obtains the bit $j$ in the basis $b'$ when Alice has prepared $\lvert\psi_{ab}\rangle$, where $a$, $b$, $b'$ and $j$ are bits.

The Claim

What Is Checked

The claim is stated over Alice’s states (6) and Bob’s measurements $M^{(b')}$, through the Born rule (2).

The library proves that both basis observables square to the identity, $O_{b'}^2 = 1$, so that each $M^{(b')}$ is a sign measurement as defined above. It proves that the vectors of Alice’s four states have unit norm and that the projector onto a unit vector is a density operator, which makes each $\lvert\psi_{ab}\rangle\langle\psi_{ab}\rvert$ a state. The matrix $\vec{n} \cdot \vec{\sigma}$ is Hermitian, so every Pauli observable is self adjoint.