The Exercise

The Hadamard gate acts on a single qubit by the matrix $$H = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix}$$(1)^✦ in the computational basis. Exercise 2.53 asks for its eigenvalues and eigenvectors.

The library states the answer for the Hadamard gate regarded as an observable of a single qubit, with an explicit eigenvector for each eigenvalue.

A Quantum System

A quantum system $S$ is a physical system whose state space is a finite dimensional complex Hilbert space.^✦ The qubit is the two level system whose state space is $\mathbb{C}^2$ itself.^✦ A pure state $|\psi\rangle$ of $S$ is a unit vector in the state space of $S$, $\lVert |\psi\rangle \rVert = 1$.^✦ The normalization of a nonzero vector $|v\rangle$ in the state space of $S$ is the pure state $|v\rangle / \lVert |v\rangle \rVert$ of $S$.^✦

An observable $A$ of $S$ is a self adjoint operator on the state space of $S$, $A^\dagger = A$.^✦ A pure state $|\psi\rangle$ of $S$ is an eigenstate of $A$ with eigenvalue $\mu$, a real number, when $$A|\psi\rangle = \mu |\psi\rangle .$$(2)^✦

The Hadamard Observable

The Hadamard observable $H$ is the observable of the qubit that acts on $\mathbb{C}^2$ by the matrix (1).^✦ Its eigenstates are written with the two vectors $$|v_+\rangle = \begin{pmatrix} 1 \\ \sqrt{2} - 1 \end{pmatrix}, \qquad |v_-\rangle = \begin{pmatrix} \sqrt{2} - 1 \\ -1 \end{pmatrix}$$(3) of $\mathbb{C}^2$. The pure states $|h_+\rangle$ and $|h_-\rangle$ of the qubit are the normalizations of $|v_+\rangle$ and $|v_-\rangle$.

The Claim

What Is Checked

The claim is stated over the Hadamard observable $H$ of the qubit, with the matrix (1), and over the two pure states $|h_\pm\rangle$ normalized from the vectors (3).

The library proves of these constructions that $|v_+\rangle$ and $|v_-\rangle$ are nonzero vectors, so that each has a normalization.