ZX-Calculus: how to prove this simple equation between two very small circuits

Question

Short version:

How could I prove in ZX-calculus that these two diagrams are equal (up to a global phase), using axioms from this paper (Fig. 1) for example? Any intuition is welcome!

Long version:

I'm starting to learn about ZX-Calculus, and I wanted to try to see the different ways to perform a CZ gate (rotation of $\pi$ angle). And it appears that there are (at least) three different ways (sorry for the bad quality of the drawings):

Version 1:

Version 2: (note the minus sign on the bottom qubit)

Version 3:

Now, version 2 is very easy to derive from version 1 if we take the axiom (EU) of this paper (we will call this axiom (EU1)), and version 3 is also easy to derive from version 1 if we take the axiom (EU) of this paper (we will call this axiom (EU2)).

But I can't find how to go from version 2 to version 3 by using only the axioms in the first paper (including EU1), or the other way around. Basically, it should be enought to prove that these two diagrams are equal (and I made the computation: they are equal, up to a global phase):

Any idea how to prove the equality of these two diagrams with axioms only from the first paper for example? It seems super easy (just 1/2 nodes!)... but I can't make it... Any intuition is welcome!

Answer 1

Here is a screenshot of a possible proof:

You can ignore the scalars if you want. The idea is to:

1. disconnect the red node using the spider rule
2. turn it into a green node with a Hadamard node
3. decompose the hadamard gate
4. use the copy rule to get rid of the red node

The above proof uses the rule from the second paper. If you want to use the other rule, the process is pretty much the same, you would simply need to disconnect the red node using the spider rule between 3. and 4., before you can use the copy rule.

The signs before the angles can be swapped by applying the Hadamard gate at the bottom on both sides of the equation, and hence changing "$-\pi/2$-red node = $\pi/2$-green node" into "$-\pi/2$-green node = $\pi/2$-red node".

Answer 2

If all the angles in your diagram are multiples of $\pi/2$, you should use the rules from "A Simplified Stabilizer ZX-calculus" instead of the original rules in the paper you linked. But I'll work with them since it's what you asked.

Because you don't care about non-zero scalar factors (such as global phase), you can simplify the rules by dropping any disconnected regions. So, for example, this:

becomes this:

Which you can perhaps see would be useful for showing that your version 1 CZ is equivalent to your version 3. The simplified stabilizer calculus paper also proves this identity:

Which relates your version 1 to your version 2. Your various CZs are just transforming the Hadamard in the middle into different forms.

Anyways, your goal is to prove this:

Which I would call "S gate can be performed by injecting a $\sqrt{X}^\dagger |0\rangle$ state". The main thing you need to do is to translate the $\sqrt{X}^\dagger |0\rangle$ part into an equivalent $\sqrt{Z}|+\rangle$ part, i.e. turn that green leaf into a red leaf so that you can just merge it into the central red node.

In the simplified stabilizer calculus axioms paper, the only rule that involves a leaf with a $\pi/2$ angle is $EU^\prime$. And if you look at their proof of that axiom from the original axioms, it includes a proof of the $\pi/2$ color change:

After discarding all the disconnected pieces on the right hand side, you have the hard part of your proof. The rest is just spider fusion.