The Exercise

A qubit is in an arbitrary state $|\psi\rangle$, to be carried into a code: a system $C$ with an encoder $E$ that takes each state of the qubit to its encoded form. The encoding is done by teleportation. One prepares the Bell pair $(|00\rangle + |11\rangle)/\sqrt{2}$ and applies the encoder to its second qubit alone; then $|\psi\rangle$ and the first qubit of the pair are measured in the Bell basis, with two bits $x$ and $y$ as the outcome. The exercise is to show that the code system is left in the encoded state $E|\psi\rangle$ up to a Pauli operation, fixed by $x$ and $y$, applied to $|\psi\rangle$ before the encoder.

The library states the identity on which this protocol rests, an expansion of the joint vector of the three systems in the Bell basis of the two measured qubits.

Systems and States

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ The composite system $S \otimes T$ of two systems $S$ and $T$ has for its state space the tensor product of their state spaces.^✦ The qubit $Q$ is the quantum system with state space $\mathbb{C}^2$.^✦

A pure state $|\psi\rangle$ of a system $S$ is a unit vector in the state space of $S$.^✦ For pure states $|\psi\rangle$ of $S$ and $|\varphi\rangle$ of $T$, the product state $|\psi\rangle|\varphi\rangle$ is the pure state of $S \otimes T$ whose vector is $|\psi\rangle \otimes |\varphi\rangle$.^✦ For a bit $i \in \{0,1\}$, the basis state $|i\rangle$ of the qubit is the pure state whose vector is the standard basis vector $e_i$ of $\mathbb{C}^2$.^✦

For bits $x$ and $y$, the Bell vector $|\beta_{xy}\rangle$ is the vector in the state space of $Q \otimes Q$ given by $$|\beta_{xy}\rangle = \frac{1}{\sqrt{2}}\bigl(|0\rangle|y\rangle + (-1)^x\,|1\rangle|\bar y\rangle\bigr),$$(1)^✦ where $\bar y = y + 1 \bmod 2$ is the flip of $y$. The pair of the exercise is $|\beta_{00}\rangle$.

An identification of two systems $S$ and $T$ is a linear isometric bijection from the state space of $S$ onto that of $T$, along which the two are regarded as one system.^✦ For three systems $A$, $B$ and $C$, the regrouping $\alpha$ is the identification of $A \otimes (B \otimes C)$ with $(A \otimes B) \otimes C$ that sends $|u\rangle \otimes (|v\rangle \otimes |w\rangle)$, for vectors $|u\rangle$, $|v\rangle$, $|w\rangle$ in the state spaces of $A$, $B$, $C$, to $$\alpha\bigl(|u\rangle \otimes (|v\rangle \otimes |w\rangle)\bigr) = (|u\rangle \otimes |v\rangle) \otimes |w\rangle.$$(2)^✦

The Encoded Resource

Let $C$ be a quantum system, the code system, and $E$ a linear map from the state space of $Q$ to that of $C$, the encoder. The unnormalised encoded resource $|\tilde\Phi_E\rangle$ of $E$ is the vector in the state space of $Q \otimes C$ given by $$|\tilde\Phi_E\rangle = |0\rangle \otimes E|0\rangle + |1\rangle \otimes E|1\rangle,$$(3)^✦ and the partially encoded resource $|\Phi_E\rangle$ of $E$ is the vector in the state space of $Q \otimes C$ obtained by rescaling $|\tilde\Phi_E\rangle$, $$|\Phi_E\rangle = \frac{1}{\sqrt{2}}\,|\tilde\Phi_E\rangle.$$(4)

Pauli Byproducts

A unitary $U$ of a system $S$ is an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$.^✦ The identity unitary of $S$ is the one whose operator is $1$^✦, and for unitaries $U$ and $V$ of $S$ the composite $UV$, first $V$ and then $U$, is again a unitary of $S$.^✦

The Pauli matrices are $$X = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \qquad Z = \begin{pmatrix} 1 & 0 \\ 0 & -1 \end{pmatrix}.$$(5) The Pauli gates $X$, the bit flip, and $Z$, the phase flip, are the unitaries of the qubit whose operators have these matrices. For bits $x$ and $y$, the Pauli byproduct $X^y Z^x$ is the unitary of the qubit that applies $Z^x$ and then $X^y$, where $Z^1 = Z$, $X^1 = X$, and $Z^0$ and $X^0$ are the identity unitary.^✦

The Claim

What Is Checked

The claim is stated over the qubit and an arbitrary code system $C$ with its encoder $E$: the regrouping (2) of the three systems, the Bell vectors (1), the partially encoded resource (4) and the Pauli byproducts $X^y Z^x$.

About these constructions the library proves that the matrices (5) are unitary, so that the Pauli gates are unitaries of the qubit, and that a composite of unitaries is a unitary, so that each byproduct is one. It proves as well that each basis state $|i\rangle$ is a unit vector and that a product of pure states is again a pure state, the norm of a product vector being the product of the norms.