The Exercise

Exercise 10.67, on page 487, shows two circuit diagrams and asks the reader to verify them. In the first, a Pauli $X$ sits on the top control line just before a Toffoli gate. The claim is that the same thing happens if the Toffoli acts first and is followed by an $X$ on that control together with a CNOT from the second control onto the target. In the second, a $Z$ sits on the target line before the Toffoli, and the claim is that this equals the Toffoli followed by a $Z$ on the target and a controlled-$Z$ between the two controls.

These are the rules for pushing a Pauli error through a Toffoli, and the book uses them in the fault-tolerant constructions of Section 10.6: an error that arrives before the gate comes out the other side as a known pattern of Paulis and controlled gates, which can be corrected. There are no diagrams in the library. Each identity is an equation between two gates on three qubits, and these notes write the equations out.

Gates on Three Qubits

A qubit is the two-level system, and three qubits form the composite $\mathrm{qubit} \otimes (\mathrm{qubit} \otimes \mathrm{qubit})$, bracketed to the right. A gate is a unitary on the whole register.^✦ Composition is written $U \circ V$ and means $V$ first, then $U$, the operator product $UV$; in a chain the rightmost gate acts first, the opposite of reading a drawn circuit from left to right.^✦ A single-qubit gate $G$ is put on the first wire as $G \otimes \mathrm{id}$, the identity on the other two, and on the third wire as $\mathrm{id} \otimes (\mathrm{id} \otimes G)$. Which wire a gate sits on is read off its position in the tensor product.

The controlled gate $C(U)$ acts on a qubit and a system: it does nothing when the control is $|0\rangle$ and applies $U$ when it is $|1\rangle$.^✦ The control is always the first factor. Controlling twice gives the doubly controlled gate on three qubits, $$C^{2}(U) = C\bigl(C(U)\bigr) ,$$(1)^✦ with the outer control on the first qubit and the inner one on the second. The Toffoli is the doubly controlled NOT, $$\mathrm{Toffoli} = C^{2}(X) ,$$(2)^✦ flipping the third qubit exactly when the first two are both $|1\rangle$. The CNOT is the singly controlled NOT, $$\mathrm{CNOT} = C(X) .$$(3)^✦ The book’s second identity needs a controlled-$Z$ between the first two qubits of the register with the third left alone. The library defines it as a controlled gate whose target is $Z$ on the second qubit, $$\mathrm{CZ}_{12} = C(Z \otimes \mathrm{id}) ,$$(4)^✦ which on a basis state is the sign $(-1)^{q_1 q_2}$.

The Identities

An $X$ on the first control, followed by the Toffoli, equals the Toffoli followed by a CNOT from the second control to the target and then the $X$: $$\mathrm{Toffoli} \circ (X \otimes \mathrm{id}) = (X \otimes \mathrm{id}) \circ (\mathrm{id} \otimes \mathrm{CNOT}) \circ \mathrm{Toffoli} .$$(5)^✦=

A $Z$ on the target, followed by the Toffoli, equals the Toffoli followed by a controlled-$Z$ on the two controls and then the $Z$: $$\mathrm{Toffoli} \circ \bigl(\mathrm{id} \otimes (\mathrm{id} \otimes Z)\bigr) = \bigl(\mathrm{id} \otimes (\mathrm{id} \otimes Z)\bigr) \circ \mathrm{CZ}_{12} \circ \mathrm{Toffoli} .$$(6)^✦=

What Is Checked

Lean has checked that both equations are well typed: the two sides are gates on the same three-qubit register, built from the controlled gates, the Paulis and the placements defined above, and each of those definitions elaborates. It has checked nothing about a proof, since there is none. What it cannot check is that the equations are the book’s diagrams. The library has no diagrams; the formalisers read Figure 10.67 and wrote these terms, and whether, for instance, $\mathrm{CZ}_{12}$ is the controlled-$Z$ the drawing shows is a judgement for the reader, made easier by the fact that every gate here is one named definition.