Graphical calculi are vital tools for representing and reasoning about quantum circuits and processes.
Some are not only graphically intuitive but also logically complete.
The best known of these is the ZX-calculus,
which is an industry candidate for an Intermediate Representation;
a language that sits between the algorithm designer’s intent and the quantum hardware’s gate instructions.
The ZX calculus, built from generalised Z and X rotations, has difficulty reasoning about arbitrary rotations.
This contrasts with the cross-hardware compiler TriQ which uses these arbitrary rotations to exploit hardware efficiencies.
In this paper we introduce the graphical calculus ZQ,
which uses quaternions to represent these arbitrary rotations, similar to TriQ,
and the phase-free Z spider to represent entanglement, similar to ZX.
We show that this calculus is sound and complete for qubit quantum computing,
while also showing that a fully spider-based representation would have been impossible.
This new calculus extends the zoo of qubit graphical calculi, each with different strengths,
and we hope it will provide a common language for the optimisation procedures of both ZX and TriQ.

§ INTRODUCTION

The purpose of this paper is to introduce a new graphical calculus,
called ZQ,
similar to the already established graphical calculi of ZX, ZW and ZH.
These calculi are universal, sound, and complete
as representations of qubit quantum computing circuits:
Any circuit can be represented as a diagram in any of these calculi,
and two circuits perform the same operation on qubits
if and only if the rules of the calculus show an equality
between the corresponding diagrams.
The ZH calculus [5] and the ZW calculus [11, 12]
are based on the algebraic structure of rings
(for qubit quantum computing we explicitly mean the calculus ).
The ZX calculus and, as we shall see, the ZQ calculus
are instead based on group structures.
This similarity in algebraic structure will
be used to find a translation between the two calculi,
providing us with a method to show the universality and completeness of ZQ,
but also highlights an important difference:
ZQ is built on a non-commutative group,
but we will show that the fundamental building blocks of ZX are restricted to commutative groups.

The ZX calculus is built from the Z and X classical structures of quantum computing, and was introduced in Ref. [8].
Even in that earliest paper the Z `phase shift' is illustrated as a rotation of the Bloch Sphere <cit.>.
By the time of Ref. [3], eight years later,
language had changed to that of Z `rotations' or `angles' <cit.>,
and explicit use is made of the Euler Angle Decomposition result;
that any rotation in 3 can be broken down into rotations about the Z then X then Z axes.
The idea behind the calculus ZQ is to represent not just the Z and X rotations of the Bloch Sphere,
but represent arbitrary rotations via unit-length quaternions.
ZX is built not just from rotations but also from spiders:
Rotations are viewed as acting on individual qubits,
but spiders link multiple qubits, expressing entanglement.
The observation of Ref. [8] is that the
structures of spiders and rotations can be merged
into a single diagrammatic entity,
where each spider (see Figure <ref>) is given a colour, of either green indicating Z or red indicating X,
and a phase, indicating the angle of rotation.

\begin{align*}
\spider{gn}{\alpha} \qquad & \qquad \spider{rn}{\alpha}
\end{align*}

The spiders of ZX can have any number of inputs and outputs,
have a colour of red or green, and are labelled by an angle.
If the angle is 0 it is often omitted.
The colours used in this paper have been chosen such that Z (green) should appear lighter than X (red), even when viewed in greyscale [20].

The Bloch Sphere, which we cover in more detail in <ref>, is not a perfect analogy [26].
Although it provides us with useful intuition and a way to consider a single qubit in real Euclidean space,
its group of rotations, 3, is a subgroup of the group of special unitary evolutions, 2,
which the standard circuit model of quantum computing actually uses [23].
The group 2 itself is isomorphic to the group of unit-length quaternions,
and so we shall use these quaternions as a replacement for 3's rotations,
giving us the `Q' in ZQ.
This use of quaternions to represent rotations is not new to quantum computing [26],
nor other domains such as engineering or computer graphics [24],
but has recently surfaced as a useful component of Intermediate Representations for quantum circuits.
Intermediate Representations sit between the user's specification of an algorithm
and the actual implementation on a specific piece of hardware.
The system TriQ [21]
provides such an Intermediate Representation, targeting existing quantum computers run by IBM, Rigetti, and the University of Maryland.
The authors claim a speed-up in execution of their benchmarks on the seven quantum computers considered,
in part because of TriQ's use of quaternions in the optimisation process <cit.>:
Any sequence of single qubit gates can be combined into just one quaternion,
then decomposed into the most efficient sequence of gates for the target hardware architecture.

Our aims in making ZQ are the following:

* Construct a graphical calculus that succinctly expresses all single qubit operations

* Provide a complete graphical calculus that can express the Intermediate Representation of TriQ

* Construct a qubit graphical calculus whose phases form a non-commutative group

Before we give the definition of ZQ we first give a brief overview of
the Bloch Sphere, the groups 2 and 3, and unit quaternions in <ref>.
In <ref> we describe the graphical calculus ZX,
in <ref> we show why the spiders of ZX are incompatible with non-commutative groups, and then
in <ref> we introduce the graphical calculus ZQ and demonstrate its universality, soundness and completeness.

§ ROTATIONS, QUATERNIONS AND TRIQ

The book `Quantum computation and quantum information' [23]
defines a qubit as a unit vector in $\Hilbert := \bbC^2$,
but notes that if two qubits differ by a unit complex scalar then
they result in the same experimental observations.
The paper `Unit Quaternions and the Bloch Sphere' [26]
instead uses the term spinor for a unit vector in $\Hilbert$,
often represented by a quaternion, with rotations also being represented as quaternions,
and the term qubit to mean a point in the quotient space $\Hilbert / v \sim e^{i \alpha} v$.
We are taking care to highlight this difference
because this paper will take qubits as unit vectors in $\bbC^2 = \Hilbert$
as in Ref. [23]
but will be using quaternions to represent rotations
in a manner related to Ref. [26].
Our reason for this is to make best use of
the $\bbC$-tensor product of $(\bbC^2)^{\tensor n}$,
allowing us to use the paradigm of Categorical Quantum Mechanics [1],
but to also provide a tidy representation of the group of rotations.

[23]
A qubit is a unit vector in $\Hilbert := \bbC^2$.
Two qubits $v$ and $v'$ are considered experimentally indistinguishable
if $v' = e^{i\alpha} v$, defining the equivalence relation $v' \sim v$.
Any qubit $v$ is equivalent via this relation to a vector defined
just using two angles, $\theta$ and $\phi$.

\begin{align}
\ket{0} & := \begin{pmatrix}
1 \\ 0
\end{pmatrix} &
\ket{1} & := \begin{pmatrix}
0 \\ 1
\end{pmatrix} &
v& \sim e^{-i \phi / 2} \cos \half[\theta] \ket{0} + e^{i \phi / 2} \sin \half[\theta] \ket{1}
\end{align}

The space of qubits quotient the relation $\sim$ is called the Bloch Sphere,
with a `qubit up to global phase' given by the spherical coordinates
$(\theta, \phi)$.

The Bloch Sphere is the familiar 2-sphere in 3-dimensional real space.
Accordingly its group of rotations is 3.

This presentation of rotations of the Bloch Sphere corresponds
to the naming of the Pauli $X$, $Y$, and $Z$ matrices
as those that fix the $x$, $y$, and $z$ axes.
This correspondence, however, is imperfect:
The Bloch Sphere has already discarded the global phase,
but the Pauli matrices act on qubits.
Rather than continue to use the language of 3D rotations
we shall instead be using unit quaternions
(via group isomorphism with 2) to label our fundamental, single-qubit evolutions.
Quaternions are a four-dimensional real algebra,
in the same way that the complex numbers are a two-dimension real algebra.

The quaternions, invented by Hamilton in 1843, are a non-commutative, four-dimensional, real algebra:

\begin{align}
\bbR + i\bbR + j \bbR + k \bbR \qquad \qquad
i^2 = j^2 = k^2 = ijk = -1
\end{align}

For ZQ we are only interested in unit-length quaternions, forming the group  under multiplication.
The group  is isomorphic with 2, via the isomorphism:

\begin{align}
\phi: \UQuat & \to \SU2     \label{eqnUQuatSU2} &
q_w + iq_x + jq_y + kq_z & \mapsto \begin{pmatrix}
q_w - iq_z & -q_y + iq_x \\
-q_y-iq_x  & q_w + iq_z
\end{pmatrix}
\end{align}

The proof that this is an isomorphism is given as Proposition <ref>.

At first glance 3 and  may seem to be unrelated mathematical entities, but
there is another way to represent unit-length quaternions, and that is by an angle and a unit vector.
It is important to note that this is not the same thing as `an angle rotation along a unit vector':
The angle-vector pair $(\alpha, \hat v)$ and the angle-vector pair $(-\alpha, -\hat v)$ are different as pairs,
but would constitute the same rotation in 3. This, in fact, describes the relationship between  and 3.

There is a canonical homomorphism from  to 3, given by

\begin{align}
\psi         : \UQuat  &\to \SO3 & (\alpha, v) &:= \cos \half[\alpha] + \sin\half[\alpha](iv_x + jv_y + kv_z)       \\
(\alpha, v) &\mapsto \text{ rotation by angle $\alpha$ along vector $v$} &  \ker \psi  &= \set{1, -1}
\end{align}

The axes $x$, $y$ and $z$ relate these quaternions as rotations (via $\phi$) to the Pauli matrices $X$, $Y$, and $Z$.
Our presentation introduces a scale factor of $\pm i$, similar to that in Ref. <cit.>.

\begin{align}
\phi((\pi, x))                         & =
\begin{pmatrix}
0 & 1 \\
1 & 0
\end{pmatrix} = -iX
\phi((\pi, y))                         & =
\begin{pmatrix}
0  & i \\
-i & 0
\end{pmatrix} = iY
\\
\phi((\pi, z))                         & =
\begin{pmatrix}
1 & 0  \\
0 & -1
\end{pmatrix} = -iZ
\phi((\pi, \frac{x + z}{\sqrt{2}})) & =
\frac{-i}{\sqrt{2}}
\begin{pmatrix}
1 & 1  \\
1 & -1
\end{pmatrix} = -iH
\end{align}

Since unit quaternions can represent the fundamental
single qubit operations (with $\psi$ linking composition of operations
to multiplication of quaternions)
it can be simpler to just use the quaternion representation,
as in the example of the cross-hardware compiler TriQ:

[Quaternions in TriQ]
The compiler TriQ uses quaternions as part of its optimisation process.
[Full-Stack, Real-System Quantum Computer Studies:
Architectural Comparisons and Design Insights [22]]
Since 1Q operations are rotations, each
1Q gate in the [Intermediate Representation] can be expressed using a unit rotation quaternion
which is a canonical representation using a 4D complex number.
TriQ composes rotation operations by multiplying the corresponding
quaternions and creates a single arbitrary rotation. This rotation is
expressed in terms of the input gate set. Furthermore, on all three
vendors, Z-axis rotations are special operations that are implemented
in classical hardware and are therefore error-free. TriQ expresses
the multiplied quaternion as a series of two Z-axis rotations and one
rotation along either X or Y axis, thereby maximizing the
number of error-free operations.

We shall explicitly construct this decomposition of a quaternion
into a Z-X-Z rotation in Proposition <ref>
when we explore how to translate from ZQ to ZX.
With these notions of rotations and quaternions established we turn to the ZX-calculus.

§ THE ZX-CALCULUS

The ZX-calculus is a graphical calculus
similar to the usual quantum circuit notation of e.g. Ref. [23].
We provide here only a brief introduction, for more see Ref. [7].
ZX-diagrams are built from red (X) and green (Z) spiders, as shown in Figure <ref>,
joined by wires.
These spiders can have any number of inputs or outputs,
and they, along with the wires, form the building blocks of the diagrams.
Two diagrams can be placed side by side (horizontal composition, $\tensor$)
or the outputs of one are plugged into the inputs of another above
(vertical composition, $\comp$).
Note that these diagrams are read bottom-to-top,
rather than left-to-right,
but this is purely a matter of convention.

These spiders and wires represent linear maps,
with the notation $\interpret{D}$ indicating the linear map associated with the diagram D (see Figure <ref>).
Indeed the calculus is universal
in that any linear map $M : \Hilbert^{\tensor m} \to \Hilbert^{\tensor n}$
can be represented as a ZX-diagram.
The calculus also comes with a set of rules,
and these rules are complete,
meaning that if two diagrams represent the same linear map
then one can be transformed to the other by the rules.
In fact there are several fragments of ZX,
each of which can be seen as a restriction on the available Z and X rotations,
and each of which has a complete ruleset:
Stabilizer ZX [2],
Clifford+T ZX [15],
various finite subgroups beyond Clifford+T ZX [16],
and the Universal ZX [13].
We shall be looking at just the last of these in this paper,
and the ruleset we shall be considering is given in Figure <ref>.

Note that the rule (EU') of Figure <ref>
includes a long description of the calculation of $\beta_1$, $\beta_2$, $\beta_3$
and $\gamma$.
This is known as a side condition,
and the complexity of the condition stems from the equivalence of different Euler Angle Decompositions.
There are other complete rulesets for Universal ZX [13]  [16],
but each has a side condition requiring the calculation of moduli and arguments of complex numbers.
When we reach the definition of ZQ we will see that there is no such side condition
related to Euler Angle Decompositions[ZQ's side condition in the (Y) rule relates to the transpose.], because
it is inherent in the group action of  and the rule (Q).

\begin{align}
\interpret{\spider{gn}{\alpha}} & = \ketbra{0...0}{0...0} +		e^{i \alpha} \ketbra{1...1}{1...1}  &
\interpret{\ \node{none}{}\ }          & = \begin{pmatrix}		1 & 0 \\ 0 & 1		\end{pmatrix} \\
\interpret{\spider{rn}{\alpha}} & =  \ketbra{+...+}{+...+} +		e^{i \alpha} \ketbra{-...-}{-...-} &
\interpret{\dcap}                  & = \begin{pmatrix}		1 & 0 & 0 & 1		\end{pmatrix}\\
\interpret{\tikzfig{wire/swap}} & =  \begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 0 & 1 & 0 \\
0 & 1 & 0 & 0 \\
0 & 0 & 0 & 1
\end{pmatrix}                                &
\interpret{\dcup}                  & = \begin{pmatrix}		1 \\ 0 \\ 0 \\ 1		\end{pmatrix}
\end{align}

The interpretation of the elements of ZX-calculus diagrams

[]Set of rules ZX for the ZX-Calculus with scalars from Ref. [25]. The right-hand side of (IV) is an empty diagram.
(...) denote zero or more wires, while (45-0.4em$\cdots$) denote one or more wires. In rule (EU'), $\beta_1,\beta_2,\beta_3$ and $\gamma$ can be determined as follows:
$x^+:=\frac{\alpha_1+\alpha_2}{2}$, $x^-:=x^+-\alpha_2$, $z := -\sin{x^+}+i\cos{x^-}$ and $
z' := \cos{x^+}-i\sin{x^-}$, then
$\beta_1 = \arg z + \arg z',
\beta_2 = 2\arg\left(i+\left|\frac{z}{z'}\right|\right),
\beta_3 = \arg z - \arg z',
\gamma = x^+-\arg(z)+\frac{\pi-\beta_2}{2}$
where by convention $\arg(0):=0$ and $z'=0\implies \beta_2=0$.

[Quantum circuits are ZX diagrams]

Quantum circuits constructed
from the universal set of gates shown in Figure <ref>
(the , parameterised Pauli Z, and Hadamard gates [23])
are ZX diagrams.
As shown in that figure each gate has a ZX-calculus analogue.
Other common gates can easily be expressed in terms of these gates,
for example $S := Z_{\frac\pi2}$ and $T := Z_{\frac\pi4}$ as well as $X_\alpha$ and CZ shown below:

\begin{align}\label{eq:zx-derived-gates}
X_\alpha & = \tikzfig{ZX/Xalpha} &
\CZ & = \tikzfig{ZX/CZ}
\end{align}

Gate                               $Z_\alpha$                       H

Circuit Diagram
(Inputs at the bottom)     circuit/CNOT           boxZ_α             boxH

ZX Diagram                     ZX/CNOT                gnα                h

Matrix Interpretation          $\begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 1 & 0 & 0 \\
0 & 0 & 0 & 1 \\
0 & 0 & 1 & 0 \\
\end{pmatrix}$     $\begin{pmatrix}
1 & 0            \\
0 & e^{i \alpha}
\end{pmatrix}$     $\frac{1}{\sqrt{2}}\begin{pmatrix}
1 & 1  \\
1 & -1
\end{pmatrix}$

A universal set of gates for quantum circuits,
their ZX counterparts, and their interpretation as matrices acting on Hilbert space.

Note that there are wires in the depictions of the  and  gates that are horizontal,
and so it is ambiguous whether they are connected to inputs or outputs.
This is a reflection of the `only connectivity matters' rule of ZX;
any deformation of the diagram, provided it preserves the connectivity of the wires,
results in another ZX diagram with the same interpretation.
We can therefore draw horizontal wires without ambiguity.

§ SPIDERS AND NON-COMMUTATIVE GROUPS

Spiders were introduced by Coecke and Duncan in the paper `Interacting Quantum Observables' [9],
and have already been exhibited in this paper as the red and green spiders of ZX.
The Observable Structures of that paper (also called spiders, Definition 6.4)
are commutative monoids over a given $\dagger$-SMC, along with other properties.
This commutativity was then vital to their Decorated Spider Rule <cit.>,
exhibited for ZX as the rule (S) of Figure <ref>.
Our first result will be to show that any monoid acting on $\Hilbert$ is commutative.

In the manner of <cit.>:
A monoid over  is a set $M$ of distinct states in 	and an associative multiplication gate $\mu$.
One of the states, $e$, is the unit for $\mu$.
We depict $\mu$ and the elements of $M$ graphically as:

\begin{align*}
\binary[white]{} & : \bbH^{\tensor 2} \to \bbH &   & \set{\state{white}{m}  : \bbC \to \bbH }_{m \in M} \\
\end{align*}

Every monoid over  is commutative.

The proof of Proposition <ref> is pure linear algebra and is found in <ref>.
Our interest in this result is that only commutative
monoids can be modelled over $\Hilbert$ in a non-degenerate manner.
Since  is a non-commutative group,
and since the action of a group $\mu : G \times G \to G$ is also necessarily a monoid,
this means that we cannot faithfully model the group structure of $\UQuat$
as a monoid over  $\Hilbert$.

There is no monoid over  $\Hilbert$ such that the monoid action $(M, \mu)$ is isomorphic
to the group action of $\UQuat$.

By Corollary <ref> we cannot find a spider
with phases labelled by unit quaternions that would obey the generalised spider
law <cit.>.

§ THE LANGUAGE ZQ

Corollary <ref> shows that we cannot simply
change ZX by labelling spiders with unit quaternions,
and so we have constructed a different approach.
We will use unit quaternion labels on directed edges to indicate rotations,
and use the phase-free Z spiders of ZX to mediate entanglement.
We present the graphical calculus ZQ as a compact closed PROP
generated by the morphisms in Figure <ref>
and then present the interpretation of these generators in Figure <ref>.
We build the transpose of the $Q_q$ node in the usual way, as shown in Figure <ref>.

The graphical calculus ZQ is formed of:

* The generators of Figure <ref>

* The interpretation of Figure <ref>

* The rules of Figure <ref>

The rules of ZQ are sound with respect to the standard interpretation.

This proof is covered in <ref>,
since it amounts to just evaluating each side of each rule.

The rules of ZQ are complete with respect to the standard interpretation.

This proof is covered in <ref>,
and is performed by an equivalence with the ZX calculus, via the translation given in Figure <ref>.

The diagrams of ZQ are universal for linear maps $\Hilbert^{\tensor m} \to \Hilbert^{\tensor n}$.

The translation from ZX diagrams to ZQ diagrams exhibited in Figure <ref>
preserves interpretations (this is shown by inspection of the interpretations), and since ZX is universal therefore ZQ is universal.

p]m1in c m2in
$Z : m \to n$             $\spider{smallZ}{}$     Z spider node

$Q_{q} : 1 \to 1$         $\node{qn}{q}$          $q \in \UQuat$

$\lambda_c : 0 \to 0$     $\lambda_c$             $c \in \bbC$

The generators of ZQ as a PROP

\begin{align}
\node{qnt}{q} & :=  \; \tikzfig{ZQ/q_y}
\end{align}

The transpose of $Q_q$ in ZQ

\begin{align}
\interpret{\spider{smallZ}{}} & =
\begin{pmatrix}
1      & 0 & \dots  &   & 0      \\
0      & 0 & \dots  &   & 0      \\
\vdots &   & \ddots &   & \vdots \\
0      &   & \dots  & 0 & 0      \\
0      &   & \dots  & 0 & 1
\end{pmatrix}
& \interpret{\dcup} & = \begin{pmatrix}
1 \\ 0 \\ 0 \\ 1
\end{pmatrix} \\[\rowgap]
\interpret{\node{qn}{q}}      & =
\begin{pmatrix}
q_w - iq_z & -q_y + iq_x \\
-q_y-iq_x  & q_w + iq_z
\end{pmatrix} \label{eqnZQInterpretQ}&
\interpret{\dcap}             & = \begin{pmatrix}
1 & 0 & 0 & 1
\end{pmatrix}\\[\rowgap]
\interpret{\lambda_c}         & =
\end{align}

Interpretations of the generators of ZQ

\begin{align*}
{\tikzfig{ZQ/q_s_lhs}}                      & \by{S} \spider{smallZ}{}               &
{\tikzfig{ZQ/q_lhs}} & \by{Q} \node{qn}{q_1 \times q_2} \\[2em]
\node{qnt}{q}                               & \by{Y} \node{qn}{\tilde q}             &
\lambda_{-1} \node{qn}{q} & \by{N} \node{qn}{-q}\\[2em]
\node{qn}{1} \by{I_q}                       & \node{none}{} \by{I_z} \node{smallZ}{} &
{\tikzfig{ZQ/q_l3_lhs}} & \by{A} \lambda_{2(q_w-iq_x)}\\[2em]
\lambda_x \lambda_y                         & \by{M} \lambda_{x \times y}            &
\lambda_1 & \by{I_1} \tikzfig{wire/empty} \\[2em]
{\tikzfig{ZQ/q_b_lhs}} \lambda_{-\sqrt{2}i} & \by{B} {\tikzfig{ZQ/q_b_rhs}}          &
{\tikzfig{ZQ/q_cp_lhs}} &\by{CP} {\tikzfig{ZQ/q_cp_rhs}}  \lambda_{\frac{i}{\sqrt{2}}} \\[2em]
{\tikzfig{ZQ/q_phase_lhs}}                  & \by{P} {\tikzfig{ZQ/q_phase_rhs}}      &
\end{align*}

The rules of ZQ.
In rule S the diagonal dots indicate one or more wires, horizontal dots indicate zero or more wires.
The right hand side of rule $I_1$ is the empty diagram,
and $\tilde q$ is the quaternion $q$ reflected in the map $j \mapsto -j$.

Using angle-vector pair notation (Definition <ref>) we also have the interpretation:

\begin{align}
\interpret{\node{qn}{\alpha, v}} & =
\begin{pmatrix}
\cos \frac{\alpha}{2} - i \sin \frac{\alpha}{2} v_z & -i \sin\frac{\alpha}{2} (v_x + i v_y)                \\
- i \sin\frac{\alpha}{2} (v_x - i v_y)              & \cos{\frac{\alpha}{2}} + i \sin\frac{\alpha}{2}{v_z}
\end{pmatrix}  \label{eqnZQInterpretAlpha}
\end{align}

This is the same as the (transpose of the) operators $R_{v}(\alpha)$ or $e^{i\alpha (v \cdot \sigma)}$ <cit.>.
This transpose arises from the choice of $\pm Y$ as the canonical Pauli $Y$ matrix.

In order to decrease diagrammatic clutter we shall use the following notation:

\begin{align}
\hedge & := \node{trap}{\pi, \frac{1}{\sqrt{2}}(x + z)} = \node{qn}{H}
\end{align}

This is a scaled version of the familiar `Hadamard edge' from e.g. [10],
and we will use the shorthand $H$ rather than writing out $\pi, \frac{1}{\sqrt{2}}(x + z)$.
Note that the Hadamard edge is symmetrical,
but the $Q_H$ quaternion edge decoration is not,
and so we will require a lemma to show that this Hadamard edge is well defined:

The Hadamard edge is well defined in ZQ,
in that:

\begin{align}
ZQ \semantic \node{qn}{\text{H}} & = \hedge = \node{qnt}{H} & ZQ \entails \node{qn}{\text{H}} & = \hedge = \node{qnt}{H}
\end{align}

For the semantics:

\begin{align}
\interpret{\node{qn}{\text{H}}} = \frac{-i}{\sqrt{2}}
\begin{pmatrix}
1 & 1  \\
1 & -1
\end{pmatrix} = \interpret{\node{qnt}{H}}
\end{align}

\begin{align}
\node{qnt}{\cos \half[\pi] + \sin\half[\pi](i + k)}
\by{Y}
\node{qn}{\cos \half[\pi] + \sin\half[\pi](i + k)}
\end{align}

§.§ Translation to and from ZX

We define the strict monoidal functors $F_X$ and $F_Q$ on generators in Figure <ref>.
In defining this translation we make use of two facts:
Firstly that we can decompose any unit quaternion into
Z then X then Z rotations. This is tantamount to Euler Angle Decomposition
and is performed explicitly in Proposition <ref>.
Secondly we need to be able to express any complex number
in a rather particular form, which is shown in Lemma <ref>.

\begin{align}
F_Q : &   & ZX \to                                                           & ZQ  \nonumber                                                                                \\
&   & \spider{gn}{\alpha} \mapsto                                      & \tikzfig{ZQ/q_spider_expand} \lambda_{e^{i\alpha/2}}                                                                                \\
&   & \spider{rn}{\alpha} \mapsto                                      & \left(\lambda_i \node{qn}{\text{H}}\right)^{\tensor n}
\comp {\tikzfig{ZQ/q_spider_expand}} \lambda_{e^{i\alpha/2}}
\comp \left(\lambda_i \node{qn}{\text{H}}\right)^{\tensor m} \\
&   & \node{h}{} \mapsto                                               & \node{qn}{\text{H}} \lambda_i                                                                                \\[\rowgap]
F_X : &   & ZQ \to                                                           & ZX \nonumber                                                                                \\
&   & \node{qn}{q} \mapsto                                             & \ \tikzfig{ZX/abc} \galpharpi{-\alpha/2}\nonumber\galpharpi{-\beta/2}\galpharpi{-\gamma/2} \tripleblobs\tripleblobs\tripleblobs    \nonumber \\
&   & \spider{smallZ}{} \mapsto                                        & \spider{gn}{}                                                                                \\
&   & \lambda_{\left(\sqrt{2}\right)^n e^{i\alpha} \cos \beta} \mapsto & \galpharpi{\alpha} \halfblobs \left(\rg{}{\pi}\right)^{\tensor n} \rg{\beta}{-\beta}
\end{align}

Translation from ZQ to ZX and back again.
The existence of $\alpha$, $\beta$ and $\gamma$ when translating the Q node is shown in Proposition <ref>,
likewise the decomposition of any complex number as $\left(\sqrt{2}\right)^n e^{i\alpha} \cos \beta$ is shown in Lemma <ref>.

There exist $\alpha$ and $\gamma \in [0, 2\pi)$, and $\beta \in [0,\pi]$ such that:

\begin{align}
q_w + i q_x + j q_y + k q_z = \left(\cos \frac{\alpha}{2} + k \sin \frac{\alpha}{2}\right)\left(\cos \frac{\beta}{2} + i \sin \frac{\beta}{2}\right)\left(\cos \frac{\gamma}{2} + k \sin \frac{\gamma}{2}\right)
\end{align}

The proof of this lemma is in <ref>.

Any complex number $c$ can be expressed uniquely as $\left(\sqrt{2}\right)^n e^{i\alpha} \cos \beta$ where
$n \in \bbN$, $\alpha \in [0,2\pi)$, $\beta \in [0, \pi)$
and where $n$ is chosen to be the least $n$ such that $\sqrt{2}^n \geq \abs{c}$.

The proof of this lemma is in <ref>.

§ CONCLUSION

This paper introduces the ZQ calculus,
showing it is sound, complete, and universal for qubit quantum computation.
What's more this paper has shown that simply extending the ZX-calculus
to allow arbitrary quaternions as phases would be fundamentally incompatible
with ZX's founding principle of spiders.
Despite this the completeness result for ZQ was shown via an equivalence with the ZX-calculus.

Additionally ZQ is, to the author's knowledge,
the first graphical calculus for qubits that uses a non-commutative phase group.
Indeed the only other qubit graphical calculus that uses a phase group that
is not a subgroup of $[0,2\pi)$
is the graphical calculus for Spekkens' Toy Bit Model in Ref. [4].
This change in algebraic structure allows for the expression of the rules of ZQ
with a far simpler, although not eliminated, appeal to side conditions in comparison with the rules of Universal ZX.

With ZQ now described the author hopes that it will serve
as an Intermediate Representation for quantum circuit synthesis,
allowing it to benefit from the optimisation strategies of both TriQ [22]
and ZX [6, 10, 19].
The optimisation results of TriQ are not solely down to the use of quaternions
but also include routing and gate-decomposition concerns, which we have not addressed here.
Further practical work would include implementing such strategies,
and implementing ZQ in proof assistants such as Quantomatic [17] or PyZX [18].
Further theoretical work would seek to eliminate the reliance on side conditions in the rules of ZQ,
and potentially adapt this calculus to express quaternionic quantum computing directly.

[1]
authorSamson Abramsky &
authorBob Coecke (year2009):
titleCategorical quantum mechanics.
journalHandbook of quantum logic and quantum
structures volume2, pp. pages261–325.

[2]
authorMiriam Backens
(year2014): titleThe ZX-calculus is complete for
stabilizer quantum mechanics.
journalNew Journal of Physics
volume16(number9), p. pages093021,

[3]
authorMiriam Backens
(year2016): titleCompleteness and the
Ph.D. thesis, schoolUniversity of Oxford.

[4]
authorMiriam Backens &
authorAli Nabi Duman
(year2015): titleA Complete Graphical Calculus
for Spekkens’ Toy Bit Theory.
journalFoundations of Physics
volume46(number1), p. pages70–103,

[5]
authorMiriam Backens &
authorAleks Kissinger
(year2019): titleZH: A Complete Graphical
Calculus for Quantum Computations Involving Classical Non-linearity.
journalElectronic Proceedings in Theoretical Computer
Science volume287, p. pages23–42,

[6]
authorMiriam Backens,
authorHector Miller-Bakewell,
authorGiovanni de Felice,
authorLeo Lobski &
authorJohn van de Wetering
(year2020): titleThere and back again: A circuit
extraction tale.

[7]
authorB. Coecke &
authorA. Kissinger
(year2017): titlePicturing Quantum Processes.
publisherCambridge University Press.

[8]
authorBob Coecke & authorRoss
Duncan (year2008):
titleAutomata, Languages and Programming: 35th International
Colloquium, ICALP 2008, Reykjavik, Iceland, July 7-11, 2008, Proceedings,
Part II, chapter chapterInteracting Quantum Observables, pp.
publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, 10.1007/978-3-540-70583-3_25.

[9]
authorBob Coecke & authorRoss
Duncan (year2011):
titleInteracting quantum observables: categorical algebra
and diagrammatics.
journalNew Journal of Physics
volume13(number4), p. pages043016.

[10]
authorRoss Duncan,
authorAleks Kissinger,
authorSimon Perdrix &
authorJohn van de Wetering
(year2019): titleGraph-theoretic Simplification
of Quantum Circuits with the ZX-calculus.

[11]
authorA. Hadzihasanovic
(year2017): titleThe algebra of entanglement
and the geometry of composition.
Ph.D. thesis, schoolUniversity of Oxford.

[12]
authorAmar Hadzihasanovic
(year2015): titleA Diagrammatic Axiomatisation
for Qubit Entanglement.
journal2015 30th Annual ACM/IEEE Symposium on Logic
in Computer Science, 10.1109/lics.2015.59.

[13]
authorAmar Hadzihasanovic,
authorKang Feng Ng &
authorQuanlong Wang
(year2018): titleTwo Complete Axiomatisations of
Pure-State Qubit Quantum Computing.
In: booktitleProceedings of the 33rd Annual ACM/IEEE
Symposium on Logic in Computer Science, seriesLICS ’18,
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, p. pages502–511,

[14]
authorMichiel Hazewinkel,
authorNadiya Gubareni &
authorVladimir V Kirichenko
(year2004): titleAlgebras, rings and modules.
volume1, publisherSpringer Science & Business

[15]
authorEmmanuel Jeandel,
authorSimon Perdrix &
authorRenaud Vilmart
(year2018): titleA Complete Axiomatisation of
the ZX-Calculus for Clifford+T Quantum Mechanics.
journalProceedings of the 33rd Annual ACM/IEEE
Symposium on Logic in Computer Science - LICS ’18,

[16]
authorEmmanuel Jeandel,
authorSimon Perdrix &
authorRenaud Vilmart
(year2018): titleDiagrammatic Reasoning beyond
Clifford+T Quantum Mechanics.
journalProceedings of the 33rd Annual ACM/IEEE
Symposium on Logic in Computer Science - LICS ’18,

[17]
authorA. Kissinger &
authorV. Zamdzhiev
(year2015): titleQuantomatic: A Proof Assistant
for Diagrammatic Reasoning.
journalArXiv e-prints.

[18]
authorAleks Kissinger &
authorJohn van de Wetering
(year2019): titlePyZX: Large Scale Automated
Diagrammatic Reasoning.

[19]
authorAleks Kissinger &
authorJohn van de Wetering
(year2019): titleReducing T-count with the

[20]
authorHector Miller-Bakewell
(year2019): titleZX-calculus and
noteAccessed: 2020-01-23.

[21]
authorPrakash Murali,
authorNorbert Matthias Linke,
authorMargaret Martonosi,
authorAli Javadi Abhari,
authorNhung Hong Nguyen &
authorCinthia Huerta Alderete
(year2019): titleFull-stack, real-system quantum
computer studies.
journalProceedings of the 46th International
Symposium on Computer Architecture - ISCA ’19,

[22]
authorPrakash Murali,
authorNorbert Matthias Linke,
authorMargaret Martonosi,
authorAli Javadi Abhari,
authorNhung Hong Nguyen &
authorCinthia Huerta Alderete
(year2019): titleFull-Stack, Real-System Quantum
Computer Studies: Architectural Comparisons and Design Insights.
In: booktitleProceedings of the 46th International
Symposium on Computer Architecture, seriesISCA ’19,
publisherAssociation for Computing Machinery,
addressNew York, NY, USA, p. pages527–540,

[23]
authorMichael A Nielsen &
authorIsaac L Chuang
(year2010): titleQuantum computation and quantum
publisherCambridge university press,

[24]
authorKen Shoemake (year1985):
titleAnimating Rotation with Quaternion Curves.
journalSIGGRAPH Comput. Graph.
volume19(number3), pp. pages245–254,

[25]
authorRenaud Vilmart
(year2019): titleA Near-Minimal Axiomatisation
of ZX-Calculus for Pure Qubit Quantum Mechanics.
journal2019 34th Annual ACM/IEEE Symposium on Logic
in Computer Science (LICS), 10.1109/lics.2019.8785765.

[26]
authorK B Wharton &
authorD Koch (year2015):
titleUnit quaternions and the Bloch sphere.
journalJournal of Physics A: Mathematical and
Theoretical volume48(number23), p.
pages235302, 10.1088/1751-8113/48/23/235302.

§ COMMUTATIVITY OF MONOIDS OVER HILBERT SPACE PROOF

Taking a generic monoid $M$
we look at the interpretation of the image of the generators of $\monprop_M$.
For brevity we will just write $\interpret{D}$
for $D$ a diagram in $\monprop_M$ to mean the interpretation
of the image of $D$ in the model.
We proceed by looking at the span of the interpretations of the elements of $M$.

\begin{align}
W & := span \set{\interpret{\state{white}{e}},\interpret{\state{white}{a}},\interpret{\state{white}{a'}}, \dots}
\end{align}

* If $\dim W = 0$ then the monoid has only one element, $e$,
and so is commutative.

* If $\dim W > 0$ then
there either $M = \set{e}$ (and so commutative),
or there is some other element $a \in M$.
This implies that $\interpret{\state{white}{e}} \neq 0$, since:

\begin{align}
\text{assume} \quad \interpret{\state{white}{e}} & = 0                                                                       \\
\therefore \interpret{\tikzfig{monoid/md_0}}     & = 0 \quad \text{(any element $a$)}                                        \\
\interpret{\tikzfig{monoid/md_0}}                & = \interpret{\state{white}{a}}  \quad  \text{($e$ is the unit for $m$)}   \\
\therefore \interpret{\state{white}{a}}          & =\interpret{\state{white}{e}}  \contradiction \quad \text{$e$ and $a$ are distinct}
\end{align}

* If $\dim W = 1$ then without loss of generality:

\begin{align}\interpret{\state{white}{e}}                 & = \begin{pmatrix}
1 \\ 0
\end{pmatrix}                                                       \\
\therefore \interpret{\state{white}{a}}      & = \begin{pmatrix}
\lambda_a \\ 0
\end{pmatrix} \; \forall a\; \quad \text{ some } \lambda_a \in \bbC \\
\interpret{\tikzfig{monoid/md_0}}            & = \interpret{\state{white}{a}}  \quad  \text{$e$ is the unit for $m$}              \\
\therefore \interpret{\binary[white]{}}      & = \begin{pmatrix}
1 & \cdot & \cdot & \cdot \\
0 & \cdot & \cdot & \cdot
\end{pmatrix} \text{ where $\cdot$ represents unknowns}             \\
\therefore \interpret{\tikzfig{monoid/md_1}} & = \begin{pmatrix}
\lambda_a \lambda_b \\ 0
\end{pmatrix}= \interpret{\tikzfig{monoid/md_2}}
\end{align}

* if $\dim W = 2$ then the states span all of $\bbC^2$:

\begin{align}
\interpret{\state{white}{e}}                 & = \begin{pmatrix}
1 \\ 0
\end{pmatrix}        \quad \text{w.l.o.g.}                                                               \\
\tikzfig{monoid/md_0}                        & \by{unit_l} \state{white}{a} \quad \forall a                                                                            \\
\therefore \interpret{\tikzfig{monoid/m_2}}  & = \interpret{\node{none}{}} = \interpret{\tikzfig{monoid/m_1}} \quad \text{since } span \set{\state{white}{a}} = \bbC^2 \\
\therefore \interpret{\binary[white]{}}      & = \begin{pmatrix}
1 & 0 & 0 & \cdot \\
0 & 1 & 1 & \cdot
\end{pmatrix} \text{ where $\cdot$ represents unknowns}                                                  \\
\therefore \interpret{\tikzfig{monoid/m_3}}  & = \interpret{\binary[white]{}}                                                                                \\
\therefore \interpret{\tikzfig{monoid/md_1}} & = \interpret{\tikzfig{monoid/md_2}}
\end{align}

§ QUATERNION / ROTATION AND QUATERNION DECOMPOSITION PROOFS

The map $\phi$, given by

\begin{align}
& \phi : & (\text{Unit Quaternions}, \times) & \to (2\times 2\text{ complex matrices}, \comp) \\
& \phi:  & q_w + iq_x + jq_y + kq_z          & \mapsto \begin{pmatrix}
q_w - iq_z & q_y - iq_x \\
-q_y-iq_x  & q_w + iq_z
\end{pmatrix}
\end{align}

is a group homomorphism with trivial kernel.

Write $q_1$ as $w + x + y + z$ and $q_2$ as $w' + x' + y' + z'$:

* Show that $\phi(1) = \begin{pmatrix}
1 & 0 \\ 0 & 1
\end{pmatrix}$:

\begin{align}
\phi(1) = & \begin{pmatrix}
1 - i0 & 0 - i0 \\
-0 -i0 & 1 + i0
\end{pmatrix}
=         \begin{pmatrix}
1 & 0 \\ 0 & 1
\end{pmatrix}
\end{align}

* Show that $\phi(q_1)\phi(q_2) = \phi(q_1 \times q_2)$:

\begin{align}
LHS =         &
\begin{pmatrix}
w - iz & y - ix \\
-y-ix  & w + iz
\end{pmatrix} \comp
\begin{pmatrix}
w' - iz' & y' - ix' \\
-y'-ix'  & w' + iz'
\end{pmatrix} \\
LHS_{(1,1)} = & ( (ww' - zz'-yy' - xx') - i(wz' - xy' + yx' + w'z ) ) \\
LHS_{(1,2)} = & ( ((w -iz)(y' - i x') + (y-ix)(w'+iz'))               \\
=             & ( wy'- zx' + yw'+xz') - i  (wx' + xw' - yz' + zy')    \\
LHS_{(2,1)} = & ( (-y - ix)(w'-iz') + (w+iz)(-y'-ix') )               \\
=             & - (yw' + xz' + wy' - zx') - i (wx' + xw' - yz' + zy') \\
LHS_{(2,2)} = & ( (-y -ix)(y'-ix') + (w + iz)(w' + i z') )            \\
=             & ( ww'-xx'-yy'-zz') +i( wz' -xy' + yx' +zw')           \\
\nonumber\\
RHS_{(1,1)} = & (  ww' - xx'-yy'-zz') - i( wz' + xy'- yx' + zw')      \\
RHS_{(1,2)} = & ( wy' - xz' + yw') + zx' - i( wx' + xw' +yz' - zy')   \\
RHS_{(2,1)} = & -( wy' - xz' + yw') + zx')-i( wx' + xw' +yz' - zy')   \\
RHS_{(2,2)} = & ( ww' - xx'-yy'-zz') + i( wz' + xy'- yx' + zw')
\end{align}

* Show that $\phi(q) = \begin{pmatrix}
1 & 0 \\ 0 & 1
\end{pmatrix} \implies q = 1$:
Looking at the matrix entries individually:

\begin{align}
1 = & \ q_w - iq_z & \implies q_w & = 1 & \text{and}\quad  q_z & = 0 \\
0 = & -q_y - iq_x  & \implies q_y & = 0 & \text{and}\quad  q_x & = 0 \\
\therefore q = & 1
\end{align}

\begin{align}
RHS = & \left(\cos \frac{\alpha}{2} + k \sin \frac{\alpha}{2}\right)\left(\cos \frac{\beta}{2} + i \sin \frac{\beta}{2}\right)\left(\cos \frac{\gamma}{2} + k \sin \frac{\gamma}{2}\right) \\
=     & \left(\cos \frac{\alpha}{2} \cos \frac{\beta}{2} \cos \frac{\gamma}{2} - \sin \frac{\alpha}{2} \cos \frac{\beta}{2} \sin \frac{\gamma}{2}\right) +                                 \\
& i \left(\cos \frac{\alpha}{2} \cos \frac{\beta}{2} \sin \frac{\gamma}{2} + \sin \frac{\alpha}{2} \cos \frac{\beta}{2} \cos \frac{\gamma}{2}\right) + \nonumber                     \\
& j \left(\cos \frac{\alpha}{2} \sin \frac{\beta}{2} \sin \frac{\gamma}{2} - \sin \frac{\alpha}{2} \sin \frac{\beta}{2} \cos \frac{\gamma}{2}\right) + \nonumber                     \\
& k \left(\cos \frac{\alpha}{2} \sin \frac{\beta}{2} \cos \frac{\gamma}{2} + \sin \frac{\alpha}{2} \sin \frac{\beta}{2} \sin \frac{\gamma}{2}\right) \nonumber                       \\
=     & \cos \frac{\beta}{2} \left(\cos \frac{\alpha + \gamma}{2} + i \sin \frac{\alpha + \gamma}{2}\right) +
j \sin \frac{\beta}{2} \left(\sin \frac{\gamma - \alpha}{2} -  i \cos \frac{\gamma - \alpha}{2}\right)\nonumber
\end{align}

From this we gather:

\begin{align}
q_w = & \cos \frac{\beta}{2} \cos \frac{\alpha + \gamma}{2} &
q_x =& \cos \frac{\beta}{2} \sin \frac{\alpha + \gamma}{2} \\
q_y = & \sin \frac{\beta}{2} \sin \frac{\gamma - \alpha}{2} &
q_z =&\sin \frac{\beta}{2} \cos \frac{\gamma - \alpha}{2}
\end{align}

And finally use these to determine values of $\alpha$, $\beta$ and $\gamma:$

* $q_w^2 + q_x^2 = \cos^2 \frac{\beta}{2}$ determines up to two different possibilities of $\beta \in [0, 2\pi)$.
We will enforce $\beta \in [0, \pi]$ to make this unique and $\cos \frac{\beta}{2}$ non-negative.

* If $\beta = 0$ then set $\gamma = 0$, use $q_w$ and $q_x$ to determine $\alpha$

* Likewise if $\beta = \pi$ set $\gamma = 0$, use $q_y$ and $q_z$ to determine $\alpha$

* Otherwise determine $\alpha + \gamma / 2$ from $q_w$ and $q_x$,
and $\alpha - \gamma / 2$ from $q_y$ and $q_z$; their sum and difference give $2\alpha$ and $\gamma$ respectively.

The choices we made in this proof we justify by noting that we can represent these choices
by certain applications of the spider rule (in the case $\beta = 0$) and $\pi$-commutativity rules
(relating $(\alpha, \beta,\gamma) \sim (\alpha + \pi, -\beta, \gamma + \pi)$) in ZX.

Express the complex number $c$ as $re^{i\alpha}$, where $r \in \bbR_{\geq 0}$.
This matches our choice of $\alpha \in [0, 2\pi)$.
For all $r$ there is at least one $n$ where $\sqrt{2}^n \geq r$ and so we can find a least such $n$.
Once we know $n$ there is a unique $\beta \in [0,\pi)$ such that $\cos{\beta} \sqrt{2}^n = r$.

§ SOUNDNESS OF ZQ

In this section we go through each of the rules given in Figure <ref>,
showing that the interpretations of the left and right hand sides of the rules are equal.

The rule S is sound:

\begin{align}
\interpret{{\tikzfig{ZQ/q_s_lhs_dots}}} & = \interpret{\spidermn{smallZ}{}{c+d}{a+b}}
\end{align}

Where there are $k \geq 1$ wires represented by $\ddots$ in the middle of the left hand side.

This is simply a restating of the original Z spider law from <cit.>.

The rule $Q$ is sound:

\begin{align}
\interpret{{\tikzfig{ZQ/q_lhs}}} & = \interpret{\node{qn}{q_1 \times q_2}}
\end{align}

Follows from $\phi$ (see Definition <ref>) being a group isomorphism.
The left hand side is multiplication in 2, the right hand side is multiplication in .

The rule $Y$ is sound:

\begin{align}
\interpret{\node{qn}{q_w + iq_x - jq_y + kq_z}} & = \interpret{\node{qnt}{q_w + iq_x + jq_y + kq_z}}
\end{align}

The action of the cups and caps in Figure <ref>
(where we defined the diagrammatic transpose),
is to enact the transpose in the interpretation:

\begin{align}
\interpret{{\tikzfig{ZQ/q_y}}} =  \begin{pmatrix}
q_w - iq_z & -q_y - iq_x \\
q_y-iq_x   & q_w + iq_z
\end{pmatrix}
=                                 \interpret{\node{qn}{q_w + iq_x - jq_y + kq_z}}
\end{align}

The rule $N$ is sound:

\begin{align}
\interpret{\lambda_{-1} \node{qn}{q}}= \interpret{\node{qn}{-q}}
\end{align}

\begin{align}
LHS =  -1 \begin{pmatrix}
q_w - iq_z & q_y - iq_x \\
-q_y-iq_x  & q_w + iq_z
\end{pmatrix}
=      \begin{pmatrix}
-q_w + iq_z & -q_y + iq_x \\
q_y+iq_x    & -q_w - iq_z
\end{pmatrix} = \, RHS
\end{align}

The rules $I_q$ and $I_z$ are sound:

\begin{align}
\interpret{\node{qn}{1}} = \interpret{\node{none}{}} = \interpret{\node{smallZ}{}}
\end{align}

They all have the interpretation $\begin{pmatrix}
1 & 0 \\ 0 & 1
\end{pmatrix}$.

The rule $A$ is sound:

\begin{align}
\interpret{{\tikzfig{ZQ/q_l3_lhs}}} = \interpret{\lambda_{2(q_w-iq_x)}}
\end{align}

\begin{align}
\interpret{{\tikzfig{ZQ/q_l3_lhs}}} = &
\begin{pmatrix}
1 & 1
\end{pmatrix} \comp
\begin{pmatrix}
q_w - iq_z & q_y - iq_x \\
-q_y-iq_x  & q_w + iq_z
\end{pmatrix} \comp
\begin{pmatrix}
1 \\ 1
\end{pmatrix} \\
=                                     & q_w - iq_z + q_y - iq_x -q_y-iq_x + q_w + iq_z \\
=                                     & 2(q_w - iq_x)                                  \\
=                                     & \interpret{\lambda_{2(q_w - iq_x)}}
\end{align}

The rule $M$ is sound:

\begin{align}
\interpret{\lambda_x \lambda_y} = \interpret{\lambda_{x \times y}}
\end{align}

Both sides have interpretation $x \times y$.

The rule $I_\lambda$ is sound:

\begin{align}
\interpret{\lambda_1} = \interpret{\epsilon}
\end{align}

Where $\epsilon$ is the empty diagram.

Both sides have interpretation $1$.

The rule $B$ is sound:

\begin{align}
\interpret{{\tikzfig{ZQ/q_b_lhs}} \lambda_{-\sqrt{2}i}} = \interpret{{\tikzfig{ZQ/q_b_rhs}}}
\end{align}

\begin{align}
LHS = & -\sqrt{2} i \times \begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 0 & 0 & 1
\end{pmatrix}^{\tensor 2} \comp
\left(\frac{-i}{\sqrt{2}}\begin{pmatrix}
1 & 1 \\ 1 & -1
\end{pmatrix}\right)^{\tensor 4} \comp \\
& \left(id_2 \tensor \begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 0 & 1 & 0 \\
0 & 1 & 0 & 0 \\
0 & 0 & 0 & 1
\end{pmatrix} \tensor \id_2\right) \comp
\begin{pmatrix}
1 & 0 \\
0 & 0 \\
0 & 0 \\
0 & 1
\end{pmatrix}^{\tensor 2} \\
=     & \frac{-i}{\sqrt{2}^3} \begin{pmatrix}
1 & 1  & 1  & 1 \\
1 & -1 & -1 & 1 \\
1 & -1 & -1 & 1 \\
1 & 1  & 1  & 1
\end{pmatrix}                                 \\
RHS = & \left(\frac{-i}{\sqrt{2}}\right)^5 \times \begin{pmatrix}
1 & 1 \\ 1 & -1
\end{pmatrix}^{\tensor 2}
\comp
\begin{pmatrix}
1 & 0 \\
0 & 0 \\
0 & 0 \\
0 & 1
\end{pmatrix} \comp \\ &  \begin{pmatrix}
1 & 1 \\ 1 & -1
\end{pmatrix} \comp
\begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 0 & 0 & 1
\end{pmatrix} \comp  \begin{pmatrix}
1 & 1 \\ 1 & -1
\end{pmatrix}^{\tensor 2} \\
=     & \left(\frac{-i}{\sqrt{2}}\right)^5 \times \begin{pmatrix}
2 & 2  & 2  & 2 \\
2 & -2 & -2 & 2 \\
2 & -2 & -2 & 2 \\
2 & 2  & 2  & 2
\end{pmatrix}
= \frac{-i}{\sqrt{2}^3} \times \begin{pmatrix}
1 & 1  & 1  & 1 \\
1 & -1 & -1 & 1 \\
1 & -1 & -1 & 1 \\
1 & 1  & 1  & 1
\end{pmatrix}
\end{align}

The rule $CP$ is sound:

\begin{align}
\interpret{{\tikzfig{ZQ/q_cp_lhs}}} = \interpret{{\tikzfig{ZQ/q_cp_rhs}}  \lambda_{\frac{i}{\sqrt{2}}}}
\end{align}

\begin{align}
LHS = & \begin{pmatrix}
1 & 1
\end{pmatrix} \comp \frac{-i}{\sqrt{2}} \begin{pmatrix}
1 & 1 \\ 1 & -1
\end{pmatrix} \comp \begin{pmatrix}
1 & 0 & 0 & 0 \\ 0 & 0 & 0 & 1
\end{pmatrix}
=  \frac{-i}{\sqrt{2}} \begin{pmatrix}
2 & 0 & 0 & 0
\end{pmatrix} \\
RHS = & \frac{i}{\sqrt{2}} \left(\begin{pmatrix}
1 & 1
\end{pmatrix} \comp \frac{-i}{\sqrt{2}} \begin{pmatrix}
1 & 1 \\ 1 & -1
\end{pmatrix} \right)^{\tensor 2}
=  \frac{-i}{\sqrt{2}} \begin{pmatrix}
2 & 0 & 0 & 0
\end{pmatrix}
\end{align}

The rule $P$ is sound:

\begin{align}
\interpret{{\tikzfig{ZQ/q_phase_lhs}}} = \interpret{{\tikzfig{ZQ/q_phase_rhs}}}
\end{align}

\begin{align}
LHS = & \begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 0 & 0 & 1
\end{pmatrix} \comp \left(\begin{pmatrix}
q_w - iq_z & 0           \\
0          & q_w + i q_z
\end{pmatrix} \tensor id_2 \right) \\
=     & \begin{pmatrix}
q_w - iq_z & 0 & 0 & 0           \\
0          & 0 & 0 & q_w + i q_z
\end{pmatrix}                                                              \\
RHS = & \begin{pmatrix}
1 & 0 & 0 & 0 \\
0 & 0 & 0 & 1
\end{pmatrix} \comp \left(id_2 \tensor \begin{pmatrix}
q_w - iq_z & 0           \\
0          & q_w + i q_z
\end{pmatrix}\right)  \\
=     & \begin{pmatrix}
q_w - iq_z & 0 & 0 & 0           \\
0          & 0 & 0 & q_w + i q_z
\end{pmatrix}
\end{align}

§ COMPLETENESS OF ZQ

The completion of ZQ is achieved by finding an equivalence between ZQ and ZX as PROPs.
We already know that ZX is complete [13]
and this proof was by a similar equivalence with ZW, which was shown to be complete in Ref. [12].
Equivalence is shown by finding a translation of the generators from ZX to ZQ and vice versa
before then translating all of the rules from ZX into ZQ (<ref>),
and keeping these as rules in ZQ.
Finally one has to ensure that any diagram translated from ZQ to ZX and back again
can be proven to be equivalent to the original ZQ diagram (<ref>).
In symbols this is:

\begin{align}
& \interpret{D_1} = \interpret{D_2} \quad \text{Two diagrams in ZQ} \\
ZX \entails                              & F_X D_1 = F_X D_2                                                 \\
\S\ref{secZXZQTranslatedRules} \entails  & F_Q F_X D_1 = F_Q F_X D_1                                         \\
\S\ref{secCompletenessZXZQBack} \entails & D_1 = F_Q F_X D_1 \qquad \text{and} \qquad D_2 = F_Q F_X D_2      \\
\therefore ZQ \entails                   & D_1 = F_Q F_X D_1 = F_Q F_X D_2 = D_2
\end{align}

§.§ Proving the translated ZX rules

We aim to show that the rules translated from ZX are all derivable from the rules in Figure <ref>, which we will refer to as $ZQ$.
We will use the ZX ruleset from <cit.>, quoted here as Figure <ref>,
and refer to individual ZX rules as $ZX_{\text{rule name}}$.
To save space, we will assume applications of the $M$ rule (scalar multiplication) in the statements of the propositions.

Translation of the Z spider

\begin{align}
ZQ \entails F_Q\left(\spider{gn}{}\right) = \spider{smallZ}{}
\end{align}

\begin{align}
LHS & = {\tikzfig{ZQ/q_spider_0}} \by{I_q} {\tikzfig{ZQ/q_spider_1}} \by{S} \spider{smallZ}{}
\end{align}

Translation of the Z spider rule

\begin{align}
ZQ     & \entails F_Q\left(ZX_S\right)                        \\
\ie ZQ & \entails {\tikzfig{ZQ/q_ts1}} = {\tikzfig{ZQ/q_ts5}}
\end{align}

(The diagonal dots represent at least one wire between the Z spiders)

\begin{align}
& \by{S} {\tikzfig{ZQ/q_ts2}}    \\
\by{P, Y} {\tikzfig{ZQ/q_ts3}}
& \by{Q, S} {\tikzfig{ZQ/q_ts4}} \\
\by{P, Q, S} {\tikzfig{ZQ/q_ts5}}
\end{align}

Translation of the Z spider identity

\begin{align}
ZQ     & \entails  F_Q\left(ZX_{I_g}\right)                                                \\
\ie ZQ & \entails \node{smallZ}{} \comp \node{qn}{1} \comp \node{smallZ}{} = \node{none}{}
\end{align}

\begin{align}
\node{smallZ}{} \comp \node{qn}{1} \comp \node{smallZ}{} \by{I_z} \node{qn}{1}
& \by{I_q} \node{none}{}
\end{align}

Translation of the X spider identity

\begin{align}
ZQ     & \entails F_Q\left(ZX_{I_r}\right)                                                                                \\
\ie ZQ & \entails  \node{qn}{\text{H}} \comp \node{smallZ}{} \comp \node{qn}{1} \comp \node{smallZ}{} \comp \node{qn}{\text{H}} \lambda_i \lambda_i = \node{none}{}
\end{align}

\begin{align}
LHS =    & \node{qn}{\text{H}} \comp \node{smallZ}{} \comp \node{qn}{1} \comp \node{smallZ}{} \comp \node{qn}{\text{H}} \lambda_i \lambda_i \\
\by{I_z} & \node{qn}{\text{H}} \comp \node{qn}{1} \comp \node{qn}{\text{H}} \lambda_i \lambda_i                                             \\
\by{I_q} & \node{qn}{\text{H}} \comp \node{qn}{\text{H}} \lambda_i \lambda_i
\by{Q} \node{qn}{-1} \lambda_i \lambda_i \\
\by{N}   & \node{qn}{1} \lambda_{-1} \lambda_i \lambda_i
\by{I_q}  \node{none}{} \lambda_{-1} \lambda_i \lambda_i
\by{M}  \node{none}{} \lambda_1
\by{I_1}  \node{none}{}
\end{align}

We introduce our first three intermediate lemmas, corresponding to properties of the following three ZX diagrams:

\begin{align}
\rg{\alpha}{\beta} \label{eqnSmallRG} , \qquad \tikzfig{ZX/HH}, \qquad \tikzfig{ZX/HHH}
\end{align}

Interaction of a Z state and Z effect joined by a Hadamard

\begin{align}
ZQ & \entails  {\tikzfig{ZQ/q_alpha_H_beta}} & = \lambda_{-\sqrt{2}\left(\left(\sin\frac{\alpha+\beta}{2}\right) + i \cos\frac{\alpha-\beta}{2}\right)}
\end{align}

\begin{align}
& \by{I_z}  {\tikzfig{ZQ/q_alpha_H_beta3}}
\by{Q} {\tikzfig{ZQ/q_alpha_H_beta4}} \by{A} \lambda_{-\sqrt{2}((\sin\frac{\alpha+\beta}{2}) + i \cos\frac{\alpha-\beta}{2})} \\[\rowgap]
\text{Since } & (\cos \frac{\alpha}{2} + k \sin \frac{\alpha}{2}) \times H \times (\cos \frac{\beta}{2} + k \sin \frac{\beta}{2}) =\nonumber \\
& \frac{1}{\sqrt{2}}(
-\sin\frac{\alpha+\beta}{2} +
i(\cos\frac{\alpha-\beta}{2}) +
j(\sin\frac{\alpha-\beta}{2}) +
\end{align}

Interaction of two Hadamard rotations

\begin{align}
ZQ \entails & \node{qn}{\text{H}} \comp \node{qn}{\text{H}} = \lambda_{-1} \node{none}{}
\end{align}

\begin{align}
\node{qn}{\text{H}} \comp \node{qn}{\text{H}} \by{Q} \node{qn}{H \times H} = \node{qn}{-1} \by{N} \node{qn}{1} \lambda_{-1} \by{I_q} \node{none}{} \lambda{-1}
\end{align}

The value of the scalar describing three Hadamard rotations in parallel

\begin{align}
ZQ \entails {\tikzfig{ZQ/q_HHH}} & = \lambda_{\frac{i}{\sqrt{2}}}
\end{align}

\begin{align}
\by{S,\,\ref{propZQHH}} & \lambda_{-1} {\tikzfig{ZQ/q_HHH2}}          & \by{Y,S} \lambda_{-1}\ {\tikzfig{ZQ/q_HHH3}}                             \\
\by{M, B}               & \lambda_{-i/\sqrt{2}}{\tikzfig{ZQ/q_HHH4}}  & \by{Y,S,I_z} \lambda_{-i/\sqrt{2}}\ {\tikzfig{ZQ/q_HHH5}}                \\
\by{CP, Y}              & \lambda_{i/2\sqrt{2}}{\tikzfig{ZQ/q_HHH6}}  & \by{I_z}  \lambda_{i/2\sqrt{2}}\ {\tikzfig{ZQ/q_HHH7}}                   \\
\by{M,\ref{propZQHH}}   & \lambda_{-i/2\sqrt{2}}{\tikzfig{ZQ/q_HHH8}} & \by{A}  \lambda_{-i/2\sqrt{2}}\ \lambda_{-i\sqrt{2}}\lambda_{-i\sqrt{2}} \\
\by{M}& \lambda_{\frac{i}{\sqrt{2}}}
\end{align}

Translation of the IV rule

\begin{align}
ZQ \entails     & F_Q\left(ZX_{IV}\right)          \\
\ie ZQ \entails & \lambda_{e^{i \frac{\alpha}{2}}}
{\tikzfig{ZQ/q_IV_1}}= \epsilon
\end{align}

\begin{align}
\lambda_{e^{i \frac{\alpha}{2}}}
{\tikzfig{ZQ/q_IV_1}} \by{I_z, I_q, S, M}   & \lambda_{e^{i \frac{\alpha}{2}}}  {\tikzfig{ZQ/q_IV_2}}                                             \\
\by{\ref{lemZQAlphaHBeta}, \ref{propZQHHH}} & \lambda_{e^{i \frac{\alpha}{2}}} \lambda_{-\sqrt{2}ie^{-i \frac{\alpha}{2}}} \lambda_{i / \sqrt{2}} \\
\by{M}                                      & \lambda_{1} \by{I_1} \epsilon
\end{align}

Translation of the CP rule

\begin{align}
ZQ \entails     & F_Q\left(ZX_{CP}\right)                                               \\
\ie ZQ \entails & \lambda_{-1} {\tikzfig{ZQ/q_CP1}} = {\tikzfig{ZQ/q_CP3}} \lambda_{-1}
\end{align}

\begin{align}
LHS \by{1_z, 1_q} & \lambda_{-1} {\tikzfig{ZQ/q_CP2}} \by{A} \lambda_{-1} \lambda_{-i\sqrt{2}}{\tikzfig{ZQ/q_CP2a}}                              \\
\by{CP}           & \lambda_{-1} \lambda_{-i\sqrt{2}} \lambda_{i / \sqrt{2}} {\tikzfig{ZQ/q_CP3}} \by{M} \lambda_{-1} {\tikzfig{ZQ/q_CP3}} = RHS
\end{align}

Translation of the B rule

\begin{align}
ZQ \entails     & F_Q\left(ZX_{B}\right)                                               \\
\ie ZQ \entails & \lambda_{-i}\ {\tikzfig{ZQ/q_b1}} = {\tikzfig{ZQ/q_b4}} \lambda_{-i}
\end{align}

\begin{align}
LHS \by{I_z, I_q} & \lambda_{-i}{\tikzfig{ZQ/q_b2}} \by{B} & \lambda_{-i} \lambda_{i / \sqrt{2}} {\tikzfig{ZQ/q_b3}} \\
\by{A, M, \ref{propZQHH}}&\lambda_{-i} \tikzfig{ZQ/q_b4}
\end{align}

Translation of the H rule

\begin{align}
ZQ \entails     & F_Q\left(H\right)                                                                                \\
\ie ZQ \entails &
\left(\lambda_i \node{qn}{\text{H}}\right)^{\tensor n} \comp
\left(\lambda_i \node{qn}{\text{H}}\right)^{\tensor n} \comp
\lambda_{e^{i\alpha/2}} \comp\\
& \quad \left(\lambda_i \node{qn}{\text{H}}\right)^{\tensor m}  \comp \left(\lambda_i \node{qn}{\text{H}}\right)^{\tensor m} \nonumber \\
& = {\tikzfig{ZQ/q_spider_expand}} \lambda_{e^{i\alpha/2}}
\end{align}

\begin{align}
LHS & \by{\ref{propZQHH}} \left(\lambda_i \lambda_i \lambda_{-1}\right)^{\tensor n}  \left(\lambda_i \lambda_i \lambda_{-1}\right)^{\tensor m}
{\tikzfig{ZQ/q_spider_expand}} \lambda_{e^{i\alpha/2}}
\by{M} {\tikzfig{ZQ/q_spider_expand}} \lambda_{e^{i\alpha/2}}
\end{align}

Before proving the translation of the (EU') rule (Proposition <ref>) we introduce some helpful lemmas.
ZQ $\entails F_Q\left(EU'\right)$.

With the conditions of $ZX_{EU'}$

\begin{align}
\left(e^{i\left(\beta_1 + \beta_2 + \beta_3 + \gamma + 9\pi\right)/2}\right) \times
\left(\frac{i}{\sqrt{2}}\right) \times
\left(-\sqrt{2}\left(e^{i\gamma/2}\right)\right) = e^{i\left(\alpha_1 + \alpha_2 + \pi\right)/2}
\end{align}

\begin{align}
LHS = & \left(e^{i\left(\beta_1 + \beta_2 + \beta_3 + \gamma + 9\pi\right)/2}\right) \times
\left(\frac{i}{\sqrt{2}}\right) \times
\left(-\sqrt{2}\left(e^{i\gamma/2}\right)\right) \\
=     & \left(-i\right)\left(e^{i\left(\beta_1 + \beta_2 + \beta_3 + 2\gamma + \pi\right)/2}\right)                                           \\
=     & \left(-i\right)\left(e^{i\left(\arg z + \arg z' + \beta_2 + \arg z - \arg z' + 2x^+ - 2 \arg z + \pi - \beta_2 + \pi\right)/2}\right) \\
=     & \left(-i\right)\left(e^{i\left(2x^++2\pi\right)/2}\right)                                                                             \\
=     & e^{i\left(\alpha_1 + \alpha_2 + \pi\right)/2}
\end{align}

The quaternion $\left(\pi, \frac{x+z}{\sqrt{2}}\right)$ and its interactions with $\left(\alpha, z\right)$ and $\left(\alpha, x\right)$:

\begin{align}
\left(\pi, \frac{x+z}{\sqrt{2}}\right) \times \left(\alpha,z\right) = \left(\alpha, x\right) \times \left(\pi, \frac{x+z}{\sqrt{2}}\right) \\
\left(\alpha,z\right) \times \left(\pi, \frac{x+z}{\sqrt{2}}\right) = \left(\pi, \frac{x+z}{\sqrt{2}}\right) \times \left(\alpha,x\right)  \\
\left(\pi, \frac{x+z}{\sqrt{2}}\right) \times \left(\pi, \frac{x+z}{\sqrt{2}}\right) = -1
\end{align}

\begin{align}
(\pi, \frac{x+z}{\sqrt{2}}) \times (\alpha, z) =                 & \frac{1}{\sqrt{2}}(i+k)(\cos \frac{\alpha}{2} + k \sin \frac{\alpha}{2})                                              \\
=                                                                & \frac{1}{\sqrt{2}}(-\sin\frac{\alpha}{2} + i \cos \frac{\alpha}{2} - j \sin \frac{\alpha}{2} +k \cos \frac{\alpha}{2} \\
=                                                                & \frac{1}{\sqrt{2}}(\cos\frac{\alpha}{2}+i\sin\frac{\alpha}{2})(i+k)                                                   \\
=                                                                & (\alpha, x) \times (\pi, \frac{x+z}{\sqrt{2}})                                                                        \\
\nonumber \\
(\pi, \frac{x+z}{\sqrt{2}})\times(\alpha, x) =                   & \frac{1}{\sqrt{2}}(i+k)(\cos \frac{\alpha}{2} + i \sin \frac{\alpha}{2})                                              \\
=                                                                & \frac{1}{\sqrt{2}}(-\sin\frac{\alpha}{2} + i \cos \frac{\alpha}{2} + j \sin \frac{\alpha}{2} +k \cos \frac{\alpha}{2} \\
=                                                                & \frac{1}{\sqrt{2}}(\cos\frac{\alpha}{2}+k\sin\frac{\alpha}{2})(i+k)                                                   \\
=                                                                & (\alpha, z) \times (\pi, \frac{x+z}{\sqrt{2}})                                                                        \\
\nonumber \\
(\pi, \frac{x+z}{\sqrt{2}}) \times (\pi, \frac{x+z}{\sqrt{2}}) = & \frac{1}{\sqrt{2}}(i+k)\frac{1}{\sqrt{2}}(i+k)                                                                        \\
=                                                                & \frac{1}{2}(-1-j-1+j) = -1
\end{align}

We reproduce the side conditions for the rule $\ZX_{EU'}$ for reference here:

[Figure 2, A Near-Minimal Axiomatisation of ZX-Calculus
for Pure Qubit Quantum Mechanics [25]]
In rule (EU'), $\beta_1$, $\beta_2$, $\beta_3$ and $\gamma$
can be determined as follows: $x^+ := \frac{\alpha_1 + \alpha_2}{2}$,
$x^- := x^-\alpha_2$, $z := - \sin (x^+) + i \cos(x^-)$
and $z' := \cos(x^+) - i \sin (x^-)$,
then $\beta_1 = \arg z + \arg z'$, $\beta_2 = 2 \arg(i + \frac{\abs{z}}{\abs{z'}})$,
$\beta_3 = \arg z - \arg z'$, $\gamma = x^+ - \arg(z) + \frac{\pi - \beta_2}{2}$
where by convention $\arg(0) := 0$ and $z' = 0 \implies \beta_2 = 0$.

With the conditions of $ZX_{EU'}$:

\begin{align}
\left(\alpha_1, z\right) \times H \times \left(\alpha_2, z\right) = H \times \left(\beta_1, z\right) \times H  \times \left(\beta_2,z\right) \times H \times \left(\beta_3, z\right) \times H
\end{align}

In the hope of easing legibility we separate out the real, $i$, $j$, and $k$ components
of quaternions onto separate lines where suitable.

\begin{align}
RHS =& H \times (\beta_1, z) \times H  \times (\beta_2,z) \times H \times (\beta_3, z) \times H \\
= & H \times H \times H \times H \times (\beta_1, x) \times  (\beta_2,z) \times (\beta_3, x) & (\ref{lemZQHComm}) \\
= & (\beta_1, x) \times  (\beta_2,z) \times (\beta_3, x)                                     & (\ref{lemZQHComm}) \\
=& (\cos \beta_1 / 2 + i \sin \beta_1 / 2) \times  (\cos \beta_2 / 2 + k \sin \beta_2 / 2) \times  (\cos \beta_3 / 2 + i \sin \beta_3 / 2) \\
=& 1(\cos \beta_1 /2 \cos \beta_2/2 \cos \beta_3/2 - \sin \beta_1 / 2 \cos \beta_2 /2 \sin \beta_3 / 2) +\\
\nonumber & i (\cos \beta_1 /2 \cos \beta_2/2 \sin \beta_3/2 + \sin \beta_1 / 2 \cos \beta_2 /2 \cos \beta_3 / 2) + \\
\nonumber&j (\cos \beta_1 /2 \sin \beta_2/2 \sin \beta_3/2 - \sin \beta_1 / 2 \sin \beta_2 /2 \cos \beta_3 / 2) + \\
\nonumber&k (\cos \beta_1 /2 \sin \beta_2/2 \cos \beta_3/2 + \sin \beta_1 / 2 \sin \beta_2 /2 \sin \beta_3 / 2) \\
= & 1 (\cos \beta_2/2)(\cos \beta_1 /2 \cos \beta_3/2 - \sin \beta_1 / 2 \sin \beta_3 / 2) + \\
\nonumber & i (\cos \beta_2 /2)(\cos \beta_1 /2 \sin \beta_3/2 + \sin \beta_1 / 2  \cos \beta_3 / 2) + \\
\nonumber & j (\sin \beta_2/2)(\cos \beta_1 /2  \sin \beta_3/2 - \sin \beta_1 / 2  \cos \beta_3 / 2) + \\
\nonumber & k (\sin \beta_2/2)(\cos \beta_1 /2 \cos \beta_3/2 + \sin \beta_1 / 2\sin \beta_3 / 2) \\
= & 1 (\cos \beta_2/2)(\cos \frac{\beta_1 + \beta_3}{2}) + \\
\nonumber & i (\cos \beta_2 /2)(\sin \frac{\beta_1 + \beta_3}{2}) + \\
\nonumber & j (\sin \beta_2/2)(\sin \frac{\beta_3 - \beta_1}{2}) + \\
\nonumber & k (\sin \beta_2/2)(\cos \frac{\beta_1 - \beta_3}{2}) \\
= & 1 (\cos \beta_2/2)(\cos \arg z) + \\
\nonumber & i (\cos \beta_2 /2)(\sin \arg z) + \\
\nonumber & j (\sin \beta_2/2)(- \sin \arg z') + \\
\nonumber & k (\sin \beta_2/2)(\cos \arg z') \\
\end{align}

Using properties of arguments and moduli we then show the following:

\begin{align}
\cos \arg (a + ib) =     & a / \abs{a+ib}                                                                            \\
\sin \arg (a + ib) =     & b / \abs{a+ib}                                                                            \\
\abs{z}^2 =              & \sin(x^+)^2 + \cos(x^-)^2                                                                 \\
\abs{z'}^2 =             & \sin(x^-)^2 + \cos(x^+)^2                                                                 \\
\abs{z}^2 + \abs{z'}^2 = & \cos^2 x^+ + \sin^2 x^+ + \cos^2 x^- + \sin^2 x^- = 2                                     \\                                            \\
\cos \arg z =            & \Re(z) / \abs{z} =  \frac{-\sin(\alpha_1 + \alpha_2)/2}{\abs{z}}                          \\
\sin \arg z =            & \Im(z) / \abs{z} = \frac{\cos(\alpha_1 - \alpha_2)/2}{\abs{z}}                            \\
\cos \arg z' =           & \Re(z') / \abs{z'}  = \frac{\cos(\alpha_1 + \alpha_2)/2}{\abs{z'}}                        \\
\sin \arg z' =           & \Im(z') / \abs{z'} =\frac{-\sin(\alpha_1 - \alpha_2)/2}{\abs{z'}}                         \\
\nonumber \\
\cos(\beta_2 / 2) =      & \cos \arg (i + \abs{z}/\abs{z'})  = \cos \arg (\abs{z'}i + \abs{z})  = \abs{z} / \sqrt{2} \\
\sin(\beta_2 / 2) =      & \sin \arg (i + \abs{z}/\abs{z'}) = \sin \arg (\abs{z'}i + \abs{z}) =\abs{z'} / \sqrt{2}
\end{align}

And now substitute these values into our expression for the right hand side:

\begin{align}
RHS =     & 1 (\cos \beta_2/2)(\cos \arg z) +                                           \\
\nonumber & i (\cos \beta_2 /2)(\sin \arg z) +                                          \\
\nonumber & j (\sin \beta_2/2)(- \sin \arg z') +                                        \\
\nonumber & k (\sin \beta_2/2)(\cos \arg z')                                            \\
=         & 1 (\abs{z} / \sqrt{2})(\frac{-\sin(\alpha_1 + \alpha_2)/2}{\abs{z}}) +      \\
\nonumber & i (\abs{z} / \sqrt{2})(\frac{\cos(\alpha_1 - \alpha_2)/2}{\abs{z}}) +       \\
\nonumber & j (\abs{z'} / \sqrt{2} )(- \frac{-\sin(\alpha_1 - \alpha_2)/2}{\abs{z'}}) + \\
\nonumber & k (\abs{z'} / \sqrt{2} )(\frac{\cos(\alpha_1 + \alpha_2)/2}{\abs{z'}})      \\
=         & (\frac{1}{\sqrt{2}}) \times                                                 \\
\nonumber & (-1 (\sin(\alpha_1 + \alpha_2)/2) +                                         \\
\nonumber & i (\cos(\alpha_1 - \alpha_2)/2) +                                           \\
\nonumber & j (\sin(\alpha_1 - \alpha_2)/2) +                                           \\
\nonumber & k (\cos(\alpha_1 + \alpha_2)/2))                                            \\
\end{align}

And now for the left hand side:

\begin{align}
LHS =     & (\alpha_1, z) \times H \times (\alpha_2, z)                                                                                \\
=         & \frac{1}{\sqrt{2}} (\cos\alpha_1 + k\sin\alpha_1) (i+k) (\cos\alpha_2 + k\sin\alpha_2)                                                  \\
=         & \frac{1}{\sqrt{2}} (i \cos\alpha_1 \cos\alpha_2 - j \cos\alpha_1\sin\alpha_2 + k \cos\alpha_1 \cos\alpha_2 - \cos\alpha_1\sin\alpha_2 + \\
\nonumber & j \sin\alpha_1\cos\alpha_2 + i \sin\alpha_1\sin\alpha_2  - \sin\alpha_1\cos\alpha_2 - k \sin\alpha_1\sin\alpha_2)                       \\
=         & \frac{1}{\sqrt{2}} (-(\cos\alpha_1\sin\alpha_2 + \sin\alpha_1\cos\alpha_2)                                                              \\
\nonumber & i(\sin\alpha_1\sin\alpha_2 + \cos\alpha_1\alpha_2) +                                                                                \\
\nonumber & j(\sin\alpha_1\cos\alpha_2 - \cos\alpha_1\sin\alpha_2) +                                                                                \\
\nonumber & k(\cos\alpha_1\cos\alpha_2 - \sin\alpha_1\sin\alpha_2))                                                                                \\
=         & (\frac{1}{\sqrt{2}}) \times                                                                                \\
\nonumber & (-1 (\sin(\alpha_1 + \alpha_2)/2) +                                                                                \\
\nonumber & i (\cos(\alpha_1 - \alpha_2)/2) +                                                                                \\
\nonumber & j (\sin(\alpha_1 - \alpha_2)/2) +                                                                                \\
\nonumber & k (\cos(\alpha_1 + \alpha_2)/2))
\end{align}

\begin{align}
ZQ \entails {\tikzfig{ZQ/q_pigamma}} & = \lambda_{-\sqrt{2}\left(e^{i\gamma/2}\right)}
\end{align}

This is a special case of Lemma <ref>

\begin{align}
ZQ \entails     & F_Q\left(EU'\right)                                                                                \\
\ie ZQ \entails & \lambda_{e^{\frac{i}{2}\left(\alpha_1 + \alpha_2 + \pi\right)}} {\tikzfig{ZQ/q_EU1}} =\lambda_{e^{i(\beta_1 + \beta_2 + \beta_3 + \gamma + 9\pi)/2}} \ {\tikzfig{ZQ/q_eur}}
\end{align}

\begin{align}
LHS \by{I_q, Q}              & \node{qn}{\left(\alpha_1, z\right) \times H \times \left(\alpha_2, z\right)} \lambda_{e^{i\left(\alpha_1 + \alpha_2 + \pi\right)/2}} \\
RHS =                        &
\overset{\lambda_{e^{i\left(\beta_1 + \beta_2 + \beta_3 + \gamma + 9\pi\right)/2}}}{{\tikzfig{ZQ/q_HHH}}}
\node{qn}{H \times \left(\beta_1, z\right) \times H  \times \left(\beta_2,z\right) \times H \times \left(\beta_3, z\right) \times H} \\
\by{\ref{lemZQEUQuaternion}} &
\lambda_{e^{i\left(\beta_1 + \beta_2 + \beta_3 + \gamma + 9\pi\right)/2}}
\node{qn}{\left(\alpha_1, z\right) \times H \times \left(\alpha_2, z\right)}  \\
\by{\ref{lemZQGamma}}        &
\lambda_{e^{i\left(\beta_1 + \beta_2 + \beta_3 + \gamma + 9\pi\right)/2}}
\lambda_{-\sqrt{2}\left(e^{i\gamma/2}\right)}
\node{qn}{\left(\alpha_1, z\right) \times H \times \left(\alpha_2, z\right)} \\
\by{\ref{propZQHHH}}         &
\lambda_{e^{i\left(\beta_1 + \beta_2 + \beta_3 + \gamma + 9\pi\right)/2}}
\lambda_{\frac{i}{\sqrt{2}}}
\lambda_{-\sqrt{2}\left(e^{i\gamma/2}\right)}
\node{qn}{\left(\alpha_1, z\right) \times H \times \left(\alpha_2, z\right)} \\
\by{\ref{lemZQQLambdas}}     &
\lambda_{e^{i\left(\alpha_1 + \alpha_2 + \pi\right)/2}}
\node{qn}{\left(\alpha_1, z\right) \times H \times \left(\alpha_2, z\right)}
\end{align}

We have shown that for every rule $L=R$ in ZX, $ZQ \entails F_Q\left(L\right) = F_Q\left(R\right)$.
We have therefore shown that if $ZX \entails D_1 = D_2$ then $ZQ \entails F_Q\left(D_1\right) = F_Q\left(D_2\right)$.

§.§ From ZQ to ZX and back again

It remains to be shown that $ZQ \entails F_Q\left(F_X\left(D\right)\right) = D$

Re-translating the Z spider

\begin{align}
ZQ \entails F_Q\left(F_X\left(\spider{smallZ}{}\right)\right) = \spider{smallZ}{}
\end{align}

\begin{align}
LHS = F_Q\left(\spider{gn}{}\right) \by{\ref{lemZQTranslationZ}} \spider{smallZ}{}
\end{align}

The following lemmas are necessary for the re-translation of the $Q$ node in Proposition <ref>.

\begin{align}
ZQ \entails F_Q\left(\tripleblobs\right) = \lambda_{1 / \sqrt{2}}
\end{align}

\begin{align}
F_Q\left(\tripleblobs\right) \by{M} \lambda_{-i} \tikzfig{ZQ/q_HHH} \by{M, \ref{propZQHHH}} \lambda_{1 / \sqrt{2}}
\end{align}

\begin{align}
ZQ \entails F_Q\left(\galpharpi{\gamma}\right) = \lambda_{-\sqrt{2}e^{i\gamma/2}}
\end{align}

\begin{align}
F_Q\left(\galpharpi{\gamma}\right) \by{Y} \tikzfig{ZQ/q_pigamma} \lambda_{e^{i\gamma/2}} \lambda_{i} \lambda_{i} \by{\ref{lemZQGamma}, M} \lambda_{\sqrt{2}e^{i\gamma}}
\end{align}

\begin{align}
ZQ \entails F_Q\left(\node{gn}{\alpha}\right) = \node{qn}{\alpha,z} \lambda_{e^{i\frac{\alpha}{2}}}
\end{align}

\begin{align}
LHS = & \node{smallZ}{} \comp \node{qn}{\alpha,z} \comp \node{smallZ}{} \lambda_{e^{i\frac{\alpha}{2}}} =\node{qn}{\alpha,z}  \lambda_{e^{i\frac{\alpha}{2}}}
\end{align}

\begin{align}
ZQ \entails F_Q\left(\node{rn}{\alpha}\right) = \node{qn}{\alpha,x} \lambda_{e^{i\frac{\alpha}{2}}}
\end{align}

\begin{align}
LHS \by{M} & \node{qn}{\text{H}} \comp\node{smallZ}{} \comp  \node{qn}{\alpha,z} \comp\node{smallZ}{} \comp  \node{qn}{\text{H}} \lambda_{-e^{i\frac{\alpha}{2}}} \\
\by{Q}     & \node{qn}{H \times \left(\alpha,z\right) \times H}  \lambda_{-e^{i\frac{\alpha}{2}}}
\by{\ref{lemZQHComm}}
\node{qn}{H \times H \times \left(\alpha,x\right)}  \lambda_{-e^{i\frac{\alpha}{2}}} \\
& \by{\ref{propZQHH}, N} \node{qn}{\alpha,x}  \lambda_{e^{i\frac{\alpha}{2}}}
\end{align}

\begin{align}
ZQ \entails F_Q\left(F_X\left(\node{qn}{q}\right)\right) = \node{qn}{q}
\end{align}

Where $q = \left(\alpha_1, z\right) \times \left(\alpha_2, x\right) \times \left(\alpha_3 , z\right)$, as in Proposition <ref>

\begin{align}
LHS =                                                                       & F_Q\left(
\node{gn}{\alpha_1} \comp  \node{rn}{\alpha_2} \comp  \node{gn}{\alpha_3} \right) \tensor
\galpharpi{-\alpha_1/2}
\galpharpi{-\alpha_2/2}
\galpharpi{-\alpha_3/2}
\tripleblobs \tripleblobs \tripleblobs \\
\by{\ref{propZQRetranslateGammaAlphaPi}, \ref{lemZQRetranslateTripleBlobs}} &
\node{gn}{\alpha_1} \comp  \node{rn}{\alpha_2} \comp  \node{gn}{\alpha_3}\right) \tensor
\lambda_{\sqrt{2}e^{-i\alpha_1/2}}
\lambda_{\sqrt{2}e^{-i\alpha_2/2}}
\lambda_{\sqrt{2}e^{-i\alpha_3/2}}
\lambda_{\frac{1}{\sqrt{2}}} \lambda_{\frac{1}{\sqrt{2}}} \lambda_{\frac{1}{\sqrt{2}}} \\
\by{M}                                                                      & F_Q\left(
\node{gn}{\alpha_1} \comp  \node{rn}{\alpha_2} \comp  \node{gn}{\alpha_3}\right) \tensor
\lambda_{e^{-\frac{i}{2}\left(\alpha_1 + \alpha_2 + \alpha_3\right)}} \\
\by{\ref{lemZQRetranslateXNode}, \ref{lemZQRetranslateZNode}}               &
\left(\node{qn}{\alpha_1,z} \comp  \node{qn}{\alpha_2,x} \comp  \node{qn}{\alpha_3,z}\right) \tensor
\lambda_{e^{-\frac{i}{2}\left(\alpha_1 + \alpha_2 + \alpha_3\right)}} \lambda_{e^{i\alpha_1/2}} \lambda_{e^{i\alpha_2/2}} \lambda_{e^{i\alpha_3/2}} \\
\by{M}                                                                      & \node{qn}{\alpha_1,z} \comp  \node{qn}{\alpha_2,x} \comp  \node{qn}{\alpha_3,z}                      \\
\by{Q}                                                                      & \node{qn}{\left(\alpha_1, z\right) \times \left(\alpha_2, x\right) \times \left(\alpha_3 , z\right)}
\end{align}

Finally we need the following lemma for Proposition <ref>.

\begin{align}
ZQ \entails F_Q\left(\rg{\beta}{-\beta}\right) = \lambda_{\sqrt{2}\cos \beta}
\end{align}

\begin{align}
LHS =  & {\tikzfig{ZQ/q_rgbb}} \lambda_{e^{i\beta_2}} \lambda_{e^{-i\beta_2}} \lambda_i
\by{M} {\tikzfig{ZQ/q_rgbb}} \lambda_i
\by{Q} {\tikzfig{ZQ/q_rgbb2}} \lambda_i \\
\by{A} & \lambda_{\sqrt{2}\cos \beta}
\end{align}

\begin{align}
ZQ \entails F_Q\left(F_X\left(\lambda_{c}\right)\right) = \lambda_{c}
\end{align}

\begin{align}
c =                            & \left(\sqrt{2}\right)^n e^{i\alpha} \cos \beta \quad \text{ for some } \alpha,\,\beta                \\
LHS =                          & F_Q\left(\galpharpi{\alpha} \halfblobs \left(\rg{}{\pi}\right)^{\tensor n} \rg{\beta}{-\beta}\right)
\by{\ref{propZQRetranslateGammaAlphaPi}, \ref{propZQHHH}} \lambda_{\sqrt{2}e^{i\alpha}} \lambda_{\frac{1}{\sqrt{2}}} \lambda_{\frac{1}{\sqrt{2}}} \left(\lambda_{\sqrt{2}}\right)^{\tensor n} F_Q\left(\rg{\beta}{-\beta}\right) \\
\by{\ref{propZQRetranslateRG}} &
\lambda_{\sqrt{2}e^{i\alpha/2}}
\lambda_{\frac{1}{\sqrt{2}}}
\lambda_{\frac{1}{\sqrt{2}}}
\left(\lambda_{\sqrt{2}}\right)^{\tensor n}
\lambda_{\sqrt{2}\cos\beta}
\by{M}  \lambda_{\left(\sqrt{2}\right)^n e^{i\alpha} \cos \beta} = \lambda_c
\end{align}

We have shown that for each of the generators of ZQ, $ZQ \entails F_Q\left(F_X\left(G\right)\right) = G$,
and since $F_Q$ and $F_X$ are monoidal functors we know that $ZQ \entails F_Q\left(F_X\left(D\right)\right) = D$ for any diagram $D$.
This concludes our proof of completeness for the rules of ZQ.