The Exercise

A Toffoli gate cannot be applied transversally to an encoded qubit, so a fault-tolerant version has to be built another way. Exercise 10.68, on page 488, takes the route of gate teleportation: prepare a special three-qubit ancilla offline, couple it to the data with CNOTs, measure the data qubits, and fix up the ancilla with Paulis and controlled gates chosen by the outcomes. The Toffoli is applied only once, during the preparation of the ancilla, where it can be checked before use. The exercise has two parts. Part (1) is a warm-up: swapping the data into a fresh block and applying a Toffoli there computes the Toffoli of the data. Part (2) is the real construction, given as a figure with an ancilla preparation box, three CNOTs, three measurements and a classically controlled correction, and the claim is that the whole circuit implements the Toffoli gate.

The library has no figure. It has the gates and states of the figure as definitions, and each part as an equation between states. These notes go through the definitions in the order the figure reads, then state the two equations.

Part (1): Swap, Then Toffoli

The register has two blocks of three qubits, the data on the left and a block prepared in $|000\rangle$ on the right. The circuit swaps the blocks and applies a Toffoli to the block that now holds the data, $$\mathrm{SwapToffoli} = (\mathrm{id} \otimes \mathrm{Toffoli}) \circ \mathrm{SWAP} ,$$(1)^✦ where $\mathrm{SWAP}$ exchanges the two three-qubit blocks. On a data state $\psi$ next to $|000\rangle$ it does what one expects: $$\mathrm{SwapToffoli}\,(\psi \otimes |000\rangle) = |000\rangle \otimes \mathrm{Toffoli}\,\psi .$$(2)^✦ The data state $\psi$ is any pure state of three qubits, not only a basis state.

The Ancilla

The resource for part (2) is the state the preparation circuit makes from $|000\rangle$: a Hadamard on each of the first two qubits, then a Toffoli, $$\mathrm{Prep} = \mathrm{Toffoli} \circ \bigl((H \otimes \mathrm{id}) \circ (\mathrm{id} \otimes (H \otimes \mathrm{id}))\bigr) ,$$(3) $$\Theta_T = \mathrm{Prep}\,|000\rangle .$$(4) This is the leftmost box of the figure, and the only place a Toffoli is applied.

Part (2): The Teleported Toffoli

The six qubits are laid side by side as the ancilla block $a_1 a_2 a_3$ followed by the data block $x y z$. The couplings act on pairs, one ancilla qubit with one data qubit, so the library first relabels the register into the three pairs $(a_1, x)$, $(a_2, y)$, $(a_3, z)$.^✦ That relabelling is the identification $\mathrm{R}$; no qubit moves, only the bracketing changes. On the paired register the couplings are three CNOTs. On the two control pairs the ancilla is the control and the data qubit is the target; on the target pair the roles are reversed, the data qubit controlling a flip of the ancilla, which is the upward arrow in the figure: $$\mathrm{Couple} = (\mathrm{CNOT} \otimes \mathrm{id}) \circ \bigl((\mathrm{id} \otimes (\mathrm{CNOT} \otimes \mathrm{id})) \circ (\mathrm{id} \otimes (\mathrm{id} \otimes \mathrm{CNOT}^{\mathrm{rev}}))\bigr) .$$(5)^✦ The state just before the measurements is the coupled register, $$\Psi_{\psi} = \mathrm{Couple}\,\mathrm{R}(\Theta_T \otimes \psi) .$$(6)^✦

Then the three data qubits are measured, $x$ and $y$ in the $Z$ basis and $z$ in the $X$ basis, with outcomes $m_1, m_2, m_3$. The library packages the three as one measurement $\mathcal{M}$ of the paired register with outcomes in $\{0,1\}^3$, acting on the data qubit of each pair and leaving the ancilla qubits untouched.^✦ Writing $\mathcal{M}_{m_1, m_2, m_3}(\rho)$ for the state after the outcome $(m_1, m_2, m_3)$, defined when that outcome has non-zero probability, the ancilla block carries the Toffoli of the data up to a known Pauli byproduct, and the byproduct is removed by a correction chosen from the outcomes. The correction is exactly where Exercise 10.67 is used: moving the Toffoli left past the byproducts $X_1^{m_1}$, $X_2^{m_2}$ and $Z_3^{m_3}$ deposits the CNOTs and the controlled-$Z$ of that exercise, and $B^{\dagger}_{m_1 m_2 m_3}$ undoes them, $$B^{\dagger}_{m_1 m_2 m_3} = \mathrm{CZ}_{12}^{m_3} \circ \bigl((\mathrm{id} \otimes (\mathrm{id} \otimes Z))^{m_3} \circ B^{\dagger}_{m_1 m_2}\bigr) ,$$(7) where $U^{m}$ means $U$ if the bit $m$ is $1$ and nothing if it is $0$, and $B^{\dagger}_{m_1 m_2}$ is the part driven by the two control outcomes: an $X$ on each control whose outcome was $1$, with the CNOT that rule (a) of Exercise 10.67 attaches to it.

The claim of part (2) is that after the correction the ancilla block is in the state $\mathrm{Toffoli}\,\psi$, whatever the input and whatever the outcome. In the library the corrected state is reshaped back from pairs to blocks with $\mathrm{R}^{-1}$, the correction is applied to the ancilla block, and the data block is traced out: $$\operatorname{Tr}_{2}\Bigl(\bigl(B^{\dagger}_{m_1 m_2 m_3} \otimes \mathrm{id}\bigr)\, \mathrm{R}^{-1}\bigl(\mathcal{M}_{m_1, m_2, m_3}(|\Psi_{\psi}\rangle\langle\Psi_{\psi}|)\bigr)\, \bigl(B^{\dagger}_{m_1 m_2 m_3} \otimes \mathrm{id}\bigr)^{\dagger}\Bigr) = |\mathrm{Toffoli}\,\psi\rangle\langle\mathrm{Toffoli}\,\psi| ,$$(8)^✦ for every three-qubit pure state $\psi$ and every outcome $(m_1, m_2, m_3)$ with $p_{\mathcal{M}}(m_1, m_2, m_3 \mid |\Psi_\psi\rangle\langle\Psi_\psi|) \ne 0$.

What Is Checked

Lean has checked that every definition above elaborates on the six-qubit register, that the measurement is a measurement, with its operators summing to the identity, that the post-measurement state is a state whenever its outcome is possible, and that both claims are well typed. It has checked nothing about a proof, since there is none. What it cannot check is that these definitions are the figure on page 488: that the three CNOTs are drawn the way the library writes them, that the measurements are in the bases the figure marks, and that the correction boxes are the gates $B^{\dagger}_{m}$ above. Each of those is one named definition with its own drawing on this page, which is the material for that judgement.