The Exercise

Figure 4.9 of the book draws a circuit on three qubits made of sixteen gates: two Hadamards on the target wire, six CNOTs, seven gates $T$ or $T^\dagger$, and one $S$. Exercise 4.24, on page 182, asks the reader to verify that this circuit is the Toffoli gate. The point of the figure is that the Toffoli gate, which is not in the standard set, can be assembled from gates that are, and the Toffoli gate in turn gives universal classical computation on a quantum computer.

The library has no figure. It has the circuit as a term, cut into two blocks the way the figure reads, and the exercise as an equation between two unitaries. These notes write out the gates, the two blocks and the equation.

Gates and Wires

Four single-qubit gates occur. The Hadamard $H$ and the Pauli $X$ are the usual ones. The others are phase gates: the library has one definition $P(\alpha)$, the unitary that leaves $|0\rangle$ alone and multiplies $|1\rangle$ by $e^{i\alpha}$, and the book’s gates are three values of it, $$T := P(\pi/4), \qquad S := P(\pi/2), \qquad T^{\dagger} := P(-\pi/4) .$$(1)^✦

The register is $\mathrm{qubit} \otimes (\mathrm{qubit} \otimes \mathrm{qubit})$, bracketed to the right, and a gate sits on a wire by being tensored with the identity on the others. We write the wire as a subscript, so the gates on this register are $$\begin{aligned}T_1 &:= T \otimes \mathrm{id}, & T_2 &:= \mathrm{id} \otimes (T \otimes \mathrm{id}), & T_3 &:= \mathrm{id} \otimes (\mathrm{id} \otimes T), \\ T^{\dagger}_2 &:= \mathrm{id} \otimes (T^{\dagger} \otimes \mathrm{id}), & T^{\dagger}_3 &:= \mathrm{id} \otimes (\mathrm{id} \otimes T^{\dagger}), & S_2 &:= \mathrm{id} \otimes (S \otimes \mathrm{id}), \\ H_3 &:= \mathrm{id} \otimes (\mathrm{id} \otimes H) .\end{aligned}$$(2) A CNOT is the controlled $X$, written $C(U)$ for the gate $U$ controlled by the first qubit, and which two wires it joins is again read off the tensor structure, $$\mathrm{CNOT}_{12} := C(X \otimes \mathrm{id}), \qquad \mathrm{CNOT}_{13} := C(\mathrm{id} \otimes X), \qquad \mathrm{CNOT}_{23} := \mathrm{id} \otimes \mathrm{CNOT} .$$(3) Composition is written $U \circ V$ and means $V$ first, then $U$, so in a chain the rightmost gate acts first, the opposite of reading the figure from left to right.^✦

The Two Blocks

The figure splits naturally at the Hadamards. Between them lie eight gates, all on the target wire or ending on it, $$Q = T_3 \circ \mathrm{CNOT}_{13} \circ T^{\dagger}_3 \circ \mathrm{CNOT}_{23} \circ T_3 \circ \mathrm{CNOT}_{13} \circ T^{\dagger}_3 \circ \mathrm{CNOT}_{23} ,$$(4)^✦ read right to left: a CNOT from the second control, a $T^\dagger$, a CNOT from the first control, a $T$, and the same four once more. After the second Hadamard come six gates on the two control wires alone, $$P = S_2 \circ T_1 \circ \mathrm{CNOT}_{12} \circ T^{\dagger}_2 \circ \mathrm{CNOT}_{12} \circ T^{\dagger}_2 .$$(5)^✦ This block never touches the target; its job is to put the right relative phases on the controls.

The Circuit

The whole figure is a Hadamard on the target, the block $Q$, a second Hadamard on the target, then the block $P$: $$\mathrm{Fig}_{49} = P \circ H_3 \circ Q \circ H_3 .$$(6)^✦ Only $H$, $S$, $T$ and CNOT occur in it, which is what the construction is for.

The Claim

The exercise is the statement that this unitary is the Toffoli gate, $$\mathrm{Fig}_{49} = \mathrm{Toffoli} ,$$(7)^✦= where $\mathrm{Toffoli} = C^2(X)$ flips the third qubit exactly when the first two are both $|1\rangle$. The standard way to see it is to follow a basis state $|q_1 q_2 q_3\rangle$ through the circuit and collect the phases: the Hadamards turn a phase flip of the target into a bit flip, $Q$ supplies the phase $(-1)^{q_1 q_2}$ on the target up to a phase on the controls, and $P$ removes that leftover. The library does not contain this calculation.

What Is Checked

Lean has checked that the two blocks and the circuit are well-typed unitaries on the three-qubit register, built from the phase gate, the Hadamard, the controlled gates and the wire placements above, and that the equation is well typed. It has checked nothing about a proof, since there is none. The subscripted names on this page are the page’s own notation, declared in the displays with $:=$; the matcher unfolds them before it compares a formula with the Lean term, so a wrong wire in one of them would break the certification of every formula that uses it. What it cannot check is that the term is the figure on page 182: that the sixteen gates are in the book’s order and on the book’s wires. The two block definitions and the circuit each carry a drawing derived from the term, which is the material for that judgement.