has to occur

ZX-Calculus Completeness]Completeness of the ZX-Calculus

E. Jeandel]Emmanuel Jeandel
Université de Lorraine, CNRS, Inria, LORIA, F 54000 Nancy, France

S. Perdrix]Simon Perdrix
Université de Lorraine, CNRS, Inria, LORIA, F 54000 Nancy, France

R. Vilmart]Renaud Vilmart
Université de Lorraine, CNRS, Inria, LORIA, F 54000 Nancy, France

The ZX-Calculus is a graphical language for diagrammatic reasoning in quantum mechanics and quantum information theory. It comes equipped with an equational presentation. We focus here on a very important property of the language: completeness, which roughly ensures the equational theory captures all of quantum mechanics. We first improve on the known-to-be-complete presentation for the so-called Clifford fragment of the language – a restriction that is not universal – by adding some axioms. Thanks to a system of back-and-forth translation between the ZX-Calculus and a third-party complete graphical language, we prove that the provided axiomatisation is complete for the first approximately universal fragment of the language, namely Clifford+T.

We then prove that the expressive power of this presentation, though aimed at achieving completeness for the aforementioned restriction, extends beyond Clifford+T, to a class of diagrams that we call linear with Clifford+T constants. We use another version of the third-party language – and an adapted system of back-and-forth translation – to complete the language for the ZX-Calculus as a whole, that is, with no restriction. We briefly discuss the added axioms, and finally, we provide a complete axiomatisation for an altered version of the language which involves an additional generator, making the presentation simpler.

§ INTRODUCTION

The ZX-Calculus is a powerful graphical language for quantum reasoning and quantum computing introduced by Bob Coecke and Ross Duncan [7].
The language comes with a way of interpreting any ZX-diagram as a matrix – called the standard interpretation. Two diagrams represent the same quantum evolution when they have the same standard interpretation. The language is also equipped with a set of axioms – transformation rules – which are sound, i.e. they preserve the standard interpretation. Their purpose is to explain how a diagram can be transformed into an equivalent one.

The ZX-calculus has several applications in quantum information processing [9] (e.g. measurement-based quantum computing  [16, 24, 18], quantum codes [14, 15, 10, 12], foundations [4, 13]), and can be used through the interactive theorem prover Quantomatic [28, 29]. However, the main obstacle to wider use of the ZX-calculus was the absence of a completeness result for a universal fragment of quantum mechanics – a restriction of the language that can be used to represent any quantum operator. Completeness would guarantee that, in this fragment, any true property is provable using the ZX-calculus. More precisely, the language would be complete if, given any two diagrams representing the same matrix, one could transform one diagram into the other using the axioms of the language.
Completeness is crucial,  it means in particular that all the fundamental properties of quantum mechanics are captured by the graphical rules.

The ZX-Calculus, as it was initially introduced, has been proved to be incomplete in general [34], and despite the necessary axioms that have since been identified [31, 27], the language remained incomplete. However, several fragments of the language have been proved to be complete (2 [2]; $\pi$-fragment [17]; single-qubit 4 [3]), but none of them are universal for quantum mechanics, even approximately. In particular all quantum algorithms expressible in these fragments are efficiently simulable on a classical computer.

We tackle this problem, and present here four main results:

* A complete axiomatisation for Clifford+T quantum mechanics

* A complete axiomatisation for the so-called linear diagrams with constants in Clifford+T

* A complete axiomatisation for unrestricted ZX-Calculus

* A complete axiomatisation for a version of (unrestricted) ZX-Calculus with additional generator

To do so, we are going to use another graphical language called the ZW-Calculus, based on the interactions of the GHZ and W states [8]. The two versions of the language we are going to exploit – denoted and – have been proven to be complete through the use of normal forms [21, 22].

Completeness for Clifford+T. The first completeness result will use the first version of the ZW-Calculus. However, its diagrams only represent matrices over $\mathbb{Z}$, and hence it is not approximately universal. We introduce the -calculus, a simple extension of the ZW-Calculus which remains  complete and in which any matrix over the dyadic rational numbers can be represented.
We then introduce two interpretations from the ZX-Calculus  to  the -Calculus and back. Thanks to these interpretations, we derive the completeness of the 4 of the ZX-Calculus from the completeness of the -Calculus. Notice that the interpretation of ZX-diagrams (which represent complex matrices)  into -diagrams (which represent dyadic rationals) requires a non trivial encoding.
Notice also that this approach provides a completion procedure. Roughly speaking each axiom of the -calculus generates an equation in the ZX-calculus: if this equation is not already provable using the existing axioms of the ZX-calculus one can treat this equality as an new axiom. A great part of the work has been to reduce all these equalities to only two additional axioms for the language.

Completeness for linear diagrams with constants in Clifford+T. We extend the result to a restriction of the ZX-Calculus that contains Clifford+T. In some axioms and derivations, it is customary to consider some parameters as variables. Such a derivation can then be seen as a uniform proof, i.e. a proof that is valid for any valuation of the variables in the diagrams. In linear diagrams, some angles are considered as variables, and some other are constant. The accepted parameters are then linear combinations of the variables and the constant angles. We show that any equation between two linear diagrams with constants in Clifford+T, that is sound for all valuations of its variables, is provable using the axioms of Clifford+T ZX-Calculus. This result proves very useful for the following results.

Completeness for unrestricted ZX-Calculus. To find a complete axiomatisation for the general ZX-Calculus, we use the same technique as for the Clifford+T completeness (back and forth interpretations), but this time using the -Calculus which is universal, i.e. its diagrams can represent any matrix over $\mathbb{C}$ with dimension a power of two. Again, the interpretation from to ZX provide a range of equations that the latter has to be able to prove. Most of them are derivable thanks to the previous result: the completeness for linear diagrams with constants in Clifford+T. The other ones lead to an additional axiom for the ZX-Calculus. This axiom is “non-linear”, in the sense that that the parameters on one side of the equality are related in a non-linear manner to those on the other side. This is necessary: the argument for incompleteness [34] can be adapted to any linear axiomatisation.

Completeness for ZX-Calculus with parametrised triangles. The proof of completeness for Clifford+T heavily relies on a particular Clifford+T diagram, which performs a non-trivial, non-unitary matrix
. To simplify the proofs, we gave it a syntactic sugar: !0.9emtriangle-node. In order to provide a simplified axiomatisation for universal quantum mechanics, we propose in the last section to add to the language a parametrised version of the triangle, motivated by the behaviour of said matrix
. The introduction of this generator greatly simplifies two axioms at the cost of an additional one: its decomposition.

Related works. After the result for Clifford+T came out, another axiomatisation was found for unrestricted ZX-Calculus [23], but for an altered version of the ZX-Calculus, that is, a version where two generators were added, namely the triangle – which we have introduced as a syntactic sugar for a diagram of Clifford+T – and the $\lambda$-box, used to simplify the translation from ZW to ZX. This axiomatisation was proven to be complete using the same method of back and forth interpretation with the -Calculus. It has a significantly higher amount of rules than the one we obtain for unrestricted ZX-Calculus.

This paper condenses two articles [25, 26], and extends them with the notion of parametrised triangle. It is structured as follows. Sections <ref> and <ref> present respectively the ZX-Calculi and the ZW-Calculi. Section <ref> is dedicated to the proof of completeness for Clifford+T, while Section <ref> extends the result to linear diagrams. Section <ref> provides methods to simplify the use of the latter result and Section <ref> makes use of them to show the provided axiomatisation for unrestricted ZX-Calculus is complete. We briefly discuss the axioms we have added so far in Section <ref>, and finally provide an alternative ZX-Calculus with parametrised triangles in Section <ref>.

§ THE ZX-CALCULUS

§.§ Syntax and Semantics

In the ZX-Calculus, quantum operators are represented as diagrams.
A ZX-diagram $D:k\to l$ with $k$ inputs and $l$ outputs is generated by:

$$R_Z^{(n,m)}(\alpha):n\to m\quad\boxed{\tikzfig{gn-alpha}} \qquad\qquad R_X^{(n,m)}(\alpha):n\to m\quad\boxed{\tikzfig{rn-alpha}}$$

$$H:1\to 1\quad\boxed{~~\tikzfig{Hadamard}~~}\qquad\qquad e:0\to 0 \quad\boxed{\phantom{\tikzfig{empty-diagram}}}\qquad\qquad\mathbb{I}:1\to 1\quad\boxed{~~\tikzfig{single-line}~~} \qquad\qquad\sigma:2\to 2\quad\boxed{\tikzfig{crossing}}$$

$$\epsilon:2\to 0\quad\boxed{\tikzfig{cup}}\qquad\qquad\eta:0\to 2\quad\boxed{\tikzfig{caps}}$$

and the two compositions:

* Spacial Composition: for any $D_1:a\to b$ and $D_2:c\to d$, $D_1\otimes D_2:a+c\to b+d$ consists in placing $D_1$ and $D_2$ side by side, $D_2$ on the right of $D_1$.

* Sequential Composition: for any $D_1:a\to b$ and $D_2:b\to c$, $D_2\circ D_1:a\to c$ consists in placing $D_1$ on the top of $D_2$, connecting the outputs of $D_1$ to the inputs of $D_2$.[
In order to be simpler, the present article eludes part of the underlying formalism (strict compact closed symmetric monoidal categories), which makes the language unambiguous. For more information, see e.g. [35].]

The standard interpretation of the ZX-diagrams associates to any diagram $D:n\to m$ a linear map $\interp{D}:\mathbb{C}^{2^n}\to\mathbb{C}^{2^m}$ inductively defined as follows:

\[ \interp{D_1\otimes D_2}:=\interp{D_1}\otimes\interp{D_2} \qquad
\interp{D_2\circ D_1}:=\interp{D_2}\circ\interp{D_1}\]

\[\interp{\tikzfig{empty-diagram}~}:=\begin{pmatrix}
\end{pmatrix} \qquad
\interp{~\tikzfig{single-line}~~}:= \begin{pmatrix}
1 & 0 \\ 0 & 1\end{pmatrix}\qquad
\interp{~\tikzfig{Hadamard}~}:= \frac{1}{\sqrt{2}}\begin{pmatrix}1 & 1\\1 & -1\end{pmatrix}\]

$$\interp{\tikzfig{crossing}}:= \begin{pmatrix}
\end{pmatrix} \qquad
\interp{\raisebox{-0.25em}{$\tikzfig{cup}$}}:= \begin{pmatrix}
\end{pmatrix} \qquad
\interp{\raisebox{-0.35em}{$\tikzfig{caps}$}}:= \begin{pmatrix}
\end{pmatrix}$$

For any $\alpha\in\mathbb{R}$, $\interp{\begin{tikzpicture}
\begin{pgfonlayer}{nodelayer}
\node [style=gn] (0) at (0, -0) {$\alpha$};
\end{pgfonlayer}
\end{tikzpicture}}:=\begin{pmatrix}1+e^{i\alpha}\end{pmatrix}$, and  for any $n,m\geq 0$ such that $n+m>0$:

%	\begin{pgfonlayer}{nodelayer}
%		\node [style=gn] (0) at (0, -0) {$\alpha$};
%	\end{pgfonlayer}
%\end{tikzpicture}}:=\begin{pmatrix}1+e^{i\alpha}\end{pmatrix} \qquad
\interp{\tikzfig{gn-alpha}}:=
\annoted{2^m}{2^n}{\begin{pmatrix}
1 & 0 & \cdots & 0 & 0 \\
0 & 0 & \cdots & 0 & 0 \\
\vdots & \vdots & \ddots & \vdots & \vdots \\
0 & 0 & \cdots & 0 & 0 \\
0 & 0 & \cdots & 0 & e^{i\alpha}
\end{pmatrix}}

$$\interp{\tikzfig{rn-alpha}}:=\interp{~\tikzfig{Hadamard}~}^{\otimes m}\circ \interp{\tikzfig{gn-alpha}}\circ \interp{~\tikzfig{Hadamard}~}^{\otimes n}$$

$\left(\text{where }M^{\otimes 0}=\begin{pmatrix}1\end{pmatrix}\text{ and }M^{\otimes k}=M\otimes M^{\otimes k-1}\text{ for any }k\in \mathbb{N}^*\right)$.

To simplify, the red and green nodes will be represented empty when holding a 0 angle:

\[ \tikzfig{gn-empty-is-gn-zero} \qquad\text{and}\qquad \tikzfig{rn-empty-is-rn-zero} \]

The ZX-Calculus is universal, i.e. for any complex matrix (with dimensions some powers of 2), there exists a diagram that represents it [7].

§.§ Fragments and Axiomatisations

The language comes equipped with an equational theory, or axiomatisation: a set of diagram transformations that can be applied locally while preserving the semantics.
When two diagrams $D_1$ and $D_2$ can be turned into one another using the rules of the ZX-Calculus, we will write $\zx\vdash D_1=D_2$. The fact that the rules can be applied locally is formalised by:

\[\zx\vdash D_1=D_2 \implies \left\lbrace \begin{array}{l}
\zx\vdash D_1\circ D = D_2\circ D\\
\zx\vdash D\circ D_1 = D\circ D_2\\
\zx\vdash D_1\otimes D = D_2\otimes D\\
\zx\vdash D\otimes D_1 = D\otimes D_2\\
\end{array}\right.\]

whenever $D$ has the right type.

Of course, the rules are chosen so that they are sound:

\[\zx\vdash D_1=D_2 \implies \interp{D_1}=\interp{D_2}\]

Completeness is the converse of soundness.

The property of completeness is essential: it implies that the language captures all the properties of quantum mechanics, and also that we can do as much with the graphical language as with matrices and linear algebra, for handling qubits.

The problem of completeness is hard to tackle, plus the parameters in the general ZX-Calculus can take their values in $\mathbb{R}$, which implies handling an uncountable set of angles. It can then be preferred to restrict the language to some finite set of values for the parameters, and study the completeness for these specific restrictions. Hence the ZX actually has several axiomatisations, each of them, while sharing some fundamental axioms, are devoted to specific fragments.

A set of fundamental axioms that are present in all axiomatisations of the qubit ZX-Calculus are the ones that fall under the paradigm “only topology matters” [7]. The language is such that any graph isomorphism (with fixed inputs and outputs) preserves the semantics, so we can bend the wires, and move nodes around as we please, so for instance we have the following equalities:

\[{\tikzfig{bent-wire}}\]

\[{\tikzfig{bent-wire-2}}\]

In the following we review some restrictions of the language, and their state-of-the-art axiomatisation.

§.§.§ Clifford

We call the Clifford fragment, or the 2 of the language, the restriction of ZX-Calculus where the nodes $R_Z$ and $R_X$ have their parameters in $\frac{\pi}{2}\mathbb{Z}$, i.e. when all the angles in the diagrams are multiples of $\frac{\pi}{2}$. This corresponds to the Clifford fragment of quantum circuits. It is a fragment of prime interest for it is used in error correction schemes [19], as well as a resource for computation in the model of measurement-based quantum computing [32]. However, the fragment is not universal i.e.  its diagrams cannot approach all quantum evolutions. It even has been shown that Clifford circuits and diagrams can be efficiently simulated by a classical computer [1]. However, an axiomatisation is known to be complete for the Clifford fragment of the ZX-Calculus [2], and is given in Figure <ref>. Notice that this axiomatisation is a simplified version of the original one [5] and that one could simplify further by removing the rule , which happens to be derivable from the others in the 2. However, since it is not derivable for arbitrary angles, it will be used in the next axiomatisations.

spider-1    s2-simple    inverse-label

b1s    b2s    k2s

euler-decomp-scalar-free     h2    ZO

[]Set of rules for the Clifford ZX-Calculus with scalars. All of these rules also hold when flipped upside-down, or with the colours red and green swapped. The right-hand side of (E) is an empty diagram. (...) denote zero or more wires, while (45-0.4em$\cdots$) denote one or more wires.

§.§.§ Real Stabiliser

A retriction of the Clifford fragment is the so-called real stabiliser, or the $\pi$-fragment, where all the angles are in $\pi\mathbb{Z}$. This fragment exactly represents graph states, and also has a complete axiomatisation [17].

§.§.§ Clifford+T

While the Clifford fragment is known to be efficiently simulable and not universal, it actually only needs a little boost to get there. Indeed, the $T$ gate, identified as $R_Z(\frac{\pi}{4})$ in the ZX-Calculus, is enough to bring approximate universality to the Clifford fragment [36]. This new restriction is called Clifford+T.

Although the axiomatisation for Clifford presented in Figure <ref> is enough to make the 1-qubit Clifford+T fragment complete [3], it is not enough to get the result for the many-qubit case. In particular, two equations of the 4 – and in the following – were shown to be unprovable [31, 27], and thus were added to the axiomatisation, but the question of the completeness of the resulting set of axioms remained an open problem. One of the main results of the present article is to provide an axiomatisation that builds on the previous one, and to show that it is complete for the fragment. The additional axioms for Clifford+T are given in Figure <ref>.

former-supp   bicolor_pi_4_eq_empty

commutation-of-controls-general-simplified   BW-simplified

[]Additional rules for the Clifford+T fragment. Together with $\zxc\setminus\{\iv,\zo\}$, they form the axiomatisation $\zxct$.

For any diagrams $D_1$ and $D_2$ of the 4 of the ZX-Calculus:

\[\interp{D_1}=\interp{D_2} \equi{} \zxct \vdash D_1=D_2\]

It is also to be noted that a complete axiomatisation has been proposed for the 2-qubit unitaries in Clifford+T [11], although the equality between some pairs of diagrams of the 4 can only be achieved by getting out of the fragment. That is, proving $D_1=D_2$ can sometimes only be achieved by proving $D_1=D_3=D_2$, but where $D_3$ is not in the fragment, and has angles that can even be irrational multiples of $\pi$.

§.§.§ Linear Diagrams

Linear diagrams are a restriction of the language that stand out from the other fragments, for they are not simply obtained by restricting the angles to be some multiples of a fraction of $\pi$.

In linear diagrams, some angles are considered as variables, and the accepted parameters in green and red nodes are affine combinations of those ($c+\sum n_i\alpha_i$ where $\alpha_i$ are variables and $c$ is constant). Two diagrams are supposed to be equal when they are equal for all valuations of said variables. More details will be provided in Section <ref>, but we are going to prove the completeness of linear diagrams with constants in $\frac{\pi}{4}\mathbb{Z}$, which will prove very useful for the next completeness result.

For any diagrams $D_1(\vec\alpha)$ and $D_2(\vec\alpha)$ linear in $\vec\alpha$ with constants in $\frac{\pi}{4}\mathbb{Z}$:

\[\forall \vec \alpha \in \mathbb R,~\interp{D_1(\vec\alpha)}=\interp{D_2(\vec\alpha)} \equi{} \forall \vec \alpha \in \mathbb R,~\zxct \vdash D_1(\vec\alpha)=D_2(\vec\alpha)\]

Then, Theorem <ref> for Clifford+T diagrams can be seen as a particular case of Theorem <ref>, where the number of variables is $0$.

§.§.§ General ZX-Calculus

Even though the axiomatisation $\zxct$ makes an approxiamtely universal fragment of the ZX-Calculus complete, we know that the said axiomatisation does not make the general ZX-Calculus complete. Indeed, an argument provided in [34] holds for all the axiomatisations we have provided thus far. However, the last main result of the paper shows that only one additional axiom is needed to get the property for the language with no restriction.

[]Additional rule for the general ZX-Calculus.

For any diagrams $D_1$ and $D_2$ of the ZX-Calculus:

\[\interp{D_1}=\interp{D_2} \equi{} \left(\zxct+\add\right) \vdash D_1=D_2\]

§.§.§ ZX-Calculus with Parametrised Triangles

This language, presented in Section <ref> shows an altered version of the ZX-Calculus, an additional generator with a parameter is introduced. It builds from the realisation that a particular diagram of the Clifford+T fragment proved so useful (and expressive) that it got a syntactic sugar: the so-called triangle. This node was introduced as a generator in [23] and later on in [37]. We propose here to make it even more expressive by giving it a parameter. This leads to a new complete axiomatisation for universal quantum computing.

§ THE ZW-CALCULI

The proofs of completeness provided in the following heavily rely on the completeness of a third-party language called the ZW-Calculus. It was introduced as the GHZ/W calculus by Coecke and Kissinger in [8], as a graphical language devoted to describing the interactions of the GHZ and W states, which constitute the only two classes of entanglement between three qubits, and has then been shown to be well suited for describing fermionic quantum computation.

It has been completed in [21], the diagrams allowing then to represent matrices over the integers $\mathbb{Z}$. We will denote this first version of the language , but we will not directly use it as it is. Instead, we will use a slightly altered version, that we denote , where it can represent any matrix over dyadic rationals. The language has then been extended to allow the completeness for matrices over any ring in [23], hence a fortiori, over $\mathbb{C}$. We will denote this last version of the language .

§.§ For Integer Matrices

We will present here the expanded version of the ZW-Calculus, i.e. the version where all the black and white nodes have a degree $\leq 3$. To stay consistent with the previous definition of the ZX-Calculus, we will assume that the diagrams are to be read from top to bottom. The ZW-Calculus has the following finite set of generators:

\[T_e=\left\lbrace
\tikzfig{Z-1-1}~,~\tikzfig{Z-2-1}~,~\tikzfig{W-1-1}~,~\tikzfig{W-1-2}~,\scalebox{1}{\tikzfig{single-line}}~,\raisebox{-0.3em}{\tikzfig{cup}}~,\raisebox{-0.4em}{\tikzfig{caps}}~,~\tikzfig{crossing}~,~\tikzfig{zw-cross}~,~\tikzfig{empty-diagram}~
\right\rbrace\]

and diagrams are created thanks to the same two – spacial and sequential – compositions as ZX.

As for the ZX-Calculus, we define a standard interpretation, that associates to any diagram of the ZW-Calculus $D$ with $n$ inputs and $m$ outputs, a linear map $\interp{D}:\mathbb{Z}^{2^n}\to\mathbb{Z}^{2^m}$, inductively defined as:

$$ \interp{D_1\otimes D_2}:=\interp{D_1}\otimes\interp{D_2} \qquad
\interp{D_2\circ D_1}:=\interp{D_2}\circ\interp{D_1}$$

$$\interp{\tikzfig{empty-diagram}~}:=\begin{pmatrix}1\end{pmatrix} \quad
\interp{~\tikzfig{single-line}~~}:= \begin{pmatrix}
1 & 0 \\ 0 & 1\end{pmatrix}\qquad
\interp{\raisebox{-0.4em}{$\tikzfig{caps}$}}:= \begin{pmatrix}
\end{pmatrix}\qquad
\interp{\raisebox{-0.3em}{$\tikzfig{cup}$}}:= \begin{pmatrix}
\end{pmatrix}$$

\interp{\tikzfig{crossing}}:= \begin{pmatrix}
\end{pmatrix} \qquad
\interp{\tikzfig{zw-cross}}:= \begin{pmatrix}
\end{pmatrix}\qquad
\interp{\tikzfig{W-1-1}}:= \begin{pmatrix}
\end{pmatrix}$$

\interp{\tikzfig{W-1-2}}:= \begin{pmatrix}
\end{pmatrix}\qquad
\interp{\tikzfig{Z-1-1}}:= \begin{pmatrix}
\end{pmatrix} \qquad
\interp{\tikzfig{Z-2-1}}:= \begin{pmatrix}
\end{pmatrix}

This map is obviously different from the one of the ZX-Calculus – the domain is different – but we will use the same notation.

ZW-Diagrams are universal for matrices of $\mathbb{Z}^{2^n}\times\mathbb{Z}^{2^m}$:

\[\forall A\in \mathbb{Z}^{2^n}\times\mathbb{Z}^{2^m},~~\exists D:n\to m,~~ \interp{D}=A\]

ZW-rule-0-no-param     $\quad$     ZW-rule-1-no-param

ZW-rule-2-no-param        ZW-rule-3-no-param

ZW-rule-4-no-param        ZW-rule-5-no-braid

3|c|ZW-rule-6-no-param $\qquad$ ZW-rule-X-no-braid

ZW-rule-7-no-param $\qquad$ reidmeister-3

Set of rules for the ZW-Calculus.

The ZW-Calculus comes with a complete set of rules ZW that is given in Figure <ref>.
Here again, the paradigm Only Topology Matters applies except for zw-cross. It gives sense to nodes that are not directly given in $T_e$, e.g.:

\[\tikzfig{zw-bent-wire-example}\]

For zw-cross, the order of inputs and outputs is important. However, it is invariant under cyclic permutations, as suggested by the shape of the node: zw-cross-cycle.

All these rules are sound. We use the same notation $\vdash$ as defined in section <ref>, and we can still apply the rewrite rules to subdiagrams.

In the following we may use the shortcuts:

black-dot-0-1 and white-dot-0-1

The main interest of this language is that it  has been proved to be complete.

For any two -diagrams $D_1$ and $D_2$:

\[\interp{D_1}=\interp{D_2} \iff \zw\vdash D_1=D_2\]

§.§ For Dyadic Matrices

We define an extension of the ZW-Calculus by adding a new node that represents the $1\times1$ matrix $\begin{pmatrix}\frac{1}{2}\end{pmatrix}$ and binding it to the calculus with an additional rule.

We define the -Calculus as the extension of the ZW-Calculus such as:

\[\left\lbrace
\begin{array}{l}
\zwh=\zw\cup\left\lbrace\tikzfig{additional-ZW-rule}~\right\rbrace
\end{array}
\right.\]

The standard interpretation of a diagram $D:n\to m$ is now a matrix
$\interp{D}:\mathbb{D}^{2^n}\to\mathbb{D}^{2^m}$ over the
ring $\mathbb{D} = \mathbb{Z}[1/2]$ of dyadic rationals and is given by
the standard interpretation of the ZW-Calculus extended with $\interp{\half}:=\begin{pmatrix}\frac{1}{2}\end{pmatrix}$.

The is sound and complete:
For two diagrams $D_1, D_2$ of the -Calculus,

\[\interp{D_1} = \interp{D_2}\iff\zwh \vdash D_1 = D_2\]

Soundness is obvious.

Now let $D_1$ and $D_2$ be two diagrams of the -Calculus such that $\interp{D_1}=\interp{D_2}$.
We can rewrite $D_1$ and $D_2$ as $D_i = d_i\otimes(\half)^{\otimes   n_i}$ for some integers $n_i$ and diagrams $d_i$ of the ZW-Calculus that do not use the $\half$ symbol.

From the new introduced rule, we get that  $\zwh\vdash d_i=D_i\otimes \left(\two\right)^{\otimes n_i}$. W.l.o.g. assume $n_1\leq n_2$. Then $\interp{d_1\otimes \left(\two\right)^{\otimes n_2-n_1}}=2^{n_2-n_1}\interp{d_1}=2^{n_2}\interp{D_1} = \interp{d_2}$. Since $d_1$ and $d_2$ are ZW-diagrams and have the same interpretation, thanks to the completeness of the ZW-Calculus, $\zwh\vdash d_1\otimes \left(\two\right)^{\otimes n_2-n_1}=d_2$, which means $\zwh\vdash D_1=D_2$ by applying $n_2$ times the new rule on both sides of the equality.

We can also precisely characterise the expressive power of this new extension.

-Diagrams are universal for matrices of $\mathbb{D}^{2^n}\times\mathbb{D}^{2^m}$:

\[\forall A\in \mathbb{D}^{2^n}\times\mathbb{D}^{2^m},~~\exists D\in \zwh,~~ \interp{D}=A\]

Let $A\in \mathbb{D}^{2^n}\times\mathbb{D}^{2^m}$. There exists $n\in\mathbb{N}$ and $A'\in \mathbb{Z}^{2^n}\times\mathbb{Z}^{2^m}$ such that $A=\frac{1}{2^n}A'$. By Lemma <ref>, there exists a ZW-diagram $D_{A'}$ such that $\interp{D_{A'}}=A'$. $D_{A'}$ is also a -diagram. Hence, we can define $D_A:=D_{A'}\otimes(\half)^{\otimes n}$ and $\interp{D_A} = \interp{\half}^n\interp{D_{A'}} = \frac{1}{2^n}A'=A$.

§.§ For Complex Matrices

The -Calculus [23] differs from the initial language in that the white nodes now bear a parameter: Z-param where $r$ is a complex number:

\[\interp{\tikzfig{Z-param}} := \annoted{2^m}{2^n}{\begin{pmatrix}
1 & 0 & \cdots & 0 & 0 \\
0 & 0 & \cdots & 0 & 0 \\
\vdots & \vdots & \ddots & \vdots & \vdots \\
0 & 0 & \cdots & 0 & 0 \\
0 & 0 & \cdots & 0 & r
\end{pmatrix}}\]

It is important to notice that the white node in the initial ZW-Calculus would now be represented by a white node with parameter $-1$. This more expressive language comes equipped with a complete set of axioms, some of which can already be found in the presentation of the ZW-Calculus. The axiomatisation is given in Figure <ref>.

For any two -diagrams $D_1$ and $D_2$:

\[\interp{D_1}=\interp{D_2} \iff \zwc\vdash D_1=D_2\]

ZW-rule-0-no-braid     $\quad$     ZW-rule-1

ZW-rule-2-no-braid        ZW-rule-3

ZW-rule-4        ZW-rule-5-no-braid

3|c|ZW-rule-6-no-braid $\qquad$ ZW-rule-X-no-braid

ZW-rule-7-no-braid $\qquad$ reidmeister-3

Set of rules for the -Calculus.

§ COMPLETENESS FOR CLIFFORD+T ZX-CALCULUS

This section is devoted to proving Theorem <ref>, that is, the completeness of the ZX-Calculus for the 4 when equipped with the rules $\zxct$. The proof method is the following:

* Provide an interpretation $[.]_W$ from the 4 of the ZX-Calculus to the -Calculus, where the semantics undergoes a well-defined homomorphism with left inverse.

* Provide an interpretation $[.]_X$ from the -Calculus to the 4 of the ZX-Calculus that respects the semantics.

* Prove that all the axioms of the -Calculus can be derived using $\zxct$ after application of $[.]_X$.

* Prove that any diagram $D$ of the 4 can be recovered from $\left[[D]_W\right]_X$.

§.§ Encoding the Clifford+T ZX-Calculus into ZW$\mathbf{_{\frac{1}{2}}}$

Our goal here is to send ZX-diagrams in the 4 into the -Calculus. The main obstacle is that the former represent matrices over $\mathbb{D}\left[\piq{}\right]$, while the latter only represent matrices over $\mathbb{D}$.

§.§.§ From ${\mathbb{Q}[\piq{}]}$ to ${\mathbb{Q}}$

All results used in the next two sections are standard in field
theory, see e.g. [33].
Let $R \subseteq \mathbb{C}$ be a (commutative) ring and $\alpha \in \mathbb{C}$.
By $R[\alpha]$ we denote the smallest subring of $\mathbb{C}$ that contains both $R$ and $\alpha$.

Of primary importance will be the ring $\mathbb{Q}[\piq{}]$, as all terms of the $\pi/4$ fragment of the ZX-Calculus have interpretations as matrices in this ring.
This is clear for all terms except possibly for $\sqrt{2}$, but $\sqrt{2} = \piq{} - \piq{3}$.

If $\alpha$ is algebraic, it is well known that $\mathbb{Q}[\alpha]$ is a field. When $F \subseteq F'$ are two fields, $F'$ can be seen as a vector space (actually an algebra) over $F$. Its dimension is denoted $[F':F]$ and we say that $F'$ is an extension of $F$ of degree $[F':F]$.
In the specific case of $\mathbb{Q}[\alpha]$, its dimension over $\mathbb{Q}$ is exactly the degree of the minimal polynomial over $\mathbb{Q}$ of $\alpha$.
Notice that the minimal polynomial of a $n-$th primitive root of the
unity is $\phi(n)$ where $\phi$ is Euler's totient function.

In our case, $\piq{}$ is a eighth primitive root of the unity, so that $\mathbb{Q}[\piq{}]$ is a vector space of dimension $4$, one basis being given by $1 ,\piq{},\piq2, \piq3$.
In particular:

Every element of $\mathbb{Q}[\piq{}]$ can be written in a unique way
$a + b \piq{} + c \piq{2} + d \piq{3}$ for some rationals numbers $a,b,c,d$.

For $x \in \mathbb{Q}[\piq{}]$, let $\psi(x)$ be the function defined by  $\psi(x) = y \mapsto x y$. For each $x$, $\psi(x)$ is a linear map and therefore can be given by a $4\times 4$ matrix in the basis $\{\piq3,\piq2, \piq{}, 1\}$.
$\psi(1)$ is of course the identity matrix and

\[
\psi(\piq{}) = M = \begin{pmatrix}
0 & 1 & 0 & 0 \\
0 & 0 & 1 & 0 \\
0 & 0 & 0 & 1 \\
-1 & 0 & 0 & 0 \\
\end{pmatrix}
\]

Notice that $M^t$ is the companion matrix of the polynomial $X^4+1$ which characterises $\piq{}$ as an algebraic number.

The map:

\[  \psi: a+b\piq{} +c\piq2 + d\piq3 \mapsto a I_4 + b M + c M^2 +d M ^3\]

is a  homomorphism of $\mathbb{Q}$-algebras from  $\mathbb{Q}[\piq{}]$ to $M_4(\mathbb{Q})$

This homomorphism has a left-inverse. Indeed, let

\[
\omega = \begin{pmatrix}
1 \\
\piq{} \\
\piq2 \\
\piq3 \\
\end{pmatrix}
\]

Then $\psi(x)\omega = x\omega$ for all $x\in \mathbb{Q}[\piq{}]$, so the left inverse of $\psi$ is given by $x\mapsto x\circ\omega$.

With this morphism, we can see elements of $\mathbb{Q}[\piq{}]$ as matrices over $\mathbb{Q}$.

Of course we can do the same with matrices over $\mathbb{Q}[\piq{}]$.

\[  \psi: A+B\piq{} +C\piq2 + D\piq3 \mapsto A\otimes  I_4 + B\otimes M + C\otimes M^2 +D\otimes M ^3\]

$\psi$ is injective and maps a matrix over $\mathbb{Q}[\piq{}]$ of dimension $n\times m$ to a matrix over $\mathbb{Q}$ of dimension $4n\times 4m$.

We use the same notation  $\psi$ as before, as the definitions are equivalent for one-by-one matrices (i.e. scalars).

It is easy to see that Proposition <ref> holds for the extended $\psi$ in the sense that $\psi(qA) = q\psi(A)$ for $q$ rational, $\psi(A+B) = \psi(A) + \psi(B)$, $\psi(AB) = \psi(A)\psi(B)$ whenever this makes sense.

Notice however that $\psi(A\otimes B)$ is not $\psi(A) \otimes \psi(B)$.

As before, $\psi$ has a left inverse, as evidenced by:

For all matrices $X$ of dimension $n \times m$, $ \psi(X)(I_m \otimes \omega) = X \otimes \omega$

While it is true that all coefficients of the standard interpretation of the $\pi/4$ fragment are in $\mathbb{Q}[\piq{}]$, we can be more precise.

Let $\mathbb{D} = \mathbb{Z}[1/2]$ be the set of all dyadic rational numbers, i.e. rational numbers of the form $p/2^n$.

It is easy to see that any element of $\mathbb{D}[\piq{}]$ can be written in a unique way
$a + b \piq{} + c \piq2 + d \piq3$ for some dyadic rational numbers $a,b,c,d$. (It is NOT a consequence of the similar statement for $\mathbb{Q}$. We have to use here the additional property that $\piq{}$ is not only an algebraic number, but also an algebraic integer).

Then it is clear that actually all coefficients of the $\pi/4$ fragment of the ZX-Calculus are in $\mathbb{D}[\piq{}]$.
As $\mathbb{D} \subset \mathbb{Q}$ all we said before still holds, and we actually obtain with $\psi$ a map from matrices over $\mathbb{D}[\piq{}]$ to matrices over $\mathbb{D}$.

We have now provided a way to see a matrix over $\mathbb{D}[\piq{}]$ as a matrix over $\mathbb{D}$. This paves the way to an interpretation from $\zxct$ to $\zwh$.

After all the hassle of the current section, and of the one to come, one can legitimately ask: Why not directly use a version of the ZW-Calculus for the ring $\mathbb{D}[\piq{}]$ ($\zw_{\mathbb{D}[\piq{}]}$), since the ZW-Calculus can be adapted to any ring? Indeed, we could have used this version of the ZW-Calculus. Basically, doing so, the interpretation $[.]_W$ becomes easier, while $[.]_X$ becomes a bit less straightforward.
However, our aim is to provide an axiomatisation that is the simplest possible for the Clifford+T ZX-Calculus. Hence, since the hard part is really to prove that all the axioms of the are derivable in ZX, it is natural to begin with the simplest ZW axiomatisation possible, hence and not $\zw_{\mathbb{D}[\piq{}]}$.

§.§.§ The Interpretation ${[.]_W}$

As announced, the interpretation $[.]_W$ maps any ZX-diagram of the 4 to a -diagram, while the semantics undergoes the homomorphism $\psi$ defined above. It is recursively defined as:

\[ \tikzfig{empty-diagram}~~\mapsto~~ \tikzfig{single-line}\quad\tikzfig{single-line} \qquad\quad
\tikzfig{single-line}~~\mapsto~~ \tikzfig{single-line}\quad\tikzfig{single-line}\quad\tikzfig{single-line} \qquad\quad
\tikzfig{cup}~~\mapsto~~ \tikzfig{cup}~~\tikzfig{single-line}\quad\tikzfig{single-line}\qquad\quad
\tikzfig{caps}~~\mapsto~~ \tikzfig{caps}~~\raisebox{0.5em}{\tikzfig{single-line}\tikzfig{single-line}} \]

\[\tikzfig{crossing}~~\mapsto~~ \tikzfig{crossing}\quad\tikzfig{single-line}\quad\tikzfig{single-line}\qquad\qquad
\tikzfig{Hadamard}~~\mapsto~~\tikzfig{hadamard-interpretation-2-no-braid}\qquad\qquad
\tikzfig{gn-pi_4-1-1}~~\mapsto~~\tikzfig{gn-pi_4-interpretation-2-no-braid}\]

\begin{align*}
\forall D_1&:n\to n',~\forall D_2:m\to m':\\
& D_1\circ D_2 \mapsto [D_1]_W\circ [D_2]_W\qquad(\text{if } m'=n)\\
& D_1\otimes D_2 \mapsto\left( \mathbb{I}^{\otimes n'}\otimes [D_2]_W\right)\circ\left(\nmcrossI{m}{n'}\right)\circ \left(\mathbb{I}^{\otimes m}\otimes [D_1]_W\right)\circ\left(\nmcrossI{n}{m}\right)
\end{align*}

\[\tikzfig{gn-kpi_4}\mapsto \left(\tikzfig{gn-0-1-m-interpretation}\right)\circ\left(\left[\tikzfig{gn-pi_4-1-1}\right]_W\right)^k\circ \left(\tikzfig{gn-0-n-1-interpretation}\right)\]

\[\tikzfig{rn-kpi_4}\mapsto \left[\left(\tikzfig{Hadamard}\right)^{\otimes m}\right]_W\circ \left[\tikzfig{gn-kpi_4}\right]_W \circ \left[\left(\tikzfig{Hadamard}\right)^{\otimes n}\right]_W\]

The interpretation is made so that the two wires on the right act as “control wires”. They are the ones that bear the encoding $\psi$, and as Proposition <ref>, they are the ones the “decoder” will be applied to. In particular, the tensor product can be understood graphically as:

\[ D_1\otimes D_2 \mapsto \tikzfig{interp-of-tensor-product-visualised-2} \]

It order for the tensor product to make sense, $D_1$ and $D_2$ should be able to commute on the control wires. This property is provided by the completeness of the ZW-Calculus, since it is semantically true.

One can check that $\interp{\left[\tikzfig{Hadamard}\right]_W} = \psi\left( \interp{\tikzfig{Hadamard}} \right) = \frac{1}{2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}\otimes (M-M^3)$ and $\interp{\left[\tikzfig{gn-pi_4-1-1}\right]_W} = \psi\left( \interp{\tikzfig{gn-pi_4-1-1}} \right) = \begin{pmatrix}I_4 & 0 \\ 0 & M\end{pmatrix}$. More generally:

Let $D$ be a diagram of the Clifford+T ZX-Calculus. Then

\[\interp{[D]_W}=\psi(\interp{D})\]

In particular, if $\interp{D_1} = \interp{D_2}$ then
$\interp{[D_1]_W} = \interp{[D_2]_W}$

The proof is a straightforward induction using the fact
that $\psi$ is an homomorphism. Slight care has to be taken to
treat the case of $D_1 \otimes D_2$:

Suppose $\interp{D_1}=\sum\limits_{k=0}^3A_k e^{i\frac{k\pi}{4}}$ and $\interp{D_2}=\sum\limits_{k=0}^3B_k e^{i\frac{k\pi}{4}}$ are their unique decomposition, and that $\interp{[D_i]_W}=\psi(\interp{D_i})$. Then:

\begin{align*}
\interp{[D_1\otimes D_2]_W} &= \left(I\otimes \psi(\interp{D_1})\right)\circ \interp{\scalebox{0.7}{\nmcrossI{}{}~}}\circ \left(I\otimes \sum\limits_{k=0}^3A_k\otimes M^k\right)\circ \interp{\scalebox{0.7}{\nmcrossI{}{}~}}\\
&= \left(\sum\limits_{l=0}^3I\otimes B_l \otimes M^l\right)\circ \left(\sum\limits_{k=0}^3A_k \otimes I\otimes M^k\right)
= \sum_{k,l}A_k\otimes B_l \otimes M^{k+l}\\
&= \psi\left(\sum_{k,l}(A_k\otimes B_l) e^{i\frac{(k+l)\pi}{4}}\right) = \psi(\interp{D_1\otimes D_2})
\end{align*}

§.§ From to Clifford+T ZX-Diagrams

We define here an interpretation $[.]_X$ that transforms any diagram of the -Calculus into a Clifford+T ZX-diagram, which is easy to do since $\mathbb{D}\subset\mathbb{D}[\piq{}]$:

\[ \tikzfig{empty-diagram} \quad\mapsto\quad \tikzfig{empty-diagram}\qquad\qquad
\tikzfig{single-line} \quad\mapsto\quad \tikzfig{single-line}\qquad\qquad
\tikzfig{caps} \quad \raisebox{0.3em}{$\mapsto$} \quad \tikzfig{caps}\qquad\qquad
\tikzfig{cup} \quad\raisebox{0.3em}{$\mapsto$}\quad \tikzfig{cup}\]

\[\tikzfig{ZW-to-ZX-braid-no-braid}\qquad\qquad
\tikzfig{ZW-to-ZX-cross-no-braid}\qquad\qquad
\half \quad\mapsto\quad \tikzfig{half-ZX} \qquad\qquad
\tikzfig{ZW-to-ZX-white-dot-1-1}\]

\[\tikzfig{ZW-to-ZX-white-dot-2-1}\qquad\qquad
\tikzfig{ZW-to-ZX-dot-1-1}\qquad\qquad
\tikzfig{ZW-to-ZX-dot-1-2}\]

\[D_1\circ D_2\mapsto [D_1]_X\circ[D_2]_X\qquad D_1\otimes D_2\mapsto [D_1]_X\otimes [D_2]_X\]

Let $D$ be a diagram of the calculus.
Then $\interp{[D]_X}=\interp{D}$

The proof is by induction on $D$.

This interpretation $[.]_X$ from the ZW-Calculus to the ZX-Calculus is pretty straightforward, except for the three-legged black node. Indeed, the two languages express two different kinds of interactions, but at the same time they share a family of generators (the ZW white node and the ZX green node are essentially the same).
This is where some syntactic sugar can come in handy.

We define the “triangle node” as:

\[\tikzfig{ug-decomp}\]

One can check that $\interp{~\tikzfig{ug-node}~} = \begin{pmatrix}1&1\\0&1\end{pmatrix}$. Then the interpretation of the three-legged black dot is simplified using :

\[\tikzfig{ZW-to-ZX-dot-1-2-simplified}\]

This shortcut will be very useful in the technical proof of the completeness of the language for Clifford+T with the set of rules of $\zxct$.

The interpretation $[.]_X$ preserves all the rules of the -Calculus:

\[ \zwh\vdash D_1=D_2 \quad\implies\quad \zxct\vdash [D_1]_X= [D_2]_X \]

The proof, quite technical, is in Appendix at Section <ref>.

§.§ Composing the Interpretations

To finish the proof it remains to compose the two interpretations and check that we can recover the initial diagram after the decoding part (Proposition <ref>), where:

$$\omega = \begin{pmatrix}1\\\piq{}\\ \piq2\\ \piq3\end{pmatrix} =\interp{\scalebox{0.8}{\tikzfig{theta}}}\qquad\text{and}\qquad
e_1=\begin{pmatrix}1&0&0&0\end{pmatrix} = \interp{\scalebox{0.8}{\tikzfig{projector-1-0-0-0}}}$$

We can recover any Clifford+T ZX-diagram $D$ from its image under the composition of the two interpretations:

\begin{align*}
\zxct\vdash D =\left(\hspace{-0.2em}\scalebox{0.8}{\tikzfig{bottom-composition}}\hspace{-0.3em}\right)\circ\left[[D]_W\right]_X\circ\left(\hspace{-0.2em}\scalebox{0.8}{\tikzfig{top-composition}}\hspace{-0.3em}\right)
\end{align*}

The proof is in Appendix at Section <ref>.

If $\zxct \vdash \left[[D_1]_W\right]_X = \left[[D_2]_W\right]_X$
then $\zxct \vdash D_1 = D_2$.

We can now prove Theorem <ref>:

Let $D_1$ and $D_2$ be two Clifford+T ZX-diagrams, such that $\interp{D_1}=\interp{D_2}$. By Proposition <ref>, $\interp{[D_1]_W}=\interp{[D_2]_W}$. Since $[D_i]_W$ are -diagrams, and since the -Calculus is complete, $\zwh\vdash [D_1]_W=[D_2]_W$. By Proposition <ref>, $\zxct\vdash \left[[D_1]_W\right]_X = \left[[D_2]_W\right]_X$. Finally, by Corollary <ref>, $\zxct \vdash D_1 = D_2$.

§.§ Expressive Power of the Clifford+T ZX-Diagrams

Since the unitary matrices over $\mathbb{D}[\piq{}]$ are representable with Clifford+T circuits [20], so are they with 4 diagrams. Using the fact that the $\zwh$-Diagrams can represent any matrix of $\mathbb{D}^{2^n}\times\mathbb{D}^{2^m}$ (Proposition <ref>), we actually show that any matrix over $\mathbb{D}[\piq{}]$ can be represented by a -diagram:

The 4 of the ZX-Calculus represents exactly  matrices over $\mathbb{D}[\piq{}]$:

\[\forall A\in \mathbb{D}[\piq{}]^{2^n\times 2^m},~~\exists D\in \zxct,~~ \interp{D}=A\]

Let $A\in \mathbb{D}[\piq{}]^{2^n\times 2^m}$. We define $A'=\psi(A)\in\mathbb{D}^{2^{n+2}\times 2^{m+2}}$. Since -diagrams are universal for matrices over dyadic rationals: $\exists D\in \zwh,~\interp{D}=A'$. Since $[.]_X$ preserves the semantics, we can define a ZX-diagram of the 4 $D'=[D]_X$ such that $\interp{D'}=A'$.

Now, by plugging 0.8theta at the top and 0.8projector-1-0-0-0 at the bottom of the two rightmost wires of $D'$, we get the diagram $D''$ which is such that $\interp{D''}=A$.

§ COMPLETENESS FOR LINEAR DIAGRAMS WITH CLIFFORD+T CONSTANTS

§.§ Variables and Constants

It is customary to view some angles in the ZX-diagrams as variables, in order to prove families of equalities. For instance, the rule displays two variables $\alpha$ and $\beta$, and potentially gives an infinite number of equalities. Notice that in the axioms of the ZX-calculus, the variables are used in a linear way, reflecting the phase group structure.

A ZX-diagram is linear in $\alpha_1, \ldots, \alpha_k$ with constants in $C\subseteq \mathbb R$, if it is generated by $R_Z^{(n,m)}(E)$, $R_X^{(n,m)}(E)$, $H$, $e$, $\mathbb I$, $\sigma$, $\epsilon$, $\eta$, and the spacial and sequential compositions, where $n,m\in \mathbb  N$, and $E$ is an affine combination of $\alpha_i$ with coefficients in $\mathbb{Z}$ and constants in $C$, i.e. of the form $\sum_{i} n_i \alpha_i+c$, with $n_i\in \mathbb Z$ and $c\in C$.

Notice that all the diagrams in Figures <ref> and <ref> are linear in $\alpha, \beta, \gamma$ with constants in $\frac \pi 4 \mathbb Z$. A diagram linear in $\alpha_1, \ldots,  \alpha_k$ is denoted $D(\alpha_1, \ldots, \alpha_k)$, or more compactly $D(\vec \alpha)$ with $\vec \alpha = \alpha_1, \ldots, \alpha_k$. Obviously, if $D(\alpha)$ is a diagram linear in $\alpha$, $D(\pi/2)$ denotes the ZX-diagram where all occurrences of $\alpha$ are replaced by $\pi/2$.

§.§ From variables to inputs

We show in this section that, given an equation involving diagrams linear in some variable $\alpha$, the variables can be extracted, splitting  the diagrams into two parts: a collection of points (nodes with parameter $\alpha$) and a constant diagram independent of the variables.

First we define the multiplicity of a variable in an equation:

For any $D_1(\vec \alpha), D_2(\vec \alpha): n\to m$ two ZX-diagrams linear in $\vec \alpha$, the multiplicity of $\alpha_1$ in the equation $D_1(\vec \alpha) = D_2(\vec \alpha)$ is defined as:

$$\mu_{\alpha_1} = \max_{i\in \{1,2\}}\left(\mu^+_{\alpha_1}(D_i(\vec \alpha))\right)  + \max_{i\in \{1,2\}}\left(\mu^-_{\alpha_1}(D_i(\vec \alpha))\right)$$

$\mu^+_{\alpha_1}(D)$ (resp. $\mu^-_{\alpha_1}(D)$) is the number of occurrences of $\alpha_1$ (resp. -$\alpha_1$) in $D$,  inductively defined as

$\mu^+_{\alpha_1}(R_Z^{(n,m)}(\ell\alpha_1+E(\alpha_2\cdots \alpha_n)))=\mu^+_{\alpha_1}(R_X^{(n,m)}(\ell\alpha_1+E(\alpha_2\cdots \alpha_n)))=\begin{cases} \ell &\text{if $\ell>0$}\\0&\text{otherwise}\end{cases}$

$\mu^-_{\alpha_1}(R_Z^{(n,m)}(\ell\alpha_1+E(\alpha_2\cdots \alpha_n)))=\mu^-_{\alpha_1}(R_X^{(n,m)}(\ell\alpha_1+E(\alpha_2\cdots \alpha_n)))=\begin{cases} -\ell&\text{if $\ell<0$}\\0&\text{otherwise}\end{cases}$

$\mu^\pm_{\alpha_1}(D\otimes D') = \mu^\pm_{\alpha_1}(D\circ D') = \mu^\pm_{\alpha_1}(D)+\mu^\pm_{\alpha_1}(D')$

$\mu^\pm_{\alpha_1}(H)=\mu^\pm_{\alpha_1}(e)=\mu^\pm_{\alpha_1}(\mathbb I)=\mu^\pm_{\alpha_1}(\sigma)=\mu^\pm_{\alpha_1}(\epsilon)=\mu^\pm_{\alpha_1}(\eta)=0$

For instance, consider the following equation:

\[\tikzfig{big-scalar-equation}\]

The multiplicity of $\alpha$ is $\mu_\alpha = 2$ and $\beta$'s is $\mu_\beta = 3$.

For any $D_1(\alpha), D_2(\alpha): n\to m$ two ZX-diagrams linear in $\alpha$ with constants in $\frac \pi 4$ $\mathbb Z$, there exist  $D_1', D'_2:r\to n+m$ two ZX-diagrams with angles multiple of $\frac \pi 4$ such that, for any $\alpha \in \mathbb R$, the equivalence

\begin{equation}\label{eq:varasinputs}
D_1(\alpha)= D_2(\alpha) \equi{} D_1'\circ \theta_r(\alpha) =  D_2'\circ \theta_r(\alpha)
\end{equation}

is provable using the axioms of $\zxct$, where $r$ is the multiplicity of $\alpha$ in $D_1(\alpha) = D_2(\alpha)$, and $\theta_r(\alpha)= \left(R_Z^{(0,1)}(\alpha)\right)^{\otimes r}$.

\[\tikzfigc{00}\eq{}\tikzfigc{01}\equi{}\tikzfigc{02}\eq{}\tikzfigc{03}\]

The proof consists in transforming the equation $D_1(\alpha)=D_2(\alpha)$ into the equivalent equation $D_1'\circ \theta_r(\alpha) =  D_1'\circ \theta_r(\alpha)$ using axioms of the ZX-calculus. This transformation involves 6 steps:

– Turn inputs into outputs. First, each input can be bent to an output using $\eta$:
\[\tikzfigc{00}\eq{}\tikzfigc{01}\equi{}\tikzfigc{02}\eq{}\tikzfigc{03}\]

– Make the red spiders green. All red spiders $R^{(k,l)}_X(n\alpha+c)$ are transformed into green spiders using the axioms and :

\[\tikzfigc{00}\eq{}\tikzfigc{01}\]

– Expending spiders. All spiders $R_Z(n\alpha +c)$ are expended using so that all the occurrences of $\alpha$ are either $\alpha$ or -$\alpha$:

\[\tikzfigc{00}\eq{}\tikzfigc{01}\]

– Changing the sign. Using all occurrences of -$\alpha$
are replaced as follows: $\rz{-$\alpha$} \mapsto\tikzfig{Rz-0-1-minus-alpha}$. Notice that this rule is not applied recursively, which would not terminate. After this step all the original $-\alpha$ have been replaced by an $\alpha$ and as many scalars scalar-e-pow-minus-i-alpha have been created. So far, we have shown:

\begin{align*}
\tikzfigc{00}\eq{}\tikzfigc{01}\equi{}
\tikzfigc{06}\eq[]{}\tikzfigc{07}
\end{align*}

– (Re)moving scalars. The scalar scalar-e-pow-i-alpha has an inverse for $\otimes$, which is scalar-e-pow-minus-i-alpha (see Lemmas <ref>, <ref> and <ref>). This has for consequence:

* $\zxct\vdash \scalebox{0.8}{\tikzfig{scalar-e-pow-minus-i-alpha}}D_1=D_2 \equi{}\zxct\vdash D_1=\scalebox{0.8}{\tikzfig{scalar-e-pow-i-alpha}}D_2$

* $\zxct\vdash \scalebox{0.8}{\tikzfig{scalar-e-pow-i-alpha}}D_1=\scalebox{0.8}{\tikzfig{scalar-e-pow-i-alpha}}D_2 \equi{} \zxct\vdash D_1=D_2$

The scalars scalar-e-pow-minus-i-alpha are eliminated by adding $\overset{-}{\mu}\substack{\max\\\alpha\ \ }:=\max\left(\mu^-_\alpha(D_1),\mu^-_\alpha(D_2)\right)$ times the scalar scalar-e-pow-i-alpha on both sides, then simplifying when we have a scalar and its inverse.

\begin{align*}
\equi{}\tikzfigc{08}\eq{}\tikzfigc{09}
\end{align*}

– Balancing the variables. At this step the number of occurrences of $\alpha$ might be different on both sides of the equation. Indeed, one can check that the side of $D_i$ has $\mu^+_\alpha(D_i)+\overset{-}{\mu}\substack{\max\\\alpha\ \ }$ occurrences of $\alpha$. One can then use the simple equation inverse-alpha (whose proof uses Lemmas <ref> and <ref>) $\overset{+}{\mu}\substack{\max\\\alpha\ \ }-\mu^+_\alpha(D_i)$ times on the side of $D_i$, where $\overset{+}{\mu}\substack{\max\\\alpha\ \ }:=\max\left(\mu^+_\alpha(D_1),\mu^+_\alpha(D_2)\right)$. We hence end up with $\mu_\alpha =\overset{+}{\mu}\substack{\max\\\alpha\ \ }+\overset{-}{\mu}\substack{\max\\\alpha\ \ }$ occurrences of $\alpha$ on both sides. Formally, $D_i'$ is defined as:

\begin{align*}
\tikzfigc{10}:=\tikzfigc{11}
\end{align*}

Proposition <ref>  implies in particular that if the equation $D_1'\circ \theta_r(\alpha) =  D_2'\circ \theta_r(\alpha)$ is provable  using the axioms of the ZX-calculus, then so is $D_1(\alpha)= D_2(\alpha)$.
Proposition <ref> also implies that if $\interp{D_1(\alpha)}= \interp{D_2(\alpha)}$, then $ \interp{D_1'\circ \theta_r(\alpha)} = \interp{ D_2'\circ \theta_r(\alpha)}$, thanks to the soundness of the ZX-calculus.

§.§ Removing the variables

Given $D_1(\alpha)$ and $D_2(\alpha)$  linear in $\alpha$ with constants in $\frac \pi 4\mathbb Z$, if $\alpha$ has multiplicity $1$ in  ${D_1(\alpha)} = {D_2(\alpha)}$, then according to Proposition <ref>, the equation  can be transformed into the following equivalent equation involving a single occurrence of $\alpha$:

\begin{equation}\label{eq:single}
\tikzfig{thm1-single-occurrence}
\end{equation}

where $D_1'$ and $D_2'$ are in the $\frac \pi 4$-fragment.
Notice that equation (<ref>) holds
if and only if $\interp{D_1'}=\interp{D_2'}$, since $\left(\rz{}, \rz{$\pi$}\right)$ forms a basis of the input space. Thus, a variable of multiplicity $1$ can easily be removed, leading to an equivalent equation in the complete $\frac \pi 4$-fragment of the ZX-calculus.

When a variable has a  multiplicity $r>1$ in an equation, the variable cannot be removed similarly as $\left(\rz{$\alpha$}\right)^{\otimes r}$ does not generate a basis of the $2^r$ dimensional space when $r>1$. However these dots can be replaced by an appropriate projector on the subspace generated by these dots, as described in the following.

§.§.§ When the multiplicity is 2

Consider the following diagram $R$:

\[\tikzfig{2-in-2-out-box-var}~~:=~~\tikzfig{matrix-X}\]

One can check that $\interp R=\begin{pmatrix}
\end{pmatrix}$. This matrix basically mixes the second and third elements of any size-4 vector. We can then show:

For any $\alpha \in \mathbb R$, $\zxct\vdash R\circ \theta_2(\alpha) = \theta_2(\alpha)$, i.e. pictorially:

\[\forall\alpha\in\mathbb{R},~~\zxct\vdash~ \tikzfig{2-gn-alpha-to-X}\]

The proof is given in appendix.

For any two ZX-diagrams $D_1,D_2 : 2 \to n$,
$(\forall \alpha\in \mathbb R, \interp{D_1\circ \theta_2(\alpha)} =  \interp{D_2\circ \theta_2(\alpha)}) \Leftrightarrow \interp{D_1\circ R}=\interp{D_2\circ R}$ i.e.,

$$\left(\forall\alpha\in\mathbb{R},~~ \interp{\tikzfig{2-gn-alpha-to-D_1}}  = \interp{\tikzfig{2-gn-alpha-to-D_2}}\right) \Leftrightarrow \interp{\tikzfig{2-gn-D_1-X}} = \interp{\tikzfig{2-gn-D_2-X}}$$

where $\alpha$ does not appear in $D_1$ or $D_2$.

The proof consists in showing that $\interp R$ is a projector onto $S= \mathop{\mathrm{span}} \{ \interp{\theta_2(\alpha)}~|~\alpha \in \mathbb{R}\}$. According to Lemma <ref>, $\interp R$ is the identity on $S$, moreover it is easy to show that $\interp R$ is a matrix of rank $3$ and that $\interp {\theta_2(0)},\interp {\theta_2(\pi/2)}, \interp {\theta_2(\pi)}$  are three linearly independent vectors in the image of $\interp R$.

§.§.§ Arbitrary multiplicity

We now want to generalise Lemma <ref> to any multiplicity $r$ of $\alpha$.
It turns out that there is no obvious generalization for $r$ wires of the matrix $\interp R$ expressible using angles multiple of $\frac \pi 4$, so we will rather use the following family  $(P_r)_{r\ge 1}$ of diagrams:

\[\left\lbrace\begin{array}{l}
\tikzfig{P1}\\
\tikzfig{2-in-2-out-box-M_2}~~:=~~ \tikzfig{matrix-M2-2-arxiv}\\
\tikzfig{matrix-M_n-def}~~=~~\scalebox{0.6}{\tikzfig{matrix-M_n-form}}
\end{array}\right.\]

For the reader convenience, here are the interpretations of $P_2$ and $P_3$:

\[
\interp{P_2} = \begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 0 & 1 & 0 \\
0 & 0 & 1 & 0 \\
0 & 0 & 0 & 1 \\
\end{pmatrix}
\qquad \interp{P_3} = \begin{pmatrix}
1 & 0 & 0 & 0 & 0 & 0 & 0 & 0  \\%000
0 & 0 & 0 & 0 & 1 & 0 & 0 & 0 \\%001
0 & 0 & 0 & 0 & 1 & 0 & 0 & 0 \\%010
0 & 0 & 0 & 0 & 0 & 0 & 1 & 0  \\%011
0 & 0 & 0 & 0 & 1 & 0 & 0 & 0  \\%100
0 & 0 & 0 & 0 & 0 & 0 & 1 & 0 \\%101
0 & 0 & 0 & 0 & 0 & 0 & 1 & 0 \\%110
0 & 0 & 0 & 0 & 0 & 0 & 0 & 1  \\%111
\end{pmatrix}
\]

We can characterise the interpretation of $P_r$ for any $r$.

For any word $\vec x\in\{0,1\}^r$, $\interp{P_r}^t\ket{\vec x}=\ket{1^{|\vec x|_1}0^{r-|\vec x|_1}}$ where $|\vec x|_1$ is the Hamming weight of $x$ i.e. the number of symbol $1$ in the word $\vec x$.

Informally, $\interp{P_r}^t$ sends all the words of the same Hamming weight to the word of the same weight where all the $1$s are on the left.

First of all, notice that the result is true for $P_2$:

\[\interp{P_2}^t\ket{00}=\ket{00},\qquad \interp{P_2}^t\ket{01}=\interp{P_2}^t\ket{10}=\ket{10},\qquad \interp{P_2}^t\ket{11}=\ket{11}\]

Let us denote $\operatorname{Op}^{[i_1,\cdots,i_k]}$ the application of the $k$-qubit operator $\operatorname{Op}$ on the wires $i_1,\cdots,i_k$. With this notation, $\interp{P_r}^t=\interp{P_2}^{t[1,2]}\circ \interp{P_2}^{t[2,3]}\circ\cdots\circ \interp{P_2}^{t[r-1,r]}\circ \interp{P_{r-1}}^{t[1,\cdots,r-1]}$.
We then prove the result by induction on $r$. Let $\vec x\in\{0,1\}^r$ be a word. Then:

\begin{align*}
\interp{P_{r+1}}\ket{\vec x0}
&= \interp{P_2}^{t[1,2]}\circ \interp{P_2}^{t[2,3]}\circ\cdots\circ \interp{P_2}^{t[r,r+1]}\circ \interp{P_r}^{t[1,\cdots,r]}\ket{\vec x0}\\
&= \interp{P_2}^{t[1,2]}\circ \cdots\circ \interp{P_2}^{t[r,r+1]} \ket{1^{|\vec x|_1}0^{r-|\vec x|_1}0}\\
%&= \interp{P_2}^{t[1,2]}\circ \cdots\circ \ket{1^{|\vec x|_1}0^{r-|\vec x|_1}0}\\
&= \cdots\\
&= \ket{1^{|\vec x|_1}0^{r+1-|\vec x|_1}}
\end{align*}

\begin{align*}
\interp{P_{r+1}}\ket{\vec x1}
&= \interp{P_2}^{t[1,2]}\circ \interp{P_2}^{t[2,3]}\circ\cdots\circ \interp{P_2}^{t[r,r+1]}\circ \interp{P_r}^{t[1,\cdots,r]}\ket{\vec x1}\\
&= \interp{P_2}^{t[1,2]}\circ \cdots\circ \interp{P_2}^{t[r,r+1]} \ket{1^{|\vec x|_1}0^{r-|\vec x|_1}1}\\
&= \interp{P_2}^{t[1,2]}\circ \cdots\circ \ket{1^{|\vec x|_1}0^{r-1-|\vec x|_1}10}\\
&= \cdots\\
&= \interp{P_2}^{t[1,2]}\circ \cdots\circ\interp{P_2}^{t[|\vec x|_1,|\vec x|_1+1]} \circ \ket{1^{|\vec x|_1}10^{r-|\vec x|_1}}\\
&= \cdots\\
&= \ket{1^{|\vec x|_1+1}0^{r-|\vec x|_1}}
\end{align*}

The rank of $\interp{P_r}$ is exactly $r+1$.

For any $r\ge 2$ and any $\alpha \in \mathbb R$, $\zxct\vdash P_r\circ \theta_r(\alpha) = \theta_r(\alpha)$ i.e.,

\[\zxct\vdash~ \tikzfig{n-gn-alpha-to-M_n}\]

Notice that $\interp{P_2\circ R} = \interp R$, so by completeness of the ZX-calculus for the $\frac \pi 4$ fragment, $\zxct\vdash P_2\circ R = R$, so  $\zx\vdash P_2\circ R \circ \theta_2(\alpha) = R\circ \theta_2(\alpha)$. According to Lemma <ref>, it implies $\zxct\vdash P_2\circ \theta_2(\alpha) = \theta_2(\alpha)$. The proof for $r>2$ is by induction on $r$.

We can now prove a similar statement as in lemma <ref>:

For any $r\ge 2$ and any $D_1,D_2 : r \to n$,
$(\forall \alpha\in \mathbb R, \interp{D_1\circ \theta_r(\alpha)} =  \interp{D_2\circ \theta_r(\alpha)}) \Leftrightarrow \interp{D_1\circ P_r}=\interp{D_2\circ P_r}$ i.e.,

\begin{align*}
\left(\forall\alpha\in\mathbb{R},~~ \interp{\tikzfig{r-gn-alpha-to-D_1}} = \interp{\tikzfig{r-gn-alpha-to-D_2}}\right) \Leftrightarrow \interp{\tikzfig{P-to-D1}} = \interp{\tikzfig{P-to-D2}}
\end{align*}

where $\alpha$ does not appear in $D_1$ nor $D_2$.

The proof consists in showing that $\interp {P_r}$ is a projector onto $S_r= \mathop{\mathrm{span}} \{ \interp{\theta_r(\alpha)}~|~\alpha \in \mathbb{R}\}$. According to  Lemma <ref>, $\interp{P_r}$ is the identity on $S_r$, and $\interp {P_r}$ is of rank at most $r+1$ according to Corollary <ref>, thus to finish the proof, it is sufficient to prove that the $r+1$ vectors $(\theta_r(\alpha^{(j)}))_{j=0\ldots r}$ are linearly independent, where $\alpha^{(j)} = j\pi/r$.

Let $\lambda_0,...,\lambda_r$ be scalars such that $\sum_j\lambda_j\theta_r(\alpha^{(j)})=0$.
Notice that the $2^p$-th row (when rows are labeled from $1$ to $2^r$) of $\theta_r(\alpha^{(j)})$ is exactly $e^{ip\alpha^{(j)}}$.
Therefore, if we look at all $2^p$-th rows of the equations, we obtain

\[ \begin{pmatrix}
\vdots&\vdots&\ddots&\vdots\\
\end{pmatrix}\begin{pmatrix}
\lambda_0\\
\lambda_1\\
\vdots\\
\lambda_r
\end{pmatrix}=0 \]

However, the first matrix is a Vandermonde matrix (actually its transpose), with
$e^{i\alpha^{(j)}}=e^{i\alpha^{(l)}}$ iff $j=l$, which is enough to state that
this matrix is invertible. Therefore all $\lambda_j$ are equal to $0$
and the vectors $\theta_r(\alpha^{(j)})$ are linearly independent.

We are now ready to prove the main theorem in the particular case of a single variable:

For any $D_1(\alpha), D_2(\alpha)$ ZX-diagrams linear in $\alpha$ with constants in $\frac \pi 4 \mathbb Z$,

$$ \forall  \alpha \in \mathbb R, \interp{D_1( \alpha)}= \interp{D_2( \alpha)}      \,\,\,\,\,\Leftrightarrow\,\,\,\,\,  \forall  \alpha \in \mathbb R, \zxct\vdash D_1( \alpha) = D_2( \alpha)       $$

[$\Leftarrow$] is a direct consequence of the soundness of the ZX-calculus.
[$\Rightarrow$] Assume $\forall  \alpha \in \mathbb R, \interp{D_1( \alpha)}= \interp{D_2( \alpha)}$. According to Proposition <ref>, $\forall  \alpha \in \mathbb R, \interp{D'_1\circ \theta_r(\alpha)}= \interp{D'_2\circ \theta_r( \alpha)}$ where $D'_i$ are in the $\frac \pi 4$-fragment of the ZX-calculus. It implies, according to Lemma <ref>, that  $\interp{D_1'\circ P_r} = \interp{D_2'\circ P_r}$. Thanks to the completeness of the ZX-calculus for the $\frac \pi 4$-fragment, $\zxct\vdash D_1'\circ P_r= D_2'\circ P_r$, so $\forall \alpha\in \mathbb R, \zxct\vdash D_1'\circ P_r \circ \theta_r(\alpha)= D_2'\circ P_r\circ \theta_r(\alpha)$. Thus, by Lemma <ref>, $\forall \alpha\in \mathbb R,~\zxct\vdash D_1' \circ \theta_r(\alpha)= D_2'\circ  \theta_r(\alpha)$, which is equivalent to $\forall  \alpha \in \mathbb R,~\zxct\vdash D_1( \alpha) = D_2( \alpha)$ according to Proposition <ref>.

§.§ Multiple variables

Proposition <ref> can be straighforwardly extended to multiple variables:

For any $D_1(\vec \alpha), D_2(\vec \alpha): n\to m$ two ZX-diagrams linear in $\vec \alpha=\alpha_1,\ldots, \alpha_k$ with constants in $\frac \pi 4 \mathbb Z$, there exist  $D_1', D'_2:(\sum_{i=1}^k r_i)\to n+m$ two ZX-diagrams with angles multiple of $\frac \pi 4$ such that, for any $\vec \alpha \in \mathbb R^k$,

\begin{equation}
\label{eq:varasinputs}
D_1(\vec \alpha)= D_2(\vec \alpha) \quad\Leftrightarrow\quad D_1'\circ \theta_{\vec r}(\vec \alpha) =  D_2'\circ \theta_{\vec r}(\vec \alpha)
\end{equation}

is provable using the axioms of the ZX-calculus, where $r_i$ is the multiplicity of $\alpha_i$ in $D_1(\vec \alpha)=D_2(\vec \alpha)$, $\vec r:=r_1, \ldots, r_k$, and $\theta_{\vec{r}}(\vec{\alpha}):=\theta_{r_1}(\alpha_1)  \otimes \ldots\otimes \theta_{r_k}(\alpha_k)$.

\begin{align*}
\end{align*}

Similarly Lemma <ref> can also be extended to multiple variables:

For any $k\ge  0$, any $\vec r=r_1,\ldots, r_k\in \mathbb N^k$ and any $D_1,D_2 : (\sum_ir_i) \to n$,
$(\forall \vec \alpha\in \mathbb R^k\!, \interp{D_1\circ \theta_{\vec r}(\vec \alpha)} =  \interp{D_2\circ \theta_{\vec r}(\vec \alpha)}) \Leftrightarrow \interp{D_1\circ P_{\vec r}}=\interp{D_2\circ P_{\vec r}}$

where no $\alpha_i$ appear in $D_1$ or $D_2$, and $P_{\vec r} = P_{r_1} \otimes \ldots \otimes P_{r_k}$.

Using Proposition <ref> and Lemma <ref> (whose proofs are similar to those of <ref> and <ref>), the proof of Theorem <ref> is similar to the single variable case (Proposition <ref>) by induction.

Notice that Theorem <ref> implies that if $\forall \vec \alpha \in \mathbb R^k,  \interp{D_1(\vec \alpha)}= \interp{D_2(\vec \alpha)} $ then $D_1(\vec \alpha)=D_2(\vec \alpha)$ has a uniform proof in the ZX-calculus in the sense that the structure of the proof is the same for all the values of $\vec \alpha \in \mathbb R^k$. Indeed, following the proof of Theorem <ref>, the sequence of axioms which leads to a proof of $D_1(\vec \alpha)=D_2(\vec \alpha)$ is independent of the particular values of $\vec \alpha$.  Notice, however, that Theorem <ref> is non constructive.

§ APPLICATIONS OF LINEAR DIAGRAMS

In order to prove that $\forall \vec \alpha \in \mathbb R^k, \zxct\vdash D_1(\vec \alpha)=D_2(\vec \alpha)$ using  Theorem <ref>, one has to double check the semantic condition $\interp{D_1(\vec \alpha)}= \interp{D_2(\vec \alpha)}$ for all $\vec \alpha \in \mathbb R^k$, which might not be easy in practice. We show in the following alternative ways to prove $\forall \vec \alpha \in \mathbb R^k, \zxct\vdash D_1(\vec \alpha)=D_2(\vec \alpha)$, the two first based on a finite case-based reasoning in the ZX-calculus, and the last one by diagram substitution.

§.§ Considering a basis

For any ZX-diagrams $D_1(\vec \alpha),D_2(\vec \alpha):1\to m$ linear in $\vec \alpha=\alpha_1, \ldots, \alpha_k$ with constants in $\frac \pi 4 \mathbb Z$, if

$$\forall j\in \{0,1\},\forall \vec \alpha \in \mathbb R^k,  \zxct\vdash {D_1(\vec \alpha)\circ R_X(j\pi)}= {D_2(\vec \alpha)\circ R_X(j\pi)}$$

$$\forall \vec \alpha \in \mathbb R^k, \zxct\vdash D_1(\vec \alpha) = D_2(\vec \alpha)$$

Assume $\zxct\vdash {D_1(\vec \alpha)\circ R_X(j\pi)}= {D_2(\vec \alpha)\circ R_X(j\pi)}$ for any $j\in \{0,1\}$ and any $\vec \alpha \in \mathbb R^k$. It implies that for $x\in \left\lbrace \left(\begin{array}{c}1\\0\end{array}\right),\left(\begin{array}{c}0\\1\end{array}\right)\right\rbrace$, $\interp{D_1(\vec \alpha)} x= \interp{D_2(\vec \alpha)}x$, so $\interp{D_1(\vec \alpha)} = \interp{D_2(\vec \alpha)}$, which implies according to Theorem  <ref> $\forall \vec \alpha \in \mathbb R^k, \zxct\vdash D_1(\vec \alpha) = D_2(\vec \alpha)$.

Notice that the Theorem <ref> can be applied recursively: in order to prove the equality between two diagrams  with  $n$ inputs, $m$ outputs, and constants in $\frac \pi 4\mathbb Z$, one can consider the $2^{n+m}$ ways to fix these inputs/outputs in a standard  basis states. It reduces the existence of a proof between two diagrams with constants in $\frac \pi 4\mathbb Z$ to the existence of proofs on scalar diagrams (diagrams with no input and no output).

\[\forall \alpha, \beta\in \mathbb R, \zxct\vdash~~ \tikzfig{add-axiom-2}\]

We can prove that this equality is derivable by plugging our basis $\left(\rx{},\rx{$\pi$}\right)$ on the input and one of the outputs. The detail is given in the appendix at Section <ref>.

§.§ Considering a finite set of angles

For any ZX-diagrams $D_1(\vec \alpha),D_2(\vec \alpha):n\to m$ linear in $\vec \alpha = \alpha_1, \ldots, \alpha_k$ with constants in $\frac \pi 4 \mathbb Z$, if

$$\forall \vec \alpha \in T_1\times \ldots \times T_k,  \zxct\vdash {D_1(\vec \alpha)}= {D_2(\vec \alpha)}$$

$$\forall \vec \alpha \in \mathbb R^k, \zxct\vdash D_1(\vec \alpha) = D_2(\vec \alpha)$$

with $T_i$  a set of $\mu_i+1$
distinct angles in $\mathbb{R}/2\pi\mathbb{Z}$
where $\mu_i$ is the multiplicity of $\alpha_i$ in $D_1(\vec \alpha) = D_2(\vec \alpha)$.

In the proof of Lemma <ref>, we actually only used $\mu_{\alpha}+1$ values of $\alpha$, that constitute a basis of $S_{\mu_{\alpha}}$. This extends naturally to several variables: the dimension of $S_{\mu_{\alpha_1}}\times\cdots\times S_{\mu_{\alpha_k}}$ is $(\mu_{\alpha_1}+1)\times\cdots\times(\mu_{\alpha_k}+1)$, and taking $\vec \alpha \in T_1\times \ldots \times T_k$ gives as many linearly independent vectors in (hence a basis of) $S_{\mu_{\alpha_1}}\times\cdots\times S_{\mu_{\alpha_k}}$.

\[\tikzfig{big-scalar-equation}\]

Notice that $\mu_{\alpha}=2$ and $\mu_{\beta}=3$ in this equation. Hence we need to evaluate it for 12 values of $(\alpha,\beta)$, for instance for $\alpha,\beta\in\{0,\pi,\frac{\pi}{2}\}\times\{0,\pi,\frac{\pi}{2},-\frac{\pi}{2}\}$.
We can actually simplify the proof, by showing that whatever the value of $\beta\in\mathbb{R}$, the equation is derivable for $\alpha\in\{0,\pi,\frac{\pi}{2}\}$. This means the equation is derivable for all

$\alpha,\beta\in\{0,\pi,\frac{\pi}{2}\}\times\mathbb{R}$, and a fortiori for all $\alpha,\beta\in\{0,\pi,\frac{\pi}{2}\}\times\{0,\pi,\frac{\pi}{2},-\frac{\pi}{2}\}$ which would be a direct application of the theorem.
Details are in appendix at Section <ref>.

The number of occurrences of a variable is not to be mistaken for its multiplicity. For instance consider the following equation:

\[\rz{$\alpha$}=\rz{-$\alpha$}\]

This equation is obviously wrong in general, but not for $0$ and $\pi$. If we tried to apply Theorem <ref> with the number of occurrences (which seems to be $1$), then we might end up with the wrong conclusion. The multiplicity (here $\mu_{\alpha}=2$) prevents this.

§.§ Diagram substitution

A diagram $D:0 \to n$ is symmetric if for any permutation $\tau$ on $\{1,\ldots n\}$,
$$Q_\tau(\interp {D}) = \interp{D}$$
where $Q_\tau:\mathbb C^{2^r}\to \mathbb C^{2^r}$ is the unique morphism such that:

$\forall \varphi_1,\ldots, \varphi_r\in \mathbb C^{2}$, $Q_\tau(\varphi_1 \otimes \ldots \otimes \varphi_r)=\varphi_{\tau(1)} \otimes \ldots \otimes \varphi_{\tau(r)}$.

In particular for any diagram $D_0:0\to 1$, $D_0\otimes \ldots \otimes D_0$ is a symmetric diagram.

For any $D_1(\vec \alpha), D_2(\vec \alpha):r\to n$ and any symmetric $D(\vec \alpha):0\to r$ such that  $D_1(\vec \alpha)$, $D_2(\vec \alpha)$, and $D(\vec \alpha)$ are linear in $\vec \alpha$ with constants in $\frac \pi 4\mathbb Z$, if $\forall \alpha_0\in \mathbb R, \forall\vec \alpha\in\mathbb{R}^k, \zxct\vdash D_1(\vec \alpha) \circ \theta_r(\alpha_0) = D_2(\vec \alpha) \circ \theta_r(\alpha_0)$ then $\forall\vec \alpha\in\mathbb{R}^k, \zxct\vdash D_1(\vec \alpha) \circ D(\vec \alpha) = D_2(\vec \alpha) \circ D(\vec  \alpha)$ i.e., pictorially:

\begin{align*}
\left(\forall \alpha_0\in \mathbb R, \forall\vec \alpha\in\mathbb{R}^k,~~ \zxct\vdash {\tikzfig{2-gn-alpha-to-D_1-bis}}  = {\tikzfig{2-gn-alpha-to-D_2-bis}}\right)
\implies ~~\left(\forall\vec \alpha\in\mathbb{R}^k, \zxct\vdash {\tikzfig{2-gn-D_1-X-bis}} = {\tikzfig{2-gn-D_2-X-bis}}\right)
\end{align*}

If $\forall \alpha_0\in \mathbb R, \forall\vec \alpha\in\mathbb{R}^k, \zxct\vdash D_1(\vec \alpha) \circ \theta_r(\alpha_0) = D_2(\vec \alpha) \circ \theta_r(\alpha_0)$ then $\interp{D_1(\vec \alpha) \circ \theta_r(\alpha_0)} = \interp{D_2(\vec \alpha) \circ \theta_r(\alpha_0)}$, so according to Lemma <ref>, $\interp{D_1(\vec \alpha) \circ P_r} = \interp{D_2(\vec \alpha) \circ P_r}$. It implies that $\zxct\vdash D_1(\vec \alpha) \circ P_r  =D_2(\vec \alpha) \circ P_r$, so $\zxct\vdash D_1(\vec \alpha) \circ P_r \circ D(\vec \alpha)  =D_2(\vec \alpha) \circ P_r\circ D(\vec \alpha)$. To complete the proof, it is enough to show that $\zxct\vdash P_r\circ D(\vec \alpha) = D(\vec \alpha)$.

Let $\mathcal S = \{\interp D ~|~ÊD:0\to n \text{ symmetrical}\}$. First we show that $\mathcal S$ is of dimension at most $r+1$.

Indeed, notice that if $\varphi \in \mathcal S$, then $\forall i,j\in \{0,\ldots , 2^r-1\}$ s.t. $|i|_1 = |j|_1$, $\varphi_i = \varphi_j$, where $|x|_1$ is the Hamming weight of the binary representation of $x$. As a consequence, for any $\varphi\in \mathcal S$, $\exists a_0, \ldots ,a_r\in \mathbb C$ s.t. $\varphi = \sum_{h=0}^na_h\varphi^{(h)}$ where $\varphi^{(h)}\in \mathbb C^{2^r}$ is defined as $\varphi^{(h)}_i=\begin{cases}1&\text{if $|i|_1 = h$}\\0&\text{otherwise}\end{cases}$. Thus $\mathcal S$ is of dimension at most $r+1$.  Moreover, for any $\alpha\in \mathbb R$, $\interp{\theta_r(\alpha)}\in \mathcal S$, so $\mathcal S \subseteq \mathcal S_r:= \mathop{\mathrm{span}} \{ \interp{\theta_r(\alpha)}~|~\alpha \in \mathbb{R}\}$. Since $\mathcal S_r$ is of dimension $r+1$ (see proof of Lemma <ref>), $\mathcal S=\mathcal S_r$.

As a consequence $\interp D\in \mathcal S_r$, so $\interp {P_r}\circ \interp {D(\vec \alpha)} = \interp {D(\vec \alpha)}$, since, according to Lemma <ref> for any $\alpha\in \mathbb R$, $\interp{P_r\circ \theta_r(\alpha)}= \interp {\theta_r(\alpha)}$. Thus, $\zxct\vdash P_r\circ D(\vec \alpha)$ thanks to Theorem <ref>.

\[\forall\alpha,\beta\in\mathbb{R}^2,\quad \zxct\vdash\tikzfig{new-supplementarity}\]

Indeed, simply by decomposing the colour-swapped version of using , we can derive:

\[\forall\alpha\in\mathbb{R},\quad\zxct\vdash \tikzfig{decomposed-supp}\]

Now we just need to apply Theorem <ref> with
$\tikzfig{diag-substitution-gen-supp-arxiv}$ which is clearly symmetrical:

\begin{align*}
\tikzfigc{00}
\eq{}\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{}\tikzfigc{03}
\end{align*}

§ COMPLETENESS FOR THE GENERAL ZX-CALCULUS

The previous result on linear diagrams gives a lot of power to the axiomatisation $\zxct$. We want now to complete this axiomatisation for the unrestricted ZX-Calculus, i.e. we want to add enough axioms to $\zxct$ so that the resulting axiomatisation makes the general ZX-Calculus complete. This problem has been addressed in [23], although to answer it, the authors added two generators to the language, and built a set of rules involving around 25 axioms. In the following, we show that we only need to add one axiom to $\zxct$.

§.§ Incompleteness

The axiomatisation $\zxct$ is complete for the Clifford+T quantum mechanics  –i.e. the $\frac \pi 4$-fragment–, but is not complete in general:

There exist two ZX-diagrams $D_1$ and $D_2$ such that:

\[\interp{D_1}=\interp{D_2}\qquad\text{and}\qquad \zxct\nvdash D_1=D_2\]

Consider the following equation:

\[\tikzfig{incomplete-pi_3}\]

This equation is sound, it represents

However, consider the interpretation $\interp{.}_9$ that multiplies all the angles by $9$. All the multiples of $\frac{\pi}{4}$ remain unchanged ($\frac{k\pi}{4}\times9=\frac{k\pi}{4}+2k\pi=\frac{k\pi}{4}$). It is then easy to show that all the rules of $\zxct$ hold with this interpretation. However:

\[\interp{\tikzfigc{00}}_9\eq{}\tikzfigc{01}\ \neq\ \tikzfigc{02}\eq{}\interp{\tikzfigc{02}}_9\]

Indeed the left hand side amounts to $4$ while the right hand side amounts to $1$.
Since all the rules of $\zxct$ hold with this interpretation, if the calculus were complete, then it would prove the above equation and so its interpretation would hold. It does not, so the ZX-Calculus is not complete.

Notice that thanks to Theorem <ref>, a completion of the ZX calculus would imply to  add  either non linear axioms, or axioms with constants not multiple of $\pi/4$. Such potential axioms have already been discovered, for instance the cyclotomic supplementarity [27]:

\[\tikzfig{cyclo-supp}\quad\text{(SUP}_n\text{)}\]

Adding this family of axioms to those of $\zxct$ would nullify the counterexample in the proof of <ref> (the equality is derivable from $\zxct+\textnormal{(SUP$_3$)}$). However, the ZX-Calculus, with this set of axioms, would still be incomplete. Indeed, the argument given in [27] still holds here.

In the following, we actually show that adding one axiom to $\zxct$ is sufficient to get the completeness in general. Contrary to the axioms of $\zxct$, this one manipulates angles in a non-linear fashion.

§.§ From ZX to ZW

Both the ZX-Calculus and the -Calculus are universal for complex matrices, so there exists a pair of translations between the two languages which preserve the semantics ($[.]_X: \zwc\to \zx$ and $[.]_W:\zx\to \zwc$ s.t. $\forall D\in \zx, \interp{[D]_W}=\interp D$ and $\forall D\in \zwc, \interp{[D]_X}=\interp D$). The axiom has been chosen so that we can prove that $\left(\zxct+\add\right)\vdash {[[D]_W]_X}= D$ for any generator $D$ of the ZX-calculus and that $\left(\zxct+\add\right)\vdash [D_1]_X=[D_2]_X$ for any axiom $D_1=D_2$ of the ZW-Calculus. The choice of the translations is however essential as the new axiom relies on them.

In [30, 23], the authors already use the same proof technique – i.e. transporting the completeness from $\zwc$ to ZX –, and hence provide two interpretations from ZX to $\zwc$ and back. The former, that we denote $[.]_W$ absolutely suits our needs:

$$\tikzfig{empty-diagram} \quad\mapsto\quad \tikzfig{empty-diagram}\qquad\qquad
\tikzfig{single-line} \quad\mapsto\quad \tikzfig{single-line}\qquad\qquad\tikzfig{ZW-to-ZX-braid-no-braid}$$

$$\tikzfig{caps} \quad\raisebox{0.3em}{$\mapsto$}\quad \tikzfig{caps}\hspace{6em}
\tikzfig{cup} \quad\raisebox{0.3em}{$\mapsto$}\quad \tikzfig{cup}$$

\tikzfig{hadamard-ZX-to-ZW}$$

$$\tikzfig{rn-alpha-2}\mapsto\left[~\tikzfig{Hadamard}~\right]_W^{\otimes m}\circ \left[\tikzfig{gn-alpha-2}\right]_W\circ \left[~\tikzfig{Hadamard}~\right]_W^{\otimes n}

$$D_1\circ D_2\mapsto [D_1]_W\circ[D_2]_W\qquad\quad D_1\otimes D_2\mapsto [D_1]_W\otimes[D_2]_W$$

§.§ From ZW$\!_{\mathbb{C}}$ to ZX

The $[.]_X$ translation
has already been partially defined in Section <ref>. To extend it to the generalised white spider present in , the main subtlety is the encoding of positive real numbers
in the ZX-diagrams.
In [30], the authors decompose, roughly speaking, a positive real number  into its integer part and its non-integer part.
Our translation relies on a different (although not unique) decomposition:

\[\forall z\in\mathbb{C},~~ \exists (n,\theta,\beta)\in\mathbb{N}\times[0;2\pi)\times\left[0;\frac{\pi}{2}\right],\quad z=2^n\cos(\beta)e^{i\theta}\]

$$\tikzfig{empty-diagram} \quad\mapsto\quad \tikzfig{empty-diagram}\qquad\qquad
\tikzfig{single-line} \quad\mapsto\quad \tikzfig{single-line}\qquad\qquad\tikzfig{ZW-to-ZX-braid-no-braid}$$

$$\tikzfig{caps} \quad\raisebox{0.3em}{$\mapsto$}\quad \tikzfig{caps}\hspace{6em}
\tikzfig{cup} \quad\raisebox{0.3em}{$\mapsto$}\quad \tikzfig{cup}$$

\tikzfig{ZW-to-ZX-dot-1-1}\\\\
\tikzfig{ZW-to-ZX-cross-no-braid}
\end{array} \qquad\quad
\tikzfig{ZW-to-ZX-dot-1-2}

$$D_1\circ D_2\mapsto [D_1]_X\circ[D_2]_X\quad\qquad D_1\otimes D_2\mapsto [D_1]_X\otimes[D_2]_X$$

$n$ is well-defined: Every complex number $x\neq0$ can be expressed as $\rho e^{i\theta}$ where $\rho\in\mathbb{R}^*_+$. If $x=0$, then $n:=0$. However, $\theta$ may take any value, but it makes no difference (see Section <ref> in appendix).

We may prove the two following propositions:

\[\left(\zxct+\add\right)\vdash D = [[D]_W]_X\]

Proof in appendix at Section <ref>.

\[\zwc\vdash D_1=D_2 \implies \left(\zxct+\add\right)\vdash [D_1]_X=[D_2]_X\]

Proof in appendix at Section <ref>.

The completeness of the calculus is now easy to prove:

Let $D_1$ and $D_2$ be two diagrams of the ZX-Calculus such that $\interp{D_1}=\interp{D_2}$. Since $[.]_W$ preserves the the semantics, $\interp{[D_1]_W}=\interp{[D_1]_W}$. By completeness of the -Calculus, $\zwc\vdash [D_1]_W=[D_2]_W$. By Proposition <ref>, $\left(\zxct+\add\right)\vdash [[D_1]_W]_X=[[D_2]_W]_X$. Finally, by Proposition <ref>, $\left(\zxct+\add\right)\vdash D_1=D_2$ which completes the proof.

§ DISCUSSION ON THE NEW AXIOMS

commutation-of-controls-general-simplified as a Commutation of Controlled Operations

A controlled operation is a fairly common concept in quantum circuits. Let $U$ be an $n\to n$ diagram representing a unitary. Then, a larger diagram $n+1\to n+1$, denoted $\Lambda U$, is considered a controlled $U$ if:

\[\tikzfig{controlled-U-ket-0}\qquad\qquad\tikzfig{controlled-U-ket-1}\]

The leftmost wire in $\Lambda U$ has a particular function: it is called the control wire. When classical data is plugged on this wire, you recover this data at the end of the operation. Plus, if $\ket0$ is plugged, the identity is recovered on the $n$ right wires, whilst if $\ket1$ is plugged, then $U$ is recovered on the right. For instance, the following diagram can be considered as $\Lambda R_Z(2\alpha)$: controlled-RZ-alpha, because

\[\tikzfig{controlled-RZ-alpha-ket-0}\qquad\text{ and }\qquad\tikzfig{controlled-RZ-alpha-ket-1}\]

One can easily reverse the roles of $\ket0$ and $\ket1$ in $\Lambda U$ by adding rn-pi-1-1 before and after the controlled operation on the control wire. The result, denoted $\overline{\Lambda}U$:

\[\tikzfig{anti-controlled-U}\]

is called an anti-controlled operation. The identity is obtained when $\ket1$ is plugged on the control wire, and $U$ when $\ket0$ is plugged.

Controlled operations haves a nice matrix interpretation: $\interp{\Lambda U} = \begin{pmatrix}I_{2^n} & 0 \\ 0 & \interp{U}\end{pmatrix}$, as well as anti-controlled operations: $\interp{\overline{\Lambda} U} = \begin{pmatrix} \interp{U} & 0 \\ 0 & I_{2^n} \end{pmatrix}$. An interesting property of controlled and anti-controlled operations, that can easily be seen thanks to the interpretation, is that they commute: $\interp{\Lambda U \circ \overline{\Lambda}V} = \interp{\overline{\Lambda}V \circ \Lambda U} = \begin{pmatrix}\interp{V} & 0 \\ 0 & \interp{U}\end{pmatrix}$.

Now, let $U(\beta)=R_Z(2\beta)\otimes \mathbb{I}=~\tikzfig{V-for-C}$ and $V(\alpha,\gamma) =~ \tikzfig{U-for-C}$. Then we can consider the following diagrams as $\Lambda U(\beta)$ and $\overline{\Lambda}V(\alpha,\gamma)$:

$$\Lambda U(\beta):=~\tikzfig{controlled-V-for-C}$$

These two diagrams should commute. The rule expresses this equality in a ZX-style, i.e. with redundant information being cropped out of the picture. Indeed, if we ignore the scalars – that are invertible –, we get on the one hand:

\begin{align*}
\tikzfigc{00}
\eq{}\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{}\tikzfigc{03}
\end{align*}

And on the other hand:

\begin{align*}
\tikzfigc{00}
\eq{}\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{}\tikzfigc{03}
\end{align*}

Hence the two equations are equivalent under the ZX-rules for Clifford.

add-axiom-3 as a Sum of Two Controls

First of all, let us notice that the following pattern, which can be found three times in , has interpretation:

\[\interp{\tikzfig{control-cos}}=\sqrt{2}\begin{pmatrix}1\\e^{i\theta}\cos(\alpha)\end{pmatrix}\]

Such a diagram can be seen as a controlled scalar. Up to the global scalar $\sqrt{2}$, if $\bra0$ is plugged at the bottom, we get $1$, but if $\bra1$ is plugged, then we get $e^{i\theta}\cos(\alpha)$. Two of occurrences of this pattern are plugged to the following pattern, with interpretation:

\[\interp{\tikzfig{add-part-of-A}}=\frac{\sqrt{2}\piq{}}{2}\begin{pmatrix}1&0&0&0\\0&\frac{1}{\sqrt{2}}&\frac{1}{\sqrt{2}}&0\end{pmatrix}\]

If two controlled scalars $\begin{pmatrix}1\\x\end{pmatrix}$ and $\begin{pmatrix}1\\y\end{pmatrix}$ are plugged on top, we get:

\[\frac{\sqrt{2}\piq{}}{2}\begin{pmatrix}1&0&0&0\\0&\frac{1}{\sqrt{2}}&\frac{1}{\sqrt{2}}&0\end{pmatrix}\begin{pmatrix}1\\y\\x\\xy\end{pmatrix}=\frac{\sqrt{2}\piq{}}{2}\begin{pmatrix}1\\\frac{1}{\sqrt{2}}(x+y)\end{pmatrix}\]

In our case, $x = e^{i\theta_1}\cos(\alpha)$ and $y = e^{i\theta_2}\cos(\beta)$. For any two such numbers, there exist $\theta_3$ and $\gamma$ such that $e^{i\theta_1}\cos(\alpha)+e^{i\theta_2}\cos(\beta) = 2e^{i\theta_3}\cos(\gamma)$. Hence:

\[\interp{\tikzfig{add-axiom-left-up}}=\sqrt{2}\piq{}\begin{pmatrix}1\\\sqrt{2}e^{i\theta_3}\cos(\gamma)\end{pmatrix}=\piq{}\begin{pmatrix}1&0\\0&\sqrt{2}\end{pmatrix}\sqrt{2}\begin{pmatrix}1\\e^{i\theta_3}\cos(\gamma)\end{pmatrix}\]

The term $\sqrt{2}\begin{pmatrix}1\\e^{i\theta_3}\cos(\gamma)\end{pmatrix}$ can be represented by the first pattern. The term $\piq{}\begin{pmatrix}1&0\\0&\sqrt{2}\end{pmatrix}$, however, can be represented by normaliser-part-of-A.

We end up with:

\[\tikzfig{add-axiom-3}\]

§ PARAMETRISATION OF THE TRIANGLE

In this section we go further, and make the triangle a generator of the language. However, contrary to [30, 23], where a $\lambda$-box has been introduced to meet the ring structure of , this property will be achieved by the triangle itself, for it is allowed a parameter:

\[\mathrm{\Delta}(r):1\to1\qquad\tikzfig{param-triangle}\qquad\text{where}\qquad
\forall r\in\mathbb{C},~~\interp{\tikzfig{param-triangle}}=\begin{pmatrix}1&r\\0&1\end{pmatrix}\]

This parametrisation changes the fundamental nature of the ZX-calculus. It leads to a new language in which a phase group and the ring structure coexist. An axiomatisation is proposed in Figure <ref>.

Set of rules for the ZX-Calculus with parametrised triangles.

We claim that our calculus is simpler than the one presented in [30]. In this new version of the ZX-Calculus, the interpretation of the parametrised triangle in $[.]_W$ is:

\[\tikzfig{param-triangle-ZX-to-ZW}\]

while the interpretation in ZX $[.]_X$ of the white dot is simplified:

\[\tikzfig{ZW-white-dot-to-ZX-param-triangle}\]

Here again, we define the parametrised green triangle, as well as the triangle with no parameter (which happens to be the same as the one we introduced before):

\[\tikzfig{param-green-triangle-definition}\hspace{6em}\tikzfig{triangle-1-def}\]

Indeed, notice that using with $\alpha = \frac{\pi}{4}$, we get the initial definition of the triangle, up to a scalar that can be dealt with.

The set of rules for Clifford+T is deducible from the set $\zxt$ in Figure <ref>.

All the rules of the Clifford+T fragment except are expressed in the set $\zxt$. Instead, this rule is replace by (BW') in , but the two are equivalent as shown in Lemma <ref>.

As a corollary, we can prove any equality between two diagrams of the Clifford+T fragment using . We may now wonder if we can have a theorem for the new language similar to Theorem <ref>. To do so we need to update our notion of linear diagrams, for now, there can be two kinds of parameters, that we need to distinguish: the ones in green and red nodes, that follow a group structure, and the ones in triangles, that follow a ring structure:

A -diagram is linear in $(\vec \alpha, \vec r)$ with constants in $C\subseteq \mathbb R$, if it is generated by $R_Z^{(n,m)}(E_\alpha)$, $R_X^{(n,m)}(E_\alpha)$, $\mathrm{\Delta}(E_r)$, $H$, $e$, $\mathbb I$, $\sigma$, $\epsilon$, $\eta$, and the spacial and sequential compositions, where $n,m\in \mathbb  N$, and:

* $E_\alpha$ is of the form $\sum_{i} n_i \alpha_i+c$, with $n_i\in \mathbb Z$ and $c\in C$

* $E_r$ is of the form $\sum_{i} n_i r_i+p$, with $n_i\in \mathbb Z$ and $p\in \mathbb{Z}$

It may look strange that $E_r$ has coefficients and constants in $\mathbb{Z}$ since the triangle should be able to hold any complex parameter. This choice actually simplifies the proof of the following theorem. Although, once we have the completeness (Theorem <ref>), the previous definition can obviously be changed with:

* $E_r$ is of the form $\sum_{i} n_i r_i+p$, with $n_i\in \mathbb C$ and $p\in \mathbb{C}$

For any diagrams $D_1(\vec\alpha,\vec r)$ and $D_2(\vec\alpha, \vec r)$ linear in $(\vec\alpha, \vec r)$ with constants in $\frac{\pi}{4}\mathbb{Z}$:

\[\left(\forall (\vec\alpha,\vec r)\in \mathbb{R}^{k_\alpha}\times\mathbb{C}^{k_r},~~\interp{D_1(\vec\alpha, \vec r)}=\interp{D_2(\vec\alpha, \vec r)}\right) \equi{} \zxt \vdash D_1(\vec\alpha, \vec r)=D_2(\vec\alpha, \vec r)\]

To prove this theorem, we will first need a few lemmas (their proofs are in Appendix at page prf:gn-inverse):

The green node gn-0-0-alpha has an inverse, denoted $\tikzfig{gn-0-0-alpha}^{-1}$, if $\alpha\neq\pi\mod 2\pi$:

\[\zxt\vdash~~\tikzfig{gn-alpha-inverse}\]

Phases can be extracted from the parameter of a triangle:

\[\tikzfig{param-triangle-times-exp}\]

A triangle with parameter $0$ is the identity:

\[\tikzfig{param-triangle-0}\]

The idea of the proof is to use to recover a diagram of the ZX-Calculus with no triangle, and use Theorem <ref>.

Let $D_1(\vec\alpha, \vec r)$ and $D_2(\vec\alpha, \vec r)$ be two linear diagrams of , such that $\interp{D_1(\vec\alpha, \vec r)}=\interp{D_2(\vec\alpha, \vec r)}$.
For any parametrised triangle, in both diagrams, we first develop its expression:

\[\tikzfig{lin-param-triangle-decomp}\]

Then, we decompose each triangle with parameter $n_jr_j$, distinguishing according to the sign of $n_j$, using , <ref> and <ref>:

\[\begin{array}{c@{\qquad\qquad}c@{\qquad\qquad}c}
n_j = 0: & n_j>0: & n_j < 0:\\
\tikzfig{param-triangle-0} & \tikzfig{lin-param-triangle-decomp-pos} & \tikzfig{lin-param-triangle-decomp-neg}
\end{array}\]

We have:

\begin{align*}
%&\left(\forall (\vec\alpha,\vec r) \in \mathbb{R}^\ell\times\mathbb{C}^k, \interp{D_1(\vec\alpha,\vec r)} = \interp{D_2(\vec\alpha,\vec r)} \right)\\
%&\iff \left(
\begin{array}{l}
\forall (\vec\alpha,\vec \theta,\vec \beta) \in \mathbb{R}^\ell\times [0,2\pi[^k\times [0,\frac{\pi}{2}[^k,\\
\quad\interp{D_1\left(\vec\alpha, \left[e^{i\theta_j}\tan(\beta_j)\right]_j\right)} = \interp{D_2\left(\vec\alpha, \left[e^{i\theta_j}\tan(\beta_j)\right]_j\right)}
\end{array}
\end{align*}

where $\left[e^{i\theta_j}\tan(\beta_j)\right]_j=e^{i\theta_1}\tan(\beta_1),\cdots,e^{i\theta_k}\tan(\beta_k)$.
In order to use , we need to add enough gn-0-0-beta_j to the diagrams. We can easily count the number of occurrences of $r_j$ in $D_1$ and $D_2$, and we define $m_j$ to be the maximum of these two quantities. We add $m_j$ occurrences of gn-0-0-beta_j to both diagrams: $D_i\otimes\left[ \bigotimes\limits_j\left(\tikzfig{gn-0-0-beta_j}\right)^{\otimes m_j}\right]$. Notice that the equation remains sound:

\begin{align*}
&\forall (\vec\alpha,\vec \theta,\vec \beta) \in \mathbb{R}^\ell\times [0,2\pi)^k\times [0,\frac{\pi}{2})^k,\\
&\!\interp{D_1\left(\vec\alpha, \left[e^{i\theta_j}\tan(\beta_j)\right]_j\right)\otimes\left[ \bigotimes\limits_j\tikzfig{gn-0-0-beta_j}^{\otimes m_j}\right]} = \interp{D_2\left(\vec\alpha, \left[e^{i\theta_j}\tan(\beta_j)\right]_j\right)\otimes\left[ \bigotimes\limits_j\tikzfig{gn-0-0-beta_j}^{\otimes m_j}\right]}
\end{align*}

Now, there is enough occurrences of gn-0-0-beta_j in both diagrams to use on all the triangles. We denote $d_i$ the resulting diagrams. These diagrams are triangle free, hence can be assimilated to diagrams of the canonical ZX-Calculus, and are linear in $(\vec\alpha,\vec\theta,\vec\beta)$. Since

$$\forall (\vec\alpha,\vec \theta,\vec \beta) \in \mathbb{R}^\ell\times [0,2\pi)^k\times [0,\frac{\pi}{2})^k,\interp{d_1(\vec\alpha,\vec\theta,\vec\beta)} = \interp{d_2(\vec\alpha,\vec\theta,\vec\beta)}$$

using Theorem <ref>, $\forall(\vec\alpha,\vec\theta,\vec\beta)\in\mathbb{R}^{\ell+2k},~\zxct \vdash d_1(\vec\alpha,\vec\theta,\vec\beta)=d_2(\vec\alpha,\vec\theta,\vec\beta)$. However, thanks to Proposition <ref>, $\forall(\vec\alpha,\vec\theta,\vec\beta)\in\mathbb{R}^{\ell+2k},~\zxt\vdash d_1(\vec\alpha,\vec\theta,\vec\beta)=d_2(\vec\alpha,\vec\theta,\vec\beta)$. Finally, for all $r\in\mathbb{C}$, there exists $(\theta,\beta) \in [0,2\pi)\times [0,\frac{\pi}{2})$ such that $r=e^{i\theta}\tan(\beta)$. Hence,
thanks to Lemma <ref>,
$\forall(\vec\alpha,\vec r)\in\mathbb{R}^\ell\times\mathbb{C}^k,~\zxt\vdash D_1(\vec\alpha, \vec r)=D_2(\vec\alpha, \vec r)$.

Again, this theorem proves to be very useful for proving the derivability of some equations, for instance:

\[\zxt\vdash\tikzfig{add-axiom-2-param-triangle}\]

\[\zxt\vdash\tikzfig{param-triangle-and-param-not-W-commute}\]

The last two lemmas are direct applications of Theorem <ref> while the following requires a bit more work.

\[\forall r,s\in\mathbb{C},~~\zxt\vdash~~\tikzfig{parallel-param-triangles}\]

The proof is in Appendix at page prf:parallel-param-triangles.

After this, it is not hard to show:

The set of rules (in <ref>) is complete for quantum mechanics.

The proof is in Appendix at page prf:completeness-t.

[1]
Scott Aaronson and Daniel Gottesman.
Improved simulation of stabilizer circuits.
Phys. Rev. A, 70:052328, Nov 2004.

[2]
Miriam Backens.
The ZX-calculus is complete for stabilizer quantum mechanics.
In New Journal of Physics, volume 16, page 093021. IOP
Publishing, Sep 2014.

[3]
Miriam Backens.
The ZX-calculus is complete for the single-qubit clifford+t group.
In Bob Coecke, Ichiro Hasuo, and Prakash Panangaden, editors, Proceedings of the 11th workshop on Quantum Physics and Logic,
Kyoto, Japan, 4-6th June 2014, volume 172 of Electronic
Proceedings in Theoretical Computer Science, pages 293–303, 2014.

[4]
Miriam Backens and Ali Nabi Duman.
A complete graphical calculus for Spekkens' toy bit theory.
Foundations of Physics, pages 1–34, 2014.

[5]
Miriam Backens, Simon Perdrix, and Quanlong Wang.
A simplified stabilizer ZX-calculus.
In Ross Duncan and Chris Heunen, editors, Proceedings
13th International Conference on Quantum Physics and Logic, Glasgow, Scotland, 6-10 June 2016, volume 236 of Electronic
Proceedings in Theoretical Computer Science, pages 1–20, 2017.

[6]
Miriam Backens, Simon Perdrix, and Quanlong Wang.
Towards a minimal stabilizer ZX-calculus.
Sep 2017.

[7]
Bob Coecke and Ross Duncan.
Interacting quantum observables: Categorical algebra and
New Journal of Physics, 13(4):043016, Apr 2011.

[8]
Bob Coecke and Aleks Kissinger.
The compositional structure of multipartite quantum entanglement.
In Automata, Languages and Programming, pages 297–308.
Springer Berlin Heidelberg, 2010.

[9]
Bob Coecke and Aleks Kissinger.
Picturing Quantum Processes: A First Course in Quantum Theory
and Diagrammatic Reasoning.
Cambridge University Press, 2017.

[10]
Nicholas Chancellor, Aleks Kissinger, Joschka Roffe, Stefan Zohren, and Dominic
Graphical structures for design and verification of quantum error
arXiv:1611.08012, 2016.

[11]
Bob Coecke and Quanlong Wang.
ZX-rules for 2-qubit Clifford+T quantum circuits, 2018.

[12]
Niel de Beaudrap and Dominic Horsman.
The ZX-calculus is a language for surface code lattice surgery.
CoRR, abs/1704.08670, 2017.

[13]
Ross Duncan and Kevin Dunne.
Interacting Frobenius algebras are Hopf.
In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2016, pages 535–544, New York, NY, USA, 2016. ACM.

[14]
Ross Duncan and Liam Garvie.
Verifying the smallest interesting colour code with quantomatic.
In Bob Coecke and Aleks Kissinger, editors, Proceedings
14th International Conference on Quantum Physics and Logic, Nijmegen, The Netherlands, 3-7 July 2017, volume 266 of Electronic
Proceedings in Theoretical Computer Science, pages 147–163, 2018.

[15]
Ross Duncan and Maxime Lucas.
Verifying the Steane code with Quantomatic.
In Bob Coecke and Matty Hoban, editors, Proceedings of
the 10th International Workshop on Quantum Physics and Logic, Castelldefels (Barcelona), Spain, 17th to 19th July 2013, volume 171 of
Electronic Proceedings in Theoretical Computer Science, pages 33–49.
Open Publishing Association, 2014.

[16]
Ross Duncan and Simon Perdrix.
Rewriting measurement-based quantum computations with generalised
Lecture Notes in Computer Science, 6199:285–296, 2010.

[17]
Ross Duncan and Simon Perdrix.
Pivoting makes the ZX-calculus complete for real stabilizers.
In Bob Coecke and Matty Hoban, editors, Proceedings of
the 10th International Workshop on Quantum Physics and Logic, Castelldefels (Barcelona), Spain, 17th to 19th July 2013, volume 171 of
Electronic Proceedings in Theoretical Computer Science, pages 50–62,

[18]
Ross Duncan.
A graphical approach to measurement-based quantum computing.
In Quantum Physics and Linguistics, pages 50–89. Oxford
University Press, Feb 2013.

[19]
D. Gottesman.
Quantum error correction and fault tolerance.
In Encyclopedia of Mathematical Physics, pages 196–201.
Elsevier, 2006.

[20]
Brett Giles and Peter Selinger.
Exact synthesis of multiqubit Clifford+T circuits.
Phys. Rev. A, 87:032332, Mar 2013.

[21]
Amar Hadzihasanovic.
A diagrammatic axiomatisation for qubit entanglement.
In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer
Science, pages 573–584, Jul 2015.

[22]
Amar Hadzihasanovic.
The Algebra of Entanglement and the Geometry of Composition.
PhD thesis, University of Oxford, 2017.

[23]
Amar Hadzihasanovic, Kang Feng Ng, and Quanlong Wang.
Two complete axiomatisations of pure-state qubit quantum computing.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS '18, pages 502–511, New York, NY, USA, 2018. ACM.

[24]
Clare Horsman.
Quantum picturalism for topological cluster-state computing.
New Journal of Physics, 13(9):095011, Sep 2011.

[25]
Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart.
A complete axiomatisation of the ZX-calculus for Clifford+T
quantum mechanics.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS '18, pages 559–568, New York, NY, USA, 2018. ACM.

[26]
Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart.
Diagrammatic reasoning beyond Clifford+T quantum mechanics.
In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS '18, pages 569–578, New York, NY, USA, 2018. ACM.

[27]
Emmanuel Jeandel, Simon Perdrix, Renaud Vilmart, and Quanlong Wang.
ZX-calculus: Cyclotomic supplementarity and incompleteness for
Clifford+T quantum mechanics.
In Kim G. Larsen, Hans L. Bodlaender, and Jean-Francois Raskin,
editors, 42nd International Symposium on Mathematical Foundations of
Computer Science (MFCS 2017), volume 83 of Leibniz International
Proceedings in Informatics (LIPIcs), pages 11:1–11:13, Dagstuhl, Germany,
2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

[28]
Aleks Kissinger, Lucas Dixon, Ross Duncan, Benjamin Frot, Alex Merry, David
Quick, Matvey Soloviev, and Vladimir Zamdzhiev.
Quantomatic, 2011.

[29]
Aleks Kissinger and Vladimir Zamdzhiev.
Quantomatic: A proof assistant for diagrammatic reasoning.
In Amy P. Felty and Aart Middeldorp, editors, Automated
Deduction - CADE-25, pages 326–336, Cham, 2015. Springer International

[30]
Kang Feng Ng and Quanlong Wang.
A universal completion of the ZX-calculus.
arxiv:1706.09877, 2017.

[31]
Simon Perdrix and Quanlong Wang.
Supplementarity is necessary for quantum diagram reasoning.
In 41st International Symposium on Mathematical Foundations of
Computer Science (MFCS 2016), volume 58 of Leibniz International
Proceedings in Informatics (LIPIcs), pages 76:1–76:14, Krakow, Poland, Aug

[32]
Robert Raussendorf, Daniel E. Browne, and Hans J. Briegel.
Measurement-based quantum computation on cluster states.
Physical Review A, 68(2), Aug 2003.

[33]
Steven Roman.
Field Theory.
Springer, 2006.

[34]
Christian Schröder de Witt and Vladimir Zamdzhiev.
The ZX-calculus is incomplete for quantum mechanics.
In Bob Coecke, Ichiro Hasuo, and Prakash Panangaden, editors, Proceedings of the 11th workshop on Quantum Physics and Logic,
Kyoto, Japan, 4-6th June 2014, volume 172 of Electronic
Proceedings in Theoretical Computer Science, pages 285–292, 2014.

[35]
Peter Selinger.
A survey of graphical languages for monoidal categories.
In New Structures for Physics, pages 289–355. Springer, 2010.

[36]
Yaoyun Shi.
Both Toffoli and controlled-not need little help to do universal
quantum computing.
Quantum Information & Computation, 3(1):84–92, 2003.

[37]
Renaud Vilmart.
A ZX-calculus with triangles for Toffoli-Hadamard,
Clifford+T, and beyond.
In Peter Selinger and Giulio Chiribella, editors, Proceedings of the 15th International Conference on Quantum Physics and
Logic, Halifax, Canada, 3-7th June 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 313–344,

§ LEMMAS FROM $\ZXCT$

In this appendix (<ref>, <ref>) are the proofs of Propositions <ref> and <ref>. To simplify the following work, we use the new node introduced as a notation in Section <ref>, and give a few lemmas in Section <ref>, and prove them in Section <ref>. We try to specify at each step which axiom or previously proven lemma has been used. The spider rule is so natural in ZX and used so many times that we decided not to list it when we use it. Keep in mind that for any provable equation, its upside down version, its colour-swapped version, and (after Lemma <ref>) its version with opposed angles are all provable.

§.§ Lemmas

\[\tikzfig{2-is-sqrt2-squared}\]

\[\tikzfig{hopf}\]

\[\tikzfig{k1}\]

\[\tikzfig{inverse}\]

\[\tikzfig{multiplying-global-phases}\]

\[\tikzfig{bicolor-0-alpha}\]

\[\tikzfig{hadamard-involution}\]

\[\tikzfig{h-loop}\]

\[\tikzfig{lemma-red-pi_2-around-green-node}\]

\[{\tikzfig{6-cycle-bialgebra}}\]

\[\tikzfig{control-pi-and-anti-CNOT-commute-simp}\]

Let $\interp{.}_{-1}$ be the interpretation that multiplies all the angles by $-1$. Then:

\[ \zxct\vdash D_1=D_2 ~~\iff~~ \zxct\vdash \interp{D_1}_{-1}=\interp{D_2}_{-1} \]

\[\tikzfig{gn-pi_2-0-0-equals-sqrt2-exp-pi_4}\]

\[\tikzfig{green-state-pi_2-is-red-state-minus-pi_2}\]

\[\tikzfig{euler-decomp-with-scalar}\]

\[\tikzfig{control-commutation-2}\]

\[\tikzfig{control-commutation-3}\]

\[\tikzfig{supp-to-minus-pi_4}\]

\[\tikzfig{triangle-decomp-2}\]

\[\tikzfig{not-ug-is-symmetrical-2}\]

\[\tikzfig{red-state-on-triangle}\]

\[\tikzfig{pi-red-state-on-triangle}\]

\[\tikzfig{red-state-on-upside-down-triangle}\]

\[\tikzfig{pi-red-state-on-upside-down-triangle}\]

\[\tikzfig{pi-green-state-on-upside-down-triangle}\]

\[\tikzfig{pi-green-state-on-triangle}\]

\[\tikzfig{anti-control-pi-control-green}\]

\[\tikzfig{looped-triangle}\]

\[\tikzfig{lemma-black-dot-swappable-outputs}\]

\[\tikzfig{BW-triangle-no-label}\]

\[\tikzfig{inverse-of-triangle}\]

\[\tikzfig{lemma-symmetric-diagram-with-triangle-hadamard}\]

\[\fit{\tikzfig{anti-control-hanging-branch-and-control-alpha-commute}}\]

\[\tikzfig{ug-and-not-W-commute-simplified}\]

\[\tikzfig{parallel-ugs-are-projections}\]

\[\tikzfig{ug-fork-absorbs-anti-CNOT}\]
\[\tikzfig{ug-fork-absorbs-CNOT}\]

\[\tikzfig{2-diagrams-of-control-triangle-axiom-simplified}\]

§.§ Proof of Lemmas

\begin{align*}
\tikzfigc{00}
\eq{\id}\tikzfigc{01}
\eq{\cp}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\h}\tikzfigc{04}
\end{align*}

Lemmas <ref> and <ref> are proven in [5, 27]. The other lemmas are in the 2 and hence are derivable by completeness of this fragment, since the axiomatisation from [6] can easily be recovered from Lemma <ref>.

The result is quite obvious for all rules except maybe for , and .

* :

\begin{align*}
\tikzfigc{00}\eq{\h}\tikzfigc{01}\eq{\h}
\tikzfigc{02}\eq{\e}\tikzfigc{03}
\end{align*}

* :

\begin{align*}
\tikzfigc{00}\eq{}\tikzfigc{01}\eq{\ref{lem:k1}}
\tikzfigc{02}\eq{\hd}\tikzfigc{03}
\end{align*}

* :

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{01}
\eq{\bw}\tikzfigc{02}
\eq{\picom\\\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{03}
\end{align*}

Moreover, it is to be noticed that $\interp{\tikzfig{ug-node}}_{-1} = \tikzfig{ug-node}$.

\begin{align*}
\tikzfigc{00}
\eq[~]{\e}\tikzfigc{01}
\eq{\h}\tikzfigc{02}
\eq{\hd}\tikzfigc{03}
\eq{\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{04}
\eq{\supp\\\ref{lem:hopf}}\tikzfigc{05}
\eq[~]{\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{06}
\end{align*}

\begin{align*}
\tikzfigc{00}\eq{\h}\tikzfigc{01}\eq{\hd}\tikzfigc{02}\eq{\cp}\tikzfigc{03}\eq{\h\\\ref{lem:gn-pi_2-0-0-equals-sqrt2-exp-pi_4}}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq[]{\hd}\tikzfigc{01}
\eq[]{\h\\\ref{lem:inverse}\\\ref{lem:multiplying-global-phases}}\tikzfigc{02}
\eq[]{\ref{lem:green-state-pi_2-is-red-state-minus-pi_2}}\tikzfigc{03}
\eq[]{\h}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:euler-decomp-with-scalar}\\\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{01}
\eq{\cp}\tikzfigc{02}
\eq[~]{\ccom}\tikzfigc{03}
\eq[~]{\cp}\tikzfigc{04}
\eq{\ref{lem:inverse}\\\ref{lem:multiplying-global-phases}\\\ref{lem:euler-decomp-with-scalar}}\tikzfigc{05}
\end{align*}

By completeness of the 2:

\[{\tikzfig{lemma-for-equivalence-c1}}\]

\begin{align*}
\tikzfigc{00}
\eq{}\tikzfigc{01}
\eq{\ref{lem:C1-original}}\tikzfigc{02}
\eq{\ref{lem:hadamard-involution}}\tikzfigc{03}
\eq{\h\\\ref{lem:2-is-sqrt2-squared}\\\ref{lem:hopf}}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{01}
\eq{\ref{lem:C1-bis}\\\ref{lem:inverse}}\tikzfigc{02}
\eq{\ref{lem:green-state-pi_2-is-red-state-minus-pi_2}\\\ref{lem:multiplying-global-phases}}\tikzfigc{03}
\eq{\ref{lem:euler-decomp-with-scalar}\\\id\\\ref{lem:multiplying-global-phases}}\tikzfigc{04}\\
\eq{\id\\\ref{lem:inverse}\\\ref{lem:hopf}}\tikzfigc{05}
\eq{\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{06}
\eq{\ref{lem:2-is-sqrt2-squared}\\\ref{lem:inverse}}\tikzfigc{07}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{def:triangle}\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{01}
\eq{\h\\\ref{lem:hopf}}\tikzfigc{02}
\eq{\ref{lem:hadamard-involution}\\\ref{lem:C1-original}}\tikzfigc{03}
\eq{\h\\\ref{lem:euler-decomp-with-scalar}\\\ref{lem:multiplying-global-phases}}\tikzfigc{04}\\
\eq{\ref{lem:red-pi_2-around-green-node}\\\ref{lem:hopf}}\tikzfigc{05}
\eq{\ref{lem:euler-decomp-with-scalar}\\\ref{lem:multiplying-global-phases}}\tikzfigc{06}
\eq{\h}\tikzfigc{07}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:triangle-decomp-2}}\tikzfigc{01}
\eq{\ref{lem:6-cycle-bialgebra}}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\ref{lem:triangle-decomp-2}}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{def:triangle}}\tikzfigc{01}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{02}
\eq{\ref{lem:gn-pi_2-0-0-equals-sqrt2-exp-pi_4}}\tikzfigc{03}
\eq{\ref{lem:green-state-pi_2-is-red-state-minus-pi_2}\\\ref{lem:multiplying-global-phases}}\tikzfigc{04}
\eq{}\tikzfigc{05}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{def:triangle}}\tikzfigc{01}
\eq{\ref{lem:k1}\\\cp}\tikzfigc{02}
\eq{\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{03}
\eq{\cp\\\ref{lem:bicolor-0-alpha}}\tikzfigc{04}
\eq{\ref{lem:2-is-sqrt2-squared}\\\ref{lem:inverse}}\tikzfigc{05}
\end{align*}

The result comes naturally from <ref>, <ref> and <ref>.

\begin{align*}
\tikzfigc{00}
\eq[~]{\ref{def:triangle}}\tikzfigc{01}
\eq[~]{\s\\\ref{lem:k1}\\\cp}\tikzfigc{02}
\eq[~]{\supp\\\ref{lem:inverse}\\\ref{lem:hopf}}\tikzfigc{03}
\eq[~]{\cp}\tikzfigc{04}
\eq[~]{\ref{lem:gn-pi_2-0-0-equals-sqrt2-exp-pi_4}}\tikzfigc{05}
\eq[~]{\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{06}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{01}
\eq{\ref{lem:k1}\\\cp}\tikzfigc{02}
\eq{\ref{lem:inverse}\\\ref{lem:pi-green-state-on-upside-down-triangle}}\tikzfigc{03}
\eq{\ref{lem:k1}\\\cp\\\ref{lem:multiplying-global-phases}}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\h}\tikzfigc{01}
\eq{\ref{lem:euler-decomp-with-scalar}\\\id\\\ref{lem:inverse}}\tikzfigc{02}
\eq{\bialg}\tikzfigc{03}
\eq{\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{04}
\eq{\ref{lem:euler-decomp-with-scalar}\\\id}\tikzfigc{05}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{def:triangle}}\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{\ref{def:triangle}}\tikzfigc{03}
\end{align*}

\begin{align*}
\tikzfigc{00}
\quad\eq[]{\ref{def:triangle}}\tikzfigc{01}
\eq{\bialg}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\ref{def:triangle}}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{01}
\eq{\ref{lem:k1}}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\ref{lem:not-triangle-is-symmetrical}\\\id}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq[\quad]{\bialg}\tikzfigc{01}
\eq[\quad]{\s\\\ref{lem:looped-triangle}}\tikzfigc{02}
\end{align*}

\begin{align*}
\tikzfigc{00}\eq{}\tikzfigc{01}
\equi{}\hspace{-1em}\tikzfigc{02}\hspace{-1.5em}\eq{}\tikzfigc{03}
\equi{\picom\\\ref{lem:inverse}\\\id\\\ref{lem:k1}}\tikzfigc{04}\eq{}\tikzfigc{05}\\
\equi{\picom\\\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{06}\eq{}\tikzfigc{07}
\equi{\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{08}\eq{}\tikzfigc{09}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\id\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{01}
\eq{\ref{def:triangle}\\\ref{lem:k1}}\tikzfigc{02}
\eq{\ref{lem:supp-to-minus-pi_4}\\\ref{lem:k1}\\\ref{lem:inverse}\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{03}
\eq{\supp\\\ref{lem:inverse}\\\ref{lem:hopf}}\tikzfigc{04}
\eq{\ref{lem:gn-pi_2-0-0-equals-sqrt2-exp-pi_4}\\\picom}\tikzfigc{05}
\eq{\id\\\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{06}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:euler-decomp-with-scalar}}\tikzfigc{01}
\eq{\ref{lem:multiplying-global-phases}\\\ref{lem:gn-pi_2-0-0-equals-sqrt2-exp-pi_4}\\\id\\\supp}\tikzfigc{02}
\eq{\id\\\picom\\\ref{lem:multiplying-global-phases}\\\ref{lem:k1}}\tikzfigc{03}
\eq{\ref{lem:multiplying-global-phases}\\\ref{lem:supp-to-minus-pi_4}}\tikzfigc{04}\\
\eq{\ref{def:triangle}\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{05}
\eq{\ref{def:triangle}}\tikzfigc{06}
\eq{\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{07}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse-of-triangle}}\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{\h}\tikzfigc{03}
\eq{\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\h}\tikzfigc{01}
\eq{\ref{lem:symmetric-diagram-with-triangle-hadamard}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{02}
\eq{\ref{def:triangle}\\\bialg\\\ref{lem:k1}}\tikzfigc{03}\\
\eq{\h}\tikzfigc{04}
\eq{\ref{lem:C1-original}}\tikzfigc{05}
\eq{\h\\\ref{lem:hopf}}\tikzfigc{06}\\
\eq{\ref{lem:green-state-pi_2-is-red-state-minus-pi_2}}\tikzfigc{07}
\eq{\ref{lem:supp-to-minus-pi_4}\\\id}\tikzfigc{08}
\eq{\ref{lem:inverse}\\\ref{lem:hopf}\\\id}\tikzfigc{09}
\eq{\h}\tikzfigc{10}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}}\!\!\!\!\!\tikzfigc{01}
\eq{\ref{lem:inverse}\\\ref{lem:hopf}\\\id\\\ref{def:triangle}}\tikzfigc{02}
\eq{\bialg\\\ref{lem:inverse}}\tikzfigc{03}\\
\eq{}\tikzfigc{04}
\eq{\ccom}\tikzfigc{05}
\eq{}\tikzfigc{06}
\end{align*}

where the penultimate diagram is the mirror of the previous one with $\gamma:=-\gamma$, so the last step consists in rolling back to the mirror of the initial diagram with $\gamma:=-\gamma$.

\begin{align*}
\tikzfigc{00}
\eq{\id\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{01}
\eq{\ref{def:triangle}\\\ref{lem:k1}}\tikzfigc{02}
\eq{\ref{lem:supp-to-minus-pi_4}\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{03}
\eq{\bialg\\\ref{lem:euler-decomp-with-scalar}}\tikzfigc{04}\\
\eq{\h}\tikzfigc{05}
\eq{\h\\\hd}\tikzfigc{06}
\eq{\picom\\\ref{lem:anti-control-hanging-branch-and-control-alpha-commute}}\tikzfigc{07}
\eq{\hd}\tikzfigc{08}
\eq{\ref{lem:euler-decomp-with-scalar}}\tikzfigc{09}\\
\eq{\ref{lem:control-pi-and-anti-CNOT-commute}}\tikzfigc{10}
\eq{\ref{lem:euler-decomp-with-scalar}}\tikzfigc{11}
\eq{\h\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{12}
\eq{\ref{lem:euler-decomp-with-scalar}\\\ref{lem:multiplying-global-phases}}\tikzfigc{13}
\eq{\ref{lem:supp-to-minus-pi_4}\\\ref{def:triangle}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{14}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:red-pi_2-around-green-node}}\tikzfigc{01}
\eq{\h}\tikzfigc{02}
\eq{\picom\\\ref{lem:C1-original}\\\ref{lem:hadamard-involution}}\tikzfigc{03}
\eq{\hd\\\ref{lem:green-state-pi_2-is-red-state-minus-pi_2}\\\ref{lem:inverse}}\tikzfigc{04}\\
\eq{\ref{lem:inverse}\\\bialg}\tikzfigc{05}
\eq{\ref{lem:inverse}\\\cp\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{06}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{def:triangle}}\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{\ref{def:triangle}\\\ref{lem:supp-to-minus-pi_4}}\tikzfigc{03}
\eq{\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}\\\ref{lem:multiplying-global-phases}\\\ref{lem:euler-decomp-with-scalar}}\tikzfigc{01}
\eq{\bialg}\tikzfigc{02}
\eq{\h}\tikzfigc{03}\\
\eq{\ref{lem:C1-original}}\tikzfigc{04}
\eq{\h\\\ref{lem:hopf}\\\ref{lem:euler-decomp-with-scalar}}\tikzfigc{05}
\eq{\ref{lem:euler-decomp-with-scalar}\\\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{06}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{def:triangle}}\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{\ref{def:triangle}}\tikzfigc{03}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:not-triangle-is-symmetrical}\\\ref{lem:k1}}\tikzfigc{01}
\eq{\ref{lem:not-triangle-is-symmetrical}\\\ref{lem:k1}}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\ref{lem:not-triangle-is-symmetrical}\\\ref{lem:k1}}\tikzfigc{04}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\id\\\ref{lem:not-ug-is-symmetrical}}\tikzfigc{01}
\eq{\h}\tikzfigc{02}
\eq{\ref{lem:symmetric-diagram-with-triangle-hadamard}}\tikzfigc{03}
\eq{\ref{lem:k1}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{04}
\eq{\id\\\cp\\\ref{lem:inverse}}\tikzfigc{05}
\eq{\ref{lem:black-dot-swappable-outputs}\\\ref{lem:n-four}}\tikzfigc{06}
\end{align*}

Moreover, from <ref>, we can easily derive:

\begin{align*}
\tikzfigc{00}
\eq{\id\\\ref{lem:symmetric-diagram-with-triangle-hadamard}}\tikzfigc{01}
\eq{\h\\\ref{lem:k1}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{02}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\id\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{01}
\eq{\ref{lem:symmetric-diagram-with-triangle-hadamard}}\tikzfigc{02}
\eq{\h}\tikzfigc{03}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\h}\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{\ref{lem:k1}\\\ref{lem:n-four}\\\ref{lem:black-dot-swappable-outputs}}\tikzfigc{03}
\eq{}\tikzfigc{04}\\
\eq{\bialg\\\ref{lem:inverse}}\tikzfigc{05}
\eq{}\tikzfigc{06}
\end{align*}

§ PROOF OF PROPOSITIONS <REF> AND <REF>

We first derive an easy but useful lemma for the following:

As shown in Section <ref>:

\[\tikzfig{ZW-to-ZX-dot-1-2-simplified}\]

\begin{align*}
\tikzfigc{00}\mapsto\tikzfigc{01}
\eq{\ref{lem:inverse}\\\ref{lem:hopf}}\tikzfigc{02}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{03}
\eq{\ref{lem:red-state-on-triangle}}\tikzfigc{04}
\eq{\ref{lem:inverse}}\tikzfigc{05}
\end{align*}

§.§ Proof of Proposition <ref>

We prove here that all the rules of the -Calculus are preserved by $[.]_X$.

$\bullet$ X:

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{\bialg}\tikzfigc{02}
\eq{\h}\tikzfigc{03}
\eq{\ref{lem:triangle-hadamard-parallel}\\\ref{lem:h-loop}}\tikzfigc{04}~~\mapsfrom~~\tikzfigc{05}
\end{align*}

$\bullet$ $0a$, $0c$, $0d$ and $0d'$ come directly from the paradigm Only Topology Matters.

$\bullet$ $0b$:

\begin{align*}
\tikzfigc{00}~~\mapsto\tikzfigc{01}
\eq{\ref{lem:k1}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{02}
\eq{\ref{lem:black-dot-swappable-outputs}}\tikzfigc{03}
\eq{\ref{lem:k1}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{04}~\mapsfrom~~\tikzfigc{05}
\end{align*}

$\bullet$ $0b'$: Using the result for rule $0b$,

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{\ref{lem:black-dot-swappable-outputs}}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\ref{lem:black-dot-swappable-outputs}}\tikzfigc{04}~~\mapsfrom~~\tikzfigc{05}
\end{align*}

$\bullet$ $1a$:

\begin{align*}
\tikzfigc{00}~~\mapsto\tikzfigc{01}
\eq{\bialg}\tikzfigc{02}
\eq{\ref{lem:n-four}}\tikzfigc{03}
\eq{\bialg}\tikzfigc{04}~~\mapsfrom~~\tikzfigc{05}
\end{align*}

$\bullet$ $1b$:

\begin{align*}
\tikzfigc{00}~~\underset{\ref{lem:arity-1-black-dot}}{\mapsto}~~\tikzfigc{01}
\eq{\ref{lem:black-dot-swappable-outputs}}\tikzfigc{02}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{03}
\eq{\ref{lem:red-state-on-upside-down-triangle}\\\id\\\ref{lem:inverse}}\tikzfigc{04}
\eq{\id}\tikzfigc{05}~~\mapsfrom~~\tikzfigc{05}
\end{align*}

$\bullet$ $1c$, $1d$, $2a$ and $2b$ come directly from the spider
rules and 𝕀.

$\bullet$ $3a$ is the expression of the colour-swapped version of Lemma <ref>.

$\bullet$ $3b$:

\begin{align*}
\tikzfigc{00}\quad\mapsto\quad\tikzfigc{01}
\eq[\quad]{\ref{lem:k1}}\tikzfigc{02}\quad\mapsfrom\quad\tikzfigc{03}
\end{align*}

$\bullet$ $4$ comes from the spider rule .

$\bullet$ $5a$: We will need a few steps to prove this equality.

\begin{align}\label{step:one}
\tikzfigc{00}
\eq[]{\s\\\bialg}\tikzfigc{01}
\eq[]{\h}\tikzfigc{02}
\eq[]{\ref{lem:triangle-hadamard-parallel}}\tikzfigc{03}
\eq[]{\s\\\ref{lem:k1}}\tikzfigc{04}
\end{align}

\begin{align}\label{step:two}
\tikzfigc{00}
\eq[]{\ref{lem:black-dot-swappable-outputs}}\tikzfigc{01}
\eq[]{\bialg}\tikzfigc{02}
\eq[]{\s\\\ref{lem:triangles-fork-absorbs-anti-CNOT}}\tikzfigc{03}
\eq[]{\ref{lem:k1}}\tikzfigc{04}
\eq[]{\ref{lem:black-dot-swappable-outputs}\\\ref{lem:k1}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{05}
\end{align}

\begin{align}\label{step:three}
\tikzfigc{00}
\eq{\ref{lem:k1}}\tikzfigc{01}
\eq{\ref{lem:n-four}\\\ref{lem:black-dot-swappable-outputs}}\tikzfigc{02}
\eq{\ref{lem:not-ug-is-symmetrical}}\tikzfigc{03}
\eq{\ref{lem:k1}}\tikzfigc{04}
\end{align}

\begin{align}\label{step:four}
\tikzfigc{00}
\eq{\ref{lem:black-dot-swappable-outputs}}\tikzfigc{01}
\eq{\bialg}\tikzfigc{02}
\eq{\ref{lem:k1}}\tikzfigc{03}\\\notag
\eq{\ref{lem:triangles-fork-absorbs-anti-CNOT}}\tikzfigc{04}
\eq{\ref{lem:k1}}\tikzfigc{05}
\end{align}

\begin{align}\label{step:five}
\tikzfigc{00}
\eq{\ref{lem:k1}}\tikzfigc{01}
\eq{\ref{step:four}}\tikzfigc{02}
\eq{\ref{lem:k1}}\tikzfigc{03}
\end{align}

\begin{align}\label{step:six}
\tikzfigc{00}
\eq{\ref{step:one}\\\ref{lem:black-dot-swappable-outputs}}\tikzfigc{01}
\eq{\ref{lem:n-five}}\tikzfigc{02}
\eq{\ref{step:three}\\\ref{lem:k1}\\\ref{lem:hopf}}\tikzfigc{03}\\\notag
\eq{\ref{lem:k1}\\\ref{step:five}}\tikzfigc{04}
\eq{\ref{lem:k1}\\\ref{step:three}}\tikzfigc{05}
\eq{\ref{lem:hopf}\\\ref{step:two}}\tikzfigc{06}
\end{align}

\begin{align}\label{step:seven}
\tikzfigc{00}
\eq{\ref{lem:k1}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{01}
\eq{\bialg}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\bialg}\tikzfigc{04}\\\notag
\eq{\ref{lem:looped-triangle}\\\ref{lem:black-dot-swappable-outputs}}\tikzfigc{05}
\eq{\ref{lem:2-is-sqrt2-squared}\\\ref{lem:triangles-fork-absorbs-anti-CNOT}}\tikzfigc{06}
\eq{\ref{lem:2-is-sqrt2-squared}\\\bialg}\tikzfigc{07}
\eq{\ref{lem:looped-triangle}\\\ref{lem:black-dot-swappable-outputs}}\tikzfigc{08}
\end{align}

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{\ref{lem:hopf}\\\ref{lem:2-is-sqrt2-squared}\\\ref{lem:control-pi-and-anti-CNOT-commute}}\tikzfigc{03}
\eq{\ref{step:seven} \\\ref{lem:hopf}}\tikzfigc{04}\\
\eq{\ref{step:six}}\tikzfigc{05}
\eq{\bialg}\tikzfigc{06}
\eq{\ref{step:seven}\\\ref{lem:hopf}}\tikzfigc{07}~~\mapsfrom\!\!\tikzfigc{08}=\tikzfigc{09}
\end{align*}

$\bullet$ $5b$:

\begin{align*}
\tikzfigc{00}~~\underset{\ref{lem:arity-1-black-dot}}{\mapsto}~~\tikzfigc{01}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{02}
\eq{\ref{lem:red-state-on-triangle}}\tikzfigc{03}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{04}~~\underset{\ref{lem:arity-1-black-dot}}{\mapsfrom}~~\tikzfigc{05}
\end{align*}

$\bullet$ $5c$:

\begin{align*}
\tikzfigc{00}~~\underset{\ref{lem:arity-1-black-dot}}{\mapsto}~~\tikzfigc{01}
\eq{\ref{lem:2-is-sqrt2-squared}}\tikzfigc{02}
\eq{\ref{lem:inverse}}\tikzfigc{03}~~\mapsfrom~~\tikzfigc{03}
\end{align*}

$\bullet$ $5d$:

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{\ref{lem:hopf}}\tikzfigc{02}
\eq{\id}\tikzfigc{03}
\eq{\ref{lem:triangles-fork-absorbs-anti-CNOT}}\tikzfigc{04}
\eq{\ref{lem:inverse}\\\ref{lem:hopf}}\tikzfigc{05}\\
\eq{\ref{lem:pi-red-state-on-triangle}\\\ref{lem:inverse}}\tikzfigc{06}
\eq{\ref{lem:inverse}\\\ref{lem:pi-green-state-on-upside-down-triangle}}\tikzfigc{07}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{08}~~\underset{\ref{lem:arity-1-black-dot}}{\mapsfrom}~~\tikzfigc{09}
\end{align*}

$\bullet$ $6a$: Thanks to the rule X we can get rid of !1emcontrol-pi induced by the crossing. Then,

\begin{align*}
\tikzfigc{00}~~\underset{\text{X}}{\mapsto}~~\tikzfigc{01}
\eq{\bialg}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\ref{lem:parallel-triangles}}\tikzfigc{04}~~\mapsfrom~~\tikzfigc{05}
\end{align*}

$\bullet$ $6b$ is exactly the copy rule .

$\bullet$ $6c$:

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{\ref{lem:inverse}\\\ref{lem:hopf}}\tikzfigc{02}
\eq{\ref{lem:inverse}\\\cp\\\id}\tikzfigc{03}
\eq{\ref{lem:red-state-on-triangle}}\tikzfigc{04}~~\underset{\ref{lem:arity-1-black-dot}}{\mapsfrom}\tikzfigc{05}
\end{align*}

$\bullet$ $7a$:

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq[]{\s\\\h}\tikzfigc{02}
\eq[]{\bialg}\tikzfigc{03}
\eq[]{\h}\tikzfigc{04}~~\mapsfrom~~\tikzfigc{05}
\end{align*}

$\bullet$ $7b$: using <ref>, and :

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{\ref{lem:k1}\\\h}\tikzfigc{02}
\end{align*}

$\bullet$ R$_2$:

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{\ref{lem:hopf}}\tikzfigc{03}~~\mapsfrom~~\tikzfigc{03}
\end{align*}

$\bullet$ R$_3$:

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{}\tikzfigc{02}
\eq{}\tikzfigc{03}~~\mapsfrom~~\tikzfigc{04}
\end{align*}

$\bullet$ $iv$: using 𝕀, , <ref> and <ref>,

\begin{align*}
\tikzfigc{00}~~\mapsto~~\tikzfigc{01}
\eq{\id}\tikzfigc{02}
\eq{}\tikzfigc{03}
\eq{\ref{lem:2-is-sqrt2-squared}\\\ref{lem:inverse}}\tikzfigc{04}
\end{align*}

§.§ Proof of Proposition <ref>

We can show inductively that:

\[\zxct\vdash \left[[D]_W\right]_X\circ\left(\tikzfig{top-composition}\right) = D\otimes \left(\tikzfig{theta}\right)\]

which is the expression of Proposition <ref>.

$\bullet$ The result is obvious for the generators empty-diagram, single-line, crossing, caps, and cup.

$\bullet$ Hadamard:

\begin{align*}
\left[~\tikzfig{hadamard-interpretation-2-no-braid}~\right]_X\hspace{-1em} \eq{} \tikzfigc{00}
\eq{\ref{lem:inverse}}\tikzfigc{01}
\eq{\h\\\ref{lem:k1}}\tikzfigc{02}
\end{align*}

and, using , , <ref>, , <ref> and <ref>:

\begin{align*}
\tikzfigc{00}
\eq{\picom\\\id\\\hd}\tikzfigc{01}
\eq{\h}\tikzfigc{02}
\eq{\ref{lem:inverse}\\\ref{lem:hopf}}\tikzfigc{03}
\eq{\ref{lem:green-state-pi_2-is-red-state-minus-pi_2}}\tikzfigc{04}
\end{align*}

Hence $ \zxct\vdash \left[\left[\tikzfig{Hadamard}\right]_W\right]_X\hspace{0em}\circ\left(\tikzfig{top-composition-1}\right) ~=~~ \tikzfig{Hadamard}\hspace{0.1em}\raisebox{-0.7em}{\tikzfig{theta}}$

$\bullet \left[~\tikzfig{gn-0-1-m-interpretation}~~\right]_X\circ\left(\tikzfig{top-composition-1}\right) = \tikzfig{gn-0-1-m-theta}$

$\bullet \left[~\tikzfig{gn-0-n-1-interpretation}~~\right]_X\circ\left(\tikzfig{top-composition}\right) = \tikzfig{gn-0-n-1-theta}$

$\bullet$ gn-pi_4-1-1:

\begin{align*}
\left[\tikzfig{gn-pi_4-interpretation-2-no-braid}\right]_X \!\!\!\!\eq{} \tikzfigc{00}
\eq{\ref{lem:inverse}\\\h\\\ref{lem:k1}\\\cp}\tikzfigc{01}
\end{align*}

\begin{align*}
\tikzfigc{00}
\eq{\ref{def:triangle}}\tikzfigc{01}
\eq{\ref{lem:supp-to-minus-pi_4}\\\ref{lem:euler-decomp-with-scalar}}\tikzfigc{02}
\eq{\h}\tikzfigc{03}\\
\eq{\ref{lem:C1-original}}\tikzfigc{04}
\eq{\h\\\cp\\\id\\\picom}\tikzfigc{05}
\end{align*}

So that:

\begin{align*}
\tikzfigc{00}
\eq{\hd}\tikzfigc{01}
\eq{\h\\\ref{lem:hopf}\\\ref{lem:not-triangle-is-symmetrical}}\tikzfigc{02}
\eq{}\tikzfigc{03}\\
\eq{\bialg}\tikzfigc{04}
\eq{}\tikzfigc{05}
\eq{\cp}\tikzfigc{06}
\end{align*}

which means $ \zxct\vdash \left[\left[\tikzfig{gn-pi_4-1-1}\right]_W\right]_X\circ\left(\tikzfig{top-composition-1}\right) ~=~~ \tikzfig{gn-pi_4-1-1}\hspace{0.1em}\raisebox{-0.7em}{\tikzfig{theta}}$

$\bullet$ $D_1\circ D_2$:

It is to be noticed that $[D_1\circ D_2]_X=[D_1]_X\circ [D_2]_X$ and $[D_1\otimes D_2]_X=[D_1]_X\otimes [D_2]_X$.
Let us write $\omega = \tikzfig{theta}$. Then:

\begin{align*}
\zxct\vdash \left[[D_1\circ D_2]_W\right]_X\circ(\mathbb{I}\otimes \omega)
&= \left[[D_1]_W\right]_X\circ \left[[D_2]_W\right]_X\circ(\mathbb{I}\otimes \omega)\\
&=  \left[[D_1]_W\right]_X\circ (D_2\otimes \omega) \\&= \left[[D_1]_W\right]_X\circ(\mathbb{I}\otimes \omega)\circ D_2 = (D_1\otimes\omega)\circ D_2 \\
&= (D_1\circ D_2)\otimes \omega
\end{align*}

$\bullet$ $D_1\otimes D_2$:

\begin{align*}
\zxct\vdash&~~\left[[D_1\otimes D_2]_W\right]_X\circ(\mathbb{I}\otimes \omega)
\eq{}\tikzfigc{00}\\
\eq{}\tikzfigc{02}\\
\eq{}\tikzfigc{04}
\eq{}D_1\otimes D_2\otimes\omega
\end{align*}

By compositions, for any diagram $D$, $\zxct\vdash \left[[D]_W\right]_X\circ(\mathbb{I}\otimes \omega) = D\otimes\omega$. Then, using Lemmas <ref> and <ref>:

\begin{align*}
\forall D\in \zxct,\quad
\zxct\vdash \left(\hspace{-0.2em}\scalebox{0.8}{\tikzfig{bottom-composition}}\hspace{-0.3em}\right)\circ\left[[D]_W\right]_X\circ\left(\hspace{-0.2em}\scalebox{0.8}{\tikzfig{top-composition}}\hspace{-0.3em}\right)=D
\end{align*}

§ LINEAR DIAGRAMS

§.§ Proof of Lemma <ref>

\begin{align*}
\tikzfigc{00}
\eq{\h\\\ref{lem:euler-decomp-with-scalar}}\tikzfigc{01}
\eq{\bialg}\tikzfigc{02}\\
\eq{\h}\tikzfigc{03}
\eq{\ref{lem:C1-original}}\tikzfigc{04}
\eq{\h}\tikzfigc{05}\\
\eq{\h\\\ref{lem:hopf}}\tikzfigc{06}
\eq{\ref{lem:green-state-pi_2-is-red-state-minus-pi_2}\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{07}
\eq{\ref{lem:supp-to-minus-pi_4}\\\ref{lem:multiplying-global-phases}}\tikzfigc{08}
\eq{\id\\\ref{lem:hopf}}\tikzfigc{09}
\end{align*}

§.§ Details of the Proof for Corollary <ref>

We first plug the basis $\left(\rx{}, \rx{$\pi$}\right)$ in the input:

* Left hand side:

\begin{align*}
\tikzfigc{00}
\eq{\cp\\\ref{lem:bicolor-0-alpha}}\tikzfigc{01}
\eq{\id\\\ref{lem:green-state-pi_2-is-red-state-minus-pi_2}\\\id\\\ref{lem:2-is-sqrt2-squared}\\\ref{lem:inverse}}\tikzfigc{02}\\
\eq{\bialg}\tikzfigc{03}
\eq{\supp\\\id}\tikzfigc{04}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{05}
\end{align*}

* Right hand side:

\begin{align*}
\tikzfigc{00}
\eq{\vdots}\tikzfigc{01}
\eq{\cp\\\id\\\ref{lem:2-is-sqrt2-squared}\\\ref{lem:inverse}}\tikzfigc{02}
\end{align*}

where the first step was already developed for the left hand side.

The resulting two diagrams are equal when  is plugged.

* $\pi$

* Left hand side:

\begin{align*}
\tikzfigc{00}
\eq{\picom\\\ref{lem:k1}\\\cp}\tikzfigc{01}
\eq{\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{02}
\eq{\ref{lem:hopf}\\\ref{lem:bicolor-0-alpha}\\\ref{lem:inverse}}\tikzfigc{03}
\end{align*}

* Right hand side:

\begin{align*}
\tikzfigc{00}
\eq{\vdots}\tikzfigc{01}
\eq{\picom\\\ref{lem:k1}\\\ref{lem:multiplying-global-phases}}\tikzfigc{02}
\end{align*}

where again the first step was already developed for the left hand side.

Now we could have concluded directly with the help of Corollaries <ref> and <ref>. For the sake of the example, though, we are going to plug our basis on, say, the left hanging branch:

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{01}
\eq{\picom\\\ref{lem:multiplying-global-phases}\\\id\\\ref{lem:2-is-sqrt2-squared}}\tikzfigc{03}
\end{align*}

* $\pi$

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:k1}\\\ref{lem:inverse}\\\cp}\tikzfigc{01}
\eq{\picom\\\ref{lem:multiplying-global-phases}\\\id\\\ref{lem:2-is-sqrt2-squared}}\tikzfigc{03}
\end{align*}

Hence, the two initial diagrams result in the same diagram when the basis is applied. Thanks to Theorem <ref>, the ZX-Calculus proves the equality between the two initial diagrams.

§.§ Details of the Proof for Corollary <ref>

* $\alpha=0$:

* Left hand side:

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{01}
\eq{\ref{lem:2-is-sqrt2-squared}\\\ref{lem:inverse}}\tikzfigc{02}
\end{align*}

* Right hand side:

\begin{align*}
\tikzfigc{00}
\eq{\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{01}
\end{align*}

* $\alpha=\pi$:

* Left hand side:

\begin{align*}
\tikzfigc{00}
\eq{\picom\\\ref{lem:k1}\\\ref{lem:inverse}\\\cp}\tikzfigc{01}
\eq{\ref{lem:2-is-sqrt2-squared}\\\ref{lem:inverse}}\tikzfigc{02}
\end{align*}

* Right hand side:

\begin{align*}
\tikzfigc{00}
\eq{\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{01}
\end{align*}

* $\alpha=\frac{\pi}{2}$:

* Left hand side:

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}\\\picom}\tikzfigc{01}
\eq{\supp}\tikzfigc{02}
\eq{\id}\tikzfigc{03}
\end{align*}

* Right hand side:

\begin{align*}
\tikzfigc{00}
\eq{\picom\\\ref{lem:multiplying-global-phases}\\\cp}\tikzfigc{01}
\eq{\supp}\tikzfigc{02}
\eq{\ref{lem:inverse}\\\cp}\tikzfigc{03}
\end{align*}

The results are the same for three different values of $\alpha$. This is enough to get the equation in Corollary <ref>, according to Theorem <ref>.

§ GENERAL ZX-CALCULUS

§.§ Proof of Proposition <ref>

The result is obvious for cups, caps, single wires, empty diagrams and swaps. Moreover, if we have the result for green dots and the Hadamard gate, then we also have it for red dots by construction.

For green dots, since $n=\max\left(0,\left\lceil \log_2(1)\right\rceil\right)=0$, $\beta = \gamma = 0$:

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}\\\cp\\\ref{lem:2-is-sqrt2-squared}}\tikzfigc{03}
\end{align*}

For Hadamard, first notice:

\begin{align*}
\tikzfigc{00}
\eq{\ref{lem:inverse}\\\cp\\\ref{lem:2-is-sqrt2-squared}}\tikzfigc{02}
\eq{\ref{lem:inverse}\\\picom}\tikzfigc{03}\\
\eq{\ref{lem:gn-pi_2-0-0-equals-sqrt2-exp-pi_4}}\tikzfigc{04}
\eq{\ref{lem:multiplying-global-phases}\\\ref{lem:bicolor-0-alpha}\\\ref{lem:inverse}}\tikzfigc{05}
\end{align*}

since $n=0$, $\beta=\arccos{1/\sqrt{2}}=\pi/4$, $\gamma=\arccos{1}=0$. Finally:

\begin{align*}
\tikzfigc{00}\quad\mapsto\quad\tikzfigc{01}\quad\mapsto\quad
\tikzfigc{02}\eq[\quad]{\s\\\id\\\ref{lem:inverse}}\tikzfigc{03}
\end{align*}

§.§ Lemmas for The General ZX-Calculus

\[\left(\zxct+\add\right)\vdash\tikzfig{add-axiom}\]

\begin{align*}
\left(\zxct+\add\right)\vdash~~\tikzfigc{00}
\eq{Thm~\ref{thm:lin-diag}}\tikzfigc{01}\\
\eq{\add}\tikzfigc{02}
\eq{\ref{lem:supp-to-minus-pi_4}\\\ref{lem:multiplying-global-phases}\\\ref{lem:bicolor-0-alpha}\\\ref{lem:inverse}}\tikzfigc{03}
\end{align*}

where $\cos(\gamma) = \frac{1}{2}(\cos(\alpha-\beta)+ \cos(\alpha+\beta)) = \cos(\alpha)\cos(\beta)$.

We can deduce an equality similar to the rule :

\[\left(\zxct+\add\right)\vdash\tikzfig{add-axiom-3-simplified-2}\]

\begin{align*}
\left(\zxct+\add\right)\vdash~~\tikzfigc{00}
\eq{\ref{lem:supp-to-minus-pi_4}\\\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{01}
\eq{\ref{lem:prod-cos}}\tikzfigc{02}\\
\eq{\ref{lem:prod-cos}}\tikzfigc{03}
\eq{\picom\\\ref{lem:multiplying-global-phases}}\tikzfigc{04}
\eq{\add}\tikzfigc{05}
\end{align*}

where $\cos(\gamma')=\frac{\cos(\gamma)}{\cos(\frac{\pi}{4})}=\sqrt{2}\cos(\gamma)$ and $\cos(\gamma'')=\sqrt{2}\cos(\gamma')=2\cos(\gamma)$. We end up with the right part of the rule , and applying the rule with $\cos(\gamma'')$ gives the wanted condition on the angles.

Let $\rho\in\mathbb{R}+$. Then, for any $n_1,n_2\geq\max\left(0,\left\lceil \log_2(\rho)\right\rceil\right)$:

\[\left(\zxct+\add\right)\vdash~~\scalebox{0.91}{\tikzfig{ZW-white-dot-to-ZX-generalised}}\]

First we prove:

\begin{align*}
\left(\zxct+\add\right)\vdash~~\tikzfigc{00}
\eq{\ref{cor:gen-supp}\\\ref{lem:inverse}\\\ref{lem:hopf}}\tikzfigc{01}
\eq{\ref{lem:prod-cos}}\tikzfigc{02}\\
\eq{\ref{lem:inverse}\\\ref{lem:k1}\\\ref{lem:multiplying-global-phases}}\tikzfigc{03}
\eq{\ref{lem:supp-to-minus-pi_4}}\tikzfigc{04}
\eq{\ref{lem:2-is-sqrt2-squared}\\\ref{lem:multiplying-global-phases}\\\ref{lem:inverse}}\tikzfigc{05}
\end{align*}

We now show the result for $n\geq\max\left(0,\left\lceil \log_2(\rho)\right\rceil\right)$ and $n+1$, which then generalises to lemma <ref> by induction: