The Exercise

A single photon is shared between two optical modes. Each mode holds either no photon or one, so each is a two level system, with $|0\rangle$ an empty mode and $|1\rangle$ a mode holding the photon. The pair carries one logical qubit in the choice of mode: the logical zero $|0_L\rangle$ has the photon in the second mode and the logical one $|1_L\rangle$ has it in the first. This is the dual rail representation of a qubit. A phase shifter of angle $\pi$ is placed on the second mode, and the exercise asks what it does to a general superposition of the two logical states.

A Quantum System

A quantum system $S$ is a physical object whose state space is a finite dimensional complex Hilbert space.^✦ A pure state $|\psi\rangle$ of $S$ is a vector of unit norm in the state space of $S$, $\lVert \psi \rVert = 1$, determined physically up to a global phase.^✦

A finite dimensional complex Hilbert space $H$ given in advance is the state space of a quantum system, the system with state space $H$.^✦ The qubit is the two level system obtained this way from $\mathbb{C}^2$.^✦ For a bit $i$, 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$; $|0\rangle$ and $|1\rangle$ are the computational basis states.^✦

The composite system $S \otimes T$ of two quantum systems $S$ and $T$ is the quantum system whose state space is the tensor product of the state spaces of $S$ and $T$.^✦ For pure states $|\psi\rangle$ of $S$ and $|\varphi\rangle$ of $T$, the product $|\psi\rangle \otimes |\varphi\rangle$ is the pure state of $S \otimes T$ whose vector is the tensor product of the two vectors.^✦ The two modes form the composite system of two qubits, and $|ij\rangle$ stands for $|i\rangle \otimes |j\rangle$.

The Dual Rail Qubit

The logical zero and the logical one are product states of two qubits: $$|0_L\rangle = |0\rangle \otimes |1\rangle = |01\rangle , \qquad |1_L\rangle = |1\rangle \otimes |0\rangle = |10\rangle .$$(1) For any complex amplitudes $c_0$ and $c_1$, the dual rail vector is $c_0 |0_L\rangle + c_1 |1_L\rangle$, a vector in the state space of two qubits.^✦ When $|c_0|^2 + |c_1|^2 = 1$, the dual rail state $|\psi(c_0, c_1)\rangle$ is the pure state of two qubits with this vector, $$|\psi(c_0, c_1)\rangle = c_0 |01\rangle + c_1 |10\rangle .$$(2)^✦

The Phase Shifter

A unitary $U$ of a quantum system $S$ is a closed system evolution of $S$: an operator on the state space of $S$ with $U^\dagger U = U U^\dagger = 1$.^✦ A unitary $U$ of $S$ carries a pure state $|\psi\rangle$ of $S$ to the pure state $U|\psi\rangle$ of $S$, whose vector is the vector of $|\psi\rangle$ acted on by $U$.^✦ The identity evolution of $S$ is the unitary whose operator is the identity $1$.^✦

For unitaries $U$ of $S$ and $V$ of $T$, the product unitary $U \otimes V$ is the unitary of $S \otimes T$ whose operator is the tensor product of the operators of $U$ and $V$.^✦ A gate on the last wire of $S \otimes T$ is a unitary of $S \otimes T$ of the form $1 \otimes V$, where $1$ is the identity evolution of $S$ and $V$ is a unitary of $T$.^✦

The phase gate $P(\alpha)$ with angle $\alpha$ is the unitary of the qubit that is diagonal in the computational basis, leaving $|0\rangle$ alone and multiplying $|1\rangle$ by the phase $e^{i\alpha}$: $$P(\alpha) = \begin{pmatrix} 1 & 0 \\ 0 & e^{i\alpha} \end{pmatrix} .$$(3)^✦

The phase gate $P(\pi)$ acts on the second mode, so the evolution of the two modes is the gate on the last wire of two qubits: $$U_\pi = 1 \otimes P(\pi) .$$(4)^✦

The Claim

What Is Checked

The claim is stated over the dual rail state (2), a pure state of the composite system of two qubits built from the logical states (1), and over the unitary (4), the phase gate (3) at angle $\pi$ on the second qubit, applied to that state as a closed system evolution.

The library proves that the vector $c_0 |01\rangle + c_1 |10\rangle$ has unit norm whenever $|c_0|^2 + |c_1|^2 = 1$, and that a product $|\psi\rangle \otimes |\varphi\rangle$ of pure states has unit norm, the norm of a product vector being the product of the norms. It proves that the phase gate is unitary, as a diagonal operator whose entries have unit modulus, and that the tensor product of two unitaries is unitary.