Providing a more complete proof on why moving surface code qubits works

Question

A prior Q&A by Jellybean and Lior is instructive on why moving qubits in the surface code works via the hole-based method described in Fowler et al. I'm hoping for more details in why not only the logical operations can transfer, but also that the logical states are preserved, even after the $M_X$ measurement.

Namely, suppose we have some double defect Z qubit in a quiescent state $| \psi \rangle$ with three stabilizers of interest: $Z_0$ is the top stabilizer, $Z_1$ is the middle stabilizer, and $Z_2$ is the new stabilizer to move the hole to. Call the state post $M_X$ and $Z_1$ measured stabilizer to be $| \psi' \rangle$.

To demonstrate that the movement worked, it seems we must show that $\langle \psi' | Z_2 | \psi' \rangle = \langle \psi | Z_1 | \psi \rangle$, i.e. measuring the qubit would still retain the logical information (with some +/- factors depending on our intermediate phases). However, this equality seems non-trivial to prove -- so, how do we demonstrate the logical information is not only preserved but also extractable via simple $Z_2$ stabilizer measurement?

Answer 1

I'm hoping for more details in why not only the logical operations can transfer but also that the logical states are preserved, even after the 𝑀𝑋 measurement

Showing that the logical operators are transfered shows that the logical states are preserved. Gates are defined by how they act on operators, this is the essence of the stabilizer formalism. In the Q&A that you refer to, it was shown that the three steps perform $Z_L \rightarrow Z_L$ and $X_L \rightarrow X_L$.

There is only one gate $U$ that performs $Z \rightarrow Z$ and $X \rightarrow X$. If we solve: \begin{align} U\lvert0\rangle &= \lvert0\rangle \\ U\lvert1\rangle &= \lvert1\rangle \\ U\lvert+\rangle &= \lvert+\rangle \\ U\lvert-\rangle &= \lvert-\rangle \end{align}

We will find that $U$ is the identity matrix. Therefore with the steps a), b) and c) shown in the figure an identity gate is implemented on the logical qubit. For more examples of understanding which gates a circuit performs using the stabilizer formalism see The Heisenberg Representation of Quantum Computers