We introduce a family of ZX-calculi which axiomatise the stabiliser fragment of
quantum theory in odd prime dimensions. These calculi recover many of the nice
features of the qubit ZX-calculus which were lost in previous proposals for
higher-dimensional systems. We then prove that these calculi are complete, i.e.
provide a set of rewrite rules which can be used to prove any equality of
stabiliser quantum operations. Adding a discard construction, we obtain a
calculus complete for mixed state stabiliser quantum mechanics in odd prime
dimensions, and this furthermore gives a complete axiomatisation for the
related diagrammatic language for affine co-isotropic relations.

The ZX-calculus is a powerful yet intuitive graphical language for reasoning
about quantum computing, or, more generally, about operations on quantum
systems <cit.>. It
allows one to represent such quantum operations pictorially, and comes equipped
with a set of rules which, in principle, make it possible to derive any equality
between those pictures <cit.>. It has now had several applications in quantum information
processing, from MBQC <cit.>,
through quantum error correction codes <cit.>. More
recently, it has been used to obtain state-of-the-art optimisation techniques
for quantum circuits <cit.> and faster classical simulation algorithms for
general quantum computations <cit.>.

Despite its origins in categorical quantum mechanics and the diagrammatic
language for finite-dimensional linear spaces <cit.> the literature on the
ZX-calculus has been concerned almost exclusively with small-dimensional quantum
systems, and even then mostly with the case of two-dimensional quantum systems,
or qubits. The qubit ZX-calculus is remarkable in its simple treatment of
stabiliser quantum mechanics, along with the fact that any diagram can be
treated purely graph-theoretically, without concern to its overall layout, and
without losing its quantum-mechanical interpretation. Those proposals that go
beyond qubits lose many of these nice features, and are significantly more
complicated than the qubit case <cit.>. In
particular, they eschew the prised “Only Connectivity Matters” (OCM)
meta-rule, often cited as one of the key features in the qubit case. In these
calculi, which can represent any linear map between the corresponding Hilbert
spaces, it is also not necessarily obvious (at least, to us) how to pick out and
work with the stabiliser fragment.

Stabiliser quantum mechanics is a simple yet particularly important fragment of
quantum theory. While much less powerful than the full fragment—it can be
efficiently classically simulated, even in odd prime dimensions
<cit.>—it has seen significant study
<cit.> and forms the basis
for a number of key methods in quantum information theory
<cit.>. Operationally, it can be described as the
fragment of quantum mechanics which is obtained if one allows only state
preparation in the computational basis, and unitary operations from the
Clifford groups <cit.>. In the qubit case,
the stabiliser fragment of the ZX-calculus was proved complete in
<cit.> while ignoring global scalars, and extended to
include scalars in <cit.>. A simplified calculus based on
these results but further reducing the set of axioms of the calculus was
presented in <cit.>.

In this article, we present a simple ZX-calculus for stabiliser quantum
mechanics in odd prime dimensions, and which recovers as many of the nice
features of the qubit calculus as possible. In odd prime dimensions, stabiliser
quantum mechanics can be given a particularly nice graphical presentation, owing
to the group-theory underlying the corresponding Clifford groups
<cit.>. We then give this calculus a set of rewrite
rules that is complete, i.e. rich enough to derive any equality of stabiliser
quantum operations. In particular, it is a design priority to recover OCM, and
to make explicit the stabiliser fragment and its group-theoretical
underpinnings. Adding a discard construction
<cit.>, we obtain a universal and complete calculus
for mixed state stabiliser quantum mechanics in odd prime dimensions. By
previous work <cit.>, this gives a complete
axiomatisation for the related diagrammatic language for affine co-isotropic
relations, while still maintaining OCM.

Although we do not do so here, these calculi can naturally be extended to
represent much larger fragments of quantum theory, up to the entire theory in
odd prime dimensions <cit.>. However, finding a complete
axiomatisation for such calculi will presumably be a much more complicated task,
and we leave this for future work.

We would like to thank Cole Comfort and Simon Perdrix for enlightening
discussions. We also thank John van de Wetering, Boldizsar Poor, and Lia Yeh as
well as our reviewers for their numerous suggestions for improvement. RIB was
funded by the ANR VanQuTe project (ANR-17-CE24-0035), as well as the Cisco
University Research Program Fund.

§ STABILISER QUANTUM MECHANICS IN ODD PRIME DIMENSIONS

Throughout this paper, \(p\) denotes an arbitrary odd prime, and \(\Z_p =
\Z/p\Z\) the ring of integers with arithmetic modulo \(p\). We also put \(\omega
\coloneqq e^{i\frac{2\pi}{p}}\), and let \(\Z_p^*\) be the group of units of
\(\Z_p\). Since \(p\) is prime, \(\Z_p\) is a field and \(\Z_p^* = \Z_p
\setminus \{0\}\) as a set. We also have need of the following definition:

\begin{equation}
\label{eq:legendre_characteristic}
\chi_p(x) =
\begin{cases}
1 \qif \text{there is no } y \in \Z_p \text{ s.t. } x = y^2; \\
0 \quad \text{otherwise};
\end{cases}
\end{equation}

which is just the characteristic function of the complement of the set of
squares in \(\Z_p\).

The Hilbert space of a qupit <cit.> is \(\mathcal{H} = \operatorname{span}\{\ket{m} \mid m \in
\Z_p\} \cong \C^p\), and we write \(U(\mathcal{H})\) the group of unitary
operators acting on \(\mathcal{H}\). We have the following standard operators on
\(\mathcal{H}\), also known as the clock and shift operators:

\begin{equation}
Z \ket{m} \coloneqq \omega^{m} \ket{m} \qand
X \ket{m} \coloneqq \ket{m+1}
\qq{for any} m \in \Z_p.
\label{eq:pauli}
\end{equation}

In particular, note that \(ZX = \omega XZ\).
We call any operator of the form \(\omega^k X^a Z^b\) for \(k,a,b \in \Z_p\) a
Pauli operator. We say a Pauli operator is trivial if it is
proportional to the identity. The collection of all Pauli operators is denoted
\(\mathscr{P}_1\) and called the Pauli group. For \(n \in \N^*\), the
generalised Pauli group is \(\mathscr{P}_n \coloneqq \bigotimes_{k=1}^n
\mathscr{P}_1\).

Of particular importance to us are the (generalised) Clifford groups.
These are defined, for each \(n \in \N^*\), as the normaliser of
\(\mathscr{P}_n\) in \(U(\mathcal{H}^{\otimes n})\): \(C\) is a Clifford
operator if for any \(P \in P_n\), \(CPC^\dagger \in \mathscr{P}_n\). It is clear that
that every Pauli operator is Clifford, but there are non-Pauli Clifford operators.
Some important examples are the Hadamard gate:

\begin{equation}
H\ket{m} = \frac{1}{\sqrt{d}} \sum_{n \in \Z_p} \omega^{mn} \ket{n}
\qq{s.t.} HXH^\dagger = Z \qand HZH^\dagger = X^{-1},
\label{eq:hadamard}
\end{equation}

and the phase gate:

\begin{equation}
S\ket{m} = \omega^{2^{-1}m(m+1)} \ket{m}
\qq{s.t.} SXS^\dagger = \omega XZ \qand SZS^\dagger = Z.
\label{eq:phase}
\end{equation}

Yet another important example is the controlled-phase gate, which acts on
\(\mathcal{H} \otimes \mathcal{H}\),

\begin{equation}
E \ket{m} \ket{n} \coloneqq \omega^{mn} \ket{m}\ket{n}.
\end{equation}

It is important to emphasise a key difference between the qupit and the qubit
case: when \(p \neq 2\), none of these operators are self-inverse.
In fact, if \(Q\) is a Pauli and \(I\) the identity operator on \(\mathcal{H}\),
we have:

\begin{equation}
Q^p = I, \quad E^p = I \otimes I \qand H^4 = I.
\end{equation}

As a side note, equations (<ref>), (<ref>) and
(<ref>) imply that both \(X\) and \(Z\), and in fact every Pauli, have
spectrum \(\{\omega^k \mid k \in \Z_p\}\). As a result, we denote \(\ket{k :
Q}\) the eigenvector of a given Pauli \(Q\) associated with eigenvalue
\(\omega^k\), and furthermore use the notation

\begin{equation}
\ket{\underbrace{k,\dots, k}_{n\text{ times}} : Q } = \bigotimes_{k=1}^n \ket{k:Q}.
\end{equation}

It follows from equation (<ref>) that we can identify \(\ket{k:Z} =
\ket{k}\).

Now, for any \(\alpha \in [0,2\pi)\), the operator \(e^{i\alpha} I\) is Clifford.
However, we want to construct calculi with a finite axiomatisation. As a result,
the diagrams in the calculus are countable and this makes it impossible for us
to represent all such phases \(e^{i\alpha}\). Unfortunately, finding a group of
phases that behaves well diagrammatically is somewhat inconvenient, and involves
some elementary number theory. For an odd prime \(p\), we consider the group of
phases given by:

* if \(p \equiv 1 \mod 4\),

\begin{equation}
\label{eq:Pp_1}
\mathbb{P}_p \coloneqq \left\{ (-1)^s \omega^t \mid s,t \in \Z \right\};
\end{equation}

* if \(p \equiv 3 \mod 4\),

\begin{equation}
\label{eq:Pp_3}
\mathbb{P}_p \coloneqq \left\{ i^s \omega^t \mid s,t \in \Z \right\}.
\end{equation}

This of course covers all cases since \(p\) is odd. Then, we restrict our
attention to the reduced Clifford group,

\begin{equation}
\mathscr{C}_n = \left\{ \lambda U \mid \lambda \in \mathbb{P}_p, U \text{ is Clifford and special unitary} \right\}.
\end{equation}

We call \(\mathscr{C}_1^{\otimes n}\) the local Clifford group on \(n\)
qupits. It is clear from these examples that \(\mathscr{C}_n\) is strictly
larger than \(\mathscr{C}_1^{\otimes n}\), but it turns out to not be that much

The reduced Clifford group \(\mathscr{C}_n\) is generated by the gate-set
\(\{H_j, S_j, E_{j,k} \mid j,k = 1, \dots, n\}\).

Stabiliser quantum mechanics can be operationally described as the
fragment of quantum mechanics in which the only operations allowed are
initialisations and measurements in the eigenbases of Pauli operators, and
unitary operations from the generalised Clifford groups. As before, we restrict
our attention to the fragment of stabiliser quantum mechanics where only unitary
operations from the reduced Clifford groups are allowed. Scalars are then taken
from the monoid \(\mathbb{G}_p \coloneqq \left\{0, \sqrt{p^r} \lambda \mid r \in
\Z, \lambda \in \mathbb{P}_p \right\}\). Little is lost for the description of
quantum algorithms, since we can always simplify by a global phase to make the
Clifford generators special unitary. Thus, we can embed any stabiliser circuit
into the calculus, and then calculate the relative phases of different branches
of a computation without restriction.

The symmetric monoidal category \(\mathsf{Stab}_p\) has as objects \(\C^{pn}\)
for each \(n \in \N\), and morphisms generated by:

* \(\C \to \C^p : \lambda \mapsto \lambda\ket{0}\);

* \(\C^{pn} \to \C^{pn} : \ket{\psi} \mapsto U\ket{\psi}\) for any \(U \in
\mathscr{C}_n\);

* \(\C^p \to \C : \ket{\psi} \mapsto \ip{0}{\psi}\).

The monoidal product is given by the usual tensor product of linear spaces.

It is clear that \(\mathsf{Stab}_p\) is a subcategory of the category
\(\mathsf{FLin}\) of finite dimensional \(\C\)-linear spaces; it is also a PROP.

§ A ZX-CALCULUS FOR ODD PRIME DIMENSIONS

In this section, we present our family of ZX-calculi, with one for each odd
prime. Relying on some of the group theoretical properties of the qupit Clifford
groups, we can give a relatively simple presentation of the calculi, which
avoids the need to explicitly consider rotations in \(p\)-dimensional space,
significantly simplifing the presentation compared to previous work
<cit.>. These calculi are also constructed in order to
satisfy the property of flexsymmetry, proposed in
<cit.>, and which allows one to recover
the OCM meta-rule. OCM is an intuitively desirable feature for the design of a
graphical language; anecdotally, it greatly simplifies the human manipulation of
diagrams, including in the proofs of this paper. More formally, it means that
the equational theory can be formalised in terms of double pushout rewriting
over graphs rather than over hypergraphs as is necessary in the more general
theory <cit.>.

Another key concern is the issue of completeness, which we begin to address in
this article. Outside of qubits <cit.>, there has so far been a complete axiomatisation
only for the stabiliser fragment in dimension \(p=3\) <cit.>.
We present an axiomatisation which is complete for the stabiliser fragment for
any odd prime \(p\), and leave the general case for future work.

§.§ Generators

For any odd prime \(p\), consider the symmetric monoidal category \(\ZXp\) with
objects \(\N\) and morphisms (or, diagrams) generated by:

\begin{align*}
\tikzfig{figures/generators/id} &: 1 \to 1 & \quad\quad\quad
\tikzfig{figures/generators/g-id} &: 1 \to 1 & \quad\quad\quad
\tikzfig{figures/generators/r-inv} &: 1 \to 1 & \\
\tikzfig{figures/generators/hadamard} &: 1 \to 1 & \quad
\tikzfig{figures/generators/g-unit} &: 0 \to 1 & \quad
\tikzfig{figures/generators/r-unit} &: 0 \to 1 & \\
\tikzfig{figures/generators/cup} &: 0 \to 2 & \quad
\tikzfig{figures/generators/g-counit} &: 1 \to 0 & \quad
\tikzfig{figures/generators/r-counit} &: 1 \to 0 & \\
\tikzfig{figures/generators/cap} &: 2 \to 0 & \quad
\tikzfig{figures/generators/g-mult} &: 2 \to 1 & \quad
\tikzfig{figures/generators/r-mult} &: 2 \to 1 & \\
\tikzfig{figures/generators/braid} &: 2 \to 2 & \quad
\tikzfig{figures/generators/g-comult} &: 1 \to 2 & \quad
\tikzfig{figures/generators/r-comult} &: 1 \to 2 &
\end{align*}

where \(x,y \in \Z_p\). We also introduce a generator \(\star : 0 \to 0\) to
simplify the calculus; it will correspond to a scalar whose representation in
terms of the other generators depends non-trivially on the dimension \(p\).
Finally, the empty diagram \(\tikzfig{figures/generators/empty_small} : 0 \to
0\) is also a morphism in the language. Morphisms are composed by connecting
output wires to input wires, and the monoidal product is given on objects by \(n
\otimes m = n+m\) and on morphisms by vertical juxtaposition of diagrams.

We extend this elementary notation with a first piece of syntactic sugar, which
is standard for the ZX-calculus family: green spiders are defined
inductively, for any \(m,n \in \N\), by

\begin{equation}
\tikzfig{figures/generators/g-spider-def}
\end{equation}

It is clear that these diagrams have types \(m+1 \to 1\), \(1 \to n+1\) and \(m
\to n\) respectively. This construction can be justified by remarking that, under
the equational theory to be presented in section <ref>, the
unlabelled green fragment of the language forms a special commutative Frobenius
algebra, which therefore admits a canonical form in terms of such “spiders”

Red spiders are defined analogously, with a small twist:

\begin{equation}
\tikzfig{figures/generators/r-spider-def}
\end{equation}

The addition of these \(1 \to 1\) red vertices (called antipodes) when
compared to green spiders mimicks a construction of the ZH-calculus
<cit.>, where they are sometimes
dubbed “harvestmen”. They are crucial in order for the red spiders to be
flexsymmetric in our equational theory and thus to recover the OCM meta-rule
mentioned above.

We can then define labelled spiders by passing the label of a \(0 \to 1\)
diagram along an input wire:

\begin{equation}
\tikzfig{figures/generators/spiders_labelled}
\end{equation}

In order to avoid clutter, we also use the following shorthand:

\begin{equation}
\tikzfig{figures/equations/hadamard_inverse}
\end{equation}

which we shall see represents the compositional inverse of
\(\tikzfig{figures/generators/hadamard}\).

§.§ Standard interpretation and universality

The standard interpretation of a \(\ZXp\)-diagram is a symmetric
monoidal functor \(\interp{-} : \ZXp \to \mathsf{FLin}\) (the category
of finite-dimensional \(\C\)-linear spaces). It is defined on objects as
\(\interp{m} \coloneqq \C^{p \times m}\), and on the generators
of the morphisms as:

\begin{align*}
\interp{\tikzfig{figures/generators/g-unit}} & = \sum_{k\in\Z_p} \omega^{2^{-1} (xk + yk^2)} \ket{k:Z} & \quad
\interp{\tikzfig{figures/generators/g-counit}} & = \sum_{k\in\Z_p} \omega^{2^{-1} (xk + yk^2)} \bra{k:Z}  \\
\interp{\tikzfig{figures/generators/g-comult}} & = \sum_{k\in\Z_p} \dyad{k:Z}{k,k:Z}&
\interp{\tikzfig{figures/generators/g-mult}} &= \sum_{k\in\Z_p} \dyad{k,k:Z}{k:Z} & \\
\interp{\tikzfig{figures/generators/g-id}} &= \sum_{k\in\Z_p} \dyad{k:Z}{k:Z} & \quad
\interp{\tikzfig{figures/generators/r-inv}} &= \sum_{k\in\Z_p} \dyad{-k:X}{k:X} & \quad \\
\interp{\tikzfig{figures/generators/r-unit}} &= \sum_{k\in\Z_p} \omega^{2^{-1} (xk + yk^2)} \ket{-k:X} & \quad
\interp{\tikzfig{figures/generators/r-counit}} &= \sum_{k\in\Z_p} \omega^{2^{-1} (xk + yk^2)}\bra{k:X} & \\
\interp{\tikzfig{figures/generators/r-comult}} &= \sum_{k\in\Z_p} \dyad{-k,-k:X}{k:X} &
\interp{\tikzfig{figures/generators/r-mult}} &= \sum_{k\in\Z_p} \dyad{-k:X}{k,k:X} & \\
\interp{\tikzfig{figures/generators/id}} &= \sum_{k\in\Z_p} \dyad{k:Z}{k:Z} & \quad
\interp{\tikzfig{figures/generators/hadamard}} &= \sum_{k\in\Z_p} \dyad{k:X}{k:Z} & \\
\interp{\tikzfig{figures/generators/cup}} &= \sum_{k\in\Z_p} \ket{kk:Z} & \quad
\interp{\tikzfig{figures/generators/cap}} &= \sum_{k\in\Z_p} \bra{kk:Z} & \\
\interp{\tikzfig{figures/generators/braid}} &= \sum_{k,\ell\in\Z_p} \dyad{k,\ell:Z}{\ell,k:Z} & \quad
\interp{\scalebox{1.4}{$\star$}} &= -1 &
\end{align*}

By the functoriality of the standard interpretation, we then deduce that

\begin{equation}
\interp{\tikzfig{figures/generators/g-spider}} = \sum_{k\in\Z_p} \omega^{2^{-1} (xk + yk^2)} \ket{k:Z}^{\otimes n} \bra{k:Z}^{\otimes m},
\end{equation}

\begin{equation}
\interp{\tikzfig{figures/generators/r-spider}} = \sum_{k\in\Z_p} \omega^{2^{-1} (xk + yk^2)} \ket{-k:X}^{\otimes n} \bra{k:X}^{\otimes m}.
\end{equation}

There are a couple of peculiarities in this standard interpretation that must be
remarked upon. Firstly, note that the red \(1 \to 1\) spider is not the
identity, but rather maps the label of any input \(X\)-eigenstate to its
additive inverse. This feature is repeated on every red spider, and is another
of the side-effects of imposing that the OCM rule must be sound for this

Secondly, and much more subtly, we have made an unconventional choice for the
interpretation of the label of spiders as a phase: there is an additional factor
\(2^{-1}\) which one might not expect. This might seem like an inconsequential
choice which ought to be removed, but it has an important consequence for the
equational theory. There is a specific rule in the axiomatisation,
(Gauss), which is sound for this choice of phases but not for the
simpler one which omits the factor \(2^{-1}\).

The standard interpretation \(\interp{-}\) is universal for the qupit
stabiliser fragment, i.e. for any stabiliser operation \(C :
\C^{p m} \to \C^{p n}\) there is a diagram \(D \in \ZXp\) such that
\(\interp{D} = C\). Put formally, the co-restriction of \(\interp{-}\) to
\(\mathsf{Stab}_p\) is full.

§.§ Axiomatisation

A presentation of the equational theory \(\ZXeq\), which is
sound and complete for the stabiliser fragment. The equations hold for any
\(a,b,c,d \in \Z_p\) and \(z \in \Z_p^*\). \(\chi_p\) is the characteristic
function of the complement of the set of squares in \(\Z_p\), defined in
equation (<ref>)

We now begin to introduce rewrite rules with which to perform purely
diagrammatic reasoning. By doing so we are in fact describing a PROP by
generators and relations <cit.>, thus the swap is required to
satisfy the following properties:

\begin{equation}
\tikzfig{figures/universality/swaprules}
\end{equation}

Note that the last equation is required to hold for any diagram $D:n\to m$. This
property states that our diagrams form a symmetric monoidal category.
Furthermore, we want this category to be self-dual compact-closed, hence the cup
and cap must satisfy:

\begin{equation}
\tikzfig{figures/universality/cupcaprule}
\end{equation}

Furthermore, as long as the connectivity of the diagram remains the same, vertices can be
freely moved around without changing the standard interpretation of the diagram.
This is a consequence of the fact that we require our generators to be
flexsymmetric, as shown in <cit.>. This amounts to imposing that all generators except
the swap satisfy:

\begin{equation}
\tikzfig{figures/universality/flexsymmetry}
\end{equation}

where $\sigma:n+m\to n+m$ stands for any permutation of the wires involving swap
maps. We will consider all the previous rules as being purely structural and
will not explicitly state their use. Using these rules, we can in fact deduce
that both the green and red spiders (and their labelled varieties) are
themselves flexsymmetric. This means that the language follows the OCM
meta-rule, and we can formally treat any \(\ZXp\)-diagram as a
graph[Note that the graphs in question must be allowed to have loops
and parallel edges, so are perhaps better called pseudographs or
multigraphs.] whose vertices are the spiders, and whose edges are
labelled by the \(1 \to 1\) generators of the language.[There is a
small ambiguity: \(1 \to 1\) spiders can be treated as either edges or
vertices. When considering diagrams, it matters little which, since any given
graph is always to be understood as one of the many equivalent
\(\ZXp\)-diagrams constructed formally out of the generators.
Any computer implementation of the calculus will have to carefully resolve
this ambiguity in its internal representation.]

Figure <ref> presents the remainder of the equational theory
\(\ZXeq\), which as we shall see axiomatises the stabiliser fragment of quantum
mechanics in the qupit ZX-calculus. Firstly though, we must be sure that all of
these rules are sound for the standard interpretation, i.e. it should not be
possible to derive an equality of diagrams whose quantum mechanical
interpretations are different.

The equational theory \(\ZXeq\) is sound for \(\interp{-}\), i.e., for any
\(A,B \in \ZXp\), \(\ZXeq \vdash A = B\) implies \(\interp{A} = \interp{B}\).
Put formally, \(\interp{-}\) factors through the projection \(\ZXp \to \ZXp /
\ZXeq\).

This set of rewriting rule also turns out to be also complete:

The equational theory \(\ZXeq\) is complete for \(\interp{-}\), i.e., for any
\(A,B \in \ZXp\), \(\interp{A} = \interp{B}\) implies \(\ZXeq \vdash A = B\).

The proof of Theorem <ref> will be the object of the following

§ SOME USEFUL STRUCTURES IN \(\ZXP\)

The set of axioms in figure <ref> is somewhat minimalistic. In this section we present how it will be manipulated in practice.

§.§ Elementary derivations

While we will see that the equations in figure <ref> are enough to
derive any equality of quantum operation in the stabiliser fragment, we describe
here some rules which are derivable in \(\ZXeq\) and particularly useful. We start by the interaction between some $1\to 1$ maps:

\begin{equation}
\tikzfig{hadanteul}
\end{equation}

The following rules, very similar to the one of <cit.>, will be central:

\begin{equation}
\tikzfig{glaeq}
\end{equation}

Here we see that the $1\to 1 $ red spider play the role of the antipode of Hopf algebra, we will then refer to it as the antipode. Finally, the pauli phases can easily move around diagrams:

\begin{equation}
\tikzfig{paulimove}
\end{equation}

§.§ Meta-rules

From the equational theory follows more general patterns that we will often use as meta-rules.

Changing colours The qubit ZX-calculus admits a particularly elegant
meta-rule: take any valid equation, and swap the colour of every spider while
keeping everything else identical. Then the resulting equation is also derivable
in the calculus. In fact this color swap transformation is equivalent to the functor mapping a diagram $D$ to $H^{\otimes m} D \circ H^{\otimes n}$. One might hope that such a rule would hold also in \(\ZXeq\).
Unfortunately, the picture is a little more intricate and less pretty since now the analog of the Hadamard gate is not an involution. Using
(Colour), one can see what happen while Hadamrd gates are going through a diagram:

\begin{equation}
\tikzfig{figures/equations/colour_commutation}
\end{equation}

This allows to formulate a variation of the color swap rules that holds for qudits as well:

If \(A \in \ZXp[n,m]\) is a diagram, we can consider any spider which is not the antipode as vertices linked by the following four kind of edges:

let \(S(A)\) be the \(\ZXp\)-diagram obtained from \(A\) by :

* swapping the colour of every vertex;

* applying the following transformation on the edges:

* adding a minus to the Pauli part of every green spider.

Then $\ZXeq \vdash S(A) = (\tikzfig{figures/generators/hadamard})^{\otimes m}
\circ A \circ (\tikzfig{figures/generators/hadamard})^{\otimes n}$.

Application of this rule will simply be referred to as (Colour), since
the colour change rule presented in figure <ref> is a subcase. Note
that, although \(S\) is not functorial, it can be easily made into a functor,
simply by post-composing with antipodes.

Note that the original colour change rule cannot hold for \(\ZXp\), since it
does if and only if the antipode is trivial. To show this, it suffices to colour
change the (G-Elim) rule.

Spider wars Just like in the qubit case, there are rules for fusing
spiders of the same colour, and splitting spiders of opposite colours. The
fusion rules are pretty much the same, up to the use of antipodes for red

\begin{equation}
\tikzfig{figures/equations/spider_fusion}
\end{equation}

They are a straightforward consequence of (Fusion) and
lemma <ref> which eliminates self-loops. The splitting rules are more
complicated, since unlike the qubit case, we now have two elementary rules for
splitting: the Hopf identity (lemma <ref>) and (Char). Using a
sequential application of these rules, it is straightforward to see that, for
any \(x,y \in \N\) such that \(x \geqslant y\), we must have:

\begin{equation}
\label{eq:spider_wars}
\tikzfig{figures/equations/spider_wars_1}
\quad\quad\quad
\tikzfig{figures/equations/spider_wars_2}
\end{equation}

We dub this collection of meta-rules (Spider), along with deformations
resulting from flexsymmetry.

§.§ Syntactic sugar for multi-edges

Before we move into the proof of completeness, we introduce some syntactic sugar
to the language. Given equation (<ref>), in \(\ZXp\), unlike the
qubit case, spiders of opposite colours can be connected by more that one edge,
and these multi-edges cannot be simplified. We therefore add some syntactic
sugar to represent such multi-edges. These constructions add no expressiveness
to the language, and are simply used to reduce the size of some recurring
diagrams. They are shamelessly stolen from previous work
<cit.>, and we use them to obtain a
particularly nice representation of qupit graph states <cit.>.
Graph states play a central role in our proof of completeness, as they have in
previous completeness results of the stabiliser fragments for dimensions \(2\)
and \(3\) <cit.>. In particular, these constructions permit a nice
presentation of how graph states evolve under local Clifford operations.

Firstly, we extend \(\ZXp\) by multipliers, which are defined inductively

\begin{equation}
\tikzfig{figures/generators/multiplier}\quad.
\end{equation}

We also define inverted multipliers, using the standard notation for graphical
languages based on symmetric monoidal categories:

\begin{equation}
\tikzfig{figures/generators/multiplier_inverted}\quad.
\end{equation}

Now, it is straightforward using (Char) to see that, for any \(m \in
\N\),

\begin{equation}
\label{eq:multiplier_modular}
\tikzfig{figures/equations/multiplier_modular}\quad,
\end{equation}

and we can restrict the labels of multipliers to \(\Z_p\). Explicitly, then, for
\(x \in \Z_p^*\),

\begin{equation}
\label{eq:multiplier_explicit}
\tikzfig{figures/equations/multiplier_explicit}\quad.
\end{equation}

Multipliers satisfy the following equations under \(\ZXeq\): for any
\(x,y\in\Z_p\) and \(z\in\Z_p^*\),

\begin{equation}
\tikzfig{figures/equations/multiplier}
\end{equation}

which amounts to saying that the multipliers form a presentation of the field
\(\Z_p\). They also satisfy the following useful copy and elimination

\begin{equation}
\tikzfig{figures/equations/multiplier2}
\end{equation}

It is worth noting at this point, that multipliers are not flexsymmetric,
thus OCM is technically lost and the diagrams cannot be treated as decorated
graphs if multipliers are included. This is one reason, beyond simplicity, that
multipliers are treated as syntactic sugar rather than as generators of the
language. Howerer, we can somewhat recover OCM if we are prepared to allow
directed graphs with labelled edges instead.

Multipliers also satisfy the following equation:

\begin{equation}
\label{eq:hadamard_multiplier}
\tikzfig{figures/equations/hadamard_multiplier}\quad,
\end{equation}

so we can also unambiguously extend the calculus with H-boxes:

\begin{equation}
\label{eq:H_box_definition}
\tikzfig{figures/generators/hadamard_weighted}\quad.
\end{equation}

H-boxes exactly match the labelled Hadamard boxes introduced for the qutrit case
<cit.> when \(p = 3\). More explicitly, H-boxes
amount to repeated Hadamard wires:

\begin{equation}
\tikzfig{figures/equations/weighted_hadamard_multiedge}
\end{equation}

We have that for any \(x\in\Z_p\),

\begin{equation}
\label{eq:hadamard_OCM}
\tikzfig{figures/equations/hadamard_inverted}
\qand
\tikzfig{figures/equations/hadamard_edge}\quad.
\end{equation}

so that H-boxes are flexsymmetric, unlike multipliers.

\(\ZXeq\) proves the following equations:

\begin{equation}
\tikzfig{figures/equations/weighted_hadamard}
\end{equation}

It follows from this that the inverse Hadamard is just the \(-1\)-weighted
Hadamard box:

\begin{equation}
\tikzfig{figures/equations/hadamard_inverse_weight}\quad.
\end{equation}

§ REPRESENTING CLIFFORD STATES AS GRAPHS

Graph states are a now familiar tool of quantum information theory. Their
properties are intricately linked with those of the Clifford group and more
generally the stabiliser fragment. The original proof of completeness of the
qubit stabiliser ZX-calculus also made extensive use of graph states. The qubit
graph states have been generalised to the case of arbitrary (finite) dimension,
and we present them here through the lens of \(\ZXp\).

The idea is to associate a state in \(L^2(\Z_p)^{\otimes V}\) to any graph on a
set \(V\) of vertices. Unlike in the qubit case, it is more natural for qupits
to consider \(\Z_p\)-edge-weighted graphs. We make the choice of identifying
such a graph with its adjacency matrix \(G \in \Z_p^{V \times V}\). Then, the
corresponding graph state is defined to be

\begin{equation}
\ket{G} = \prod_{\substack{(u,v) \in V \\ u \neq v}} E_{u,v}^{G_{u,v}}
\bigotimes_{u\in{V}} \ket{0:X}_u.
\end{equation}

In other words, to obtain the graph state, first initialise each qupit in the
state \(\ket{0:X}\). Then, for each edge in \(G\) with weight \(G_{uv}\), apply
the entangling operation \(E_{uv}^{G_{uv}}\). Since \(E\) gates commute, they
can be applied in any order.

As a simple example, the graph

\begin{equation}
\label{eq:simple_graph}
\tikzfig{figures/simple_graph} \quad \qq{has adjacency matrix}
\begin{pmatrix}
0 & 3 & 1 \\
3 & 0 & 1 \\
1 & 1 & 0
\end{pmatrix},
\end{equation}

and is associated with the graph state \(E_{1,2} E_{1,3}^3 E_{2,3} (\ket{0:X}
\otimes \ket{0:X} \otimes \ket{0:X})\).

§.§ Graph states in \(\ZXp\)

The associated graph state is represented in \(\ZXp\) as:

\begin{equation}
\label{eq:simple_graph_state}
\tikzfig{figures/simple_graph_state}
\end{equation}

where the equality is obtained solely by fusing the green spiders. One
immediately recognises the graph from equation (<ref>) in the
RHS of equation (<ref>).

Here is a slightly more involved example:

\begin{equation}
\tikzfig{figures/graph}
\quad \qq{is associated to the state} \quad
\tikzfig{figures/graph_state}
\end{equation}

where each spider is connected to an output wire.

Hopefully, it should be clear that from these examples that for any given graph
\(G \in \Z_p^{V \times V}\), one can obtain the \(\ZXp\)-diagram for the corresponding
graph state by identifying each vertex with a green spider, and each edge with a
correspondingly weight H-edge. More formally:

A \(\ZXp\)-diagram is a graph state diagram if

* it contains only green spiders;

* every spider is connected to a single output by a plain wire;

* the spiders are connected only by H-edges.

Every graph state diagram is uniquely associated to a graph, and vice-versa.
Since we are going to reason about such diagrams in generality and without
referring to a specific graph, we use the following informal notation to
represent the \(\ZXp\)-diagram associated to \(G\):

\begin{equation}
\tikzfig{figures/graph_state_notation}\quad.
\end{equation}

In order to avoid having to track uninteresting scalars, we assume that the
interpretation of this diagram is normalised. This amounts to including, along
with the purely graph-theoretical part, a pair of scalars

\begin{equation}
\left( \tikzfig{figures/equations/soundness/sqroot_d_inv} \right)^{\otimes\abs{V}}
\qand
\left( \tikzfig{figures/equations/soundness/sqroot_d_unlabelled} \right)^{\otimes\abs{E}},
\end{equation}

where \(V\) is the set of vertices in \(G\) and \(E\) the set of edges. These
are simply the normalisation factors for states and entangling gates in G (see
equations (<ref>) and (<ref>)). It should
now be clear that

\begin{equation}
\ket{G} = \interp{\tikzfig{figures/graph_state_notation}}\quad.
\end{equation}

Note that this notation for graph states can be formalised using the
“scalable” construction <cit.>, but this would involve
introducing rather more machinery than we really need.

§.§ Manipulating graph states

Having shown how to represent graph states within \(\ZXp\), we now gives some
natural rules for manipulating diagrams involving them under \(\ZXeq\).

Two graph states \(\ket{G}\) and \(\ket{H}\) are said to be local Clifford
equivalent is there is a sequence of local Clifford operations that maps
\(\ket{G}\) to \(\ket{H}\). It was show in <cit.> that
any local Clifford equivalence can be decomposed as a sequence of elementary
local Clifford operations called local scaling and local
complementation. These are particularly nice operations since their actions
on a graph state \(\ket{G}\) are straightforward to understand at the level of
the graph \(G\) defining the graph state.

§.§.§ Pauli stabilisers

It is well-known that graph states admit simple Pauli stabilisers, namely, for
each \(v \in V\),

\begin{equation}
X_v^\gamma \prod_{w \in N(v)} Z_w^{\gamma G_{vw}} \ket{G} = \ket{G}.
\end{equation}

We can give a simple formulation of these rules within \(\ZXp\), and they can be
derived in \(\ZXeq\):

\(\ZXeq\) proves the Pauli stabiliser rules for graph states:

\begin{equation*}
\tikzfig{figures/equations/pauli_stabiliser},
\end{equation*}

where the red spiders is connected to vertex \(w\) in the graph \(G\), and
each neighbour \(k\) of \(w\) is connected to a green vertex with phase
\((\gamma G_{kw},0)\).

§.§.§ Local scaling

For any \(\gamma \in \Z_p^*\), the \(\gamma\)-scaling about a vertex
\(w\) in a graph \(G\) is given by:

\begin{equation}
(G \overset{\gamma}{\circ} w)_{uv} \coloneqq
\begin{cases}
\gamma G_{uv} \quad \text{if} \quad u = w \quad \text{or} \quad v = w;\\
G_{uv} \quad \text{otherwise}.
\end{cases}
\end{equation}

In other words, we apply a multiplicative scaling to all of the edges in the
neighbourhood of \(w\). For example:

\begin{equation}
\tikzfig{figures/local_scaling_example_lhs}
\quad \overset{\overset{\gamma}{\circ} w}{\longmapsto} \quad
\tikzfig{figures/local_scaling_example_rhs} \quad.
\end{equation}

Local scaling is derivable in \(\ZXeq\): for any graph \(G \in \Z_p^{N
\times N}\), \(\gamma \in \Z_p\) and \(w \in \{1,2,\cdots,N\}\), \(\ZXeq\)
proves that

\begin{equation}
\tikzfig{figures/equations/local_scaling} \quad,
\end{equation}

where in the LHS, the multiplier is connected to vertex \(w\).

§.§.§ Local complementation

For any \(\gamma \in \Z_d^*\), the \(\gamma\)-weighted local
\(\Z_d\)-complementation or \(\gamma\)-complementation about a vertex \(w\)
in a graph \(G \i  \Z_d^{V \times V}\) is defined as:

\begin{equation}
(G \overset{\gamma}{\star} w)_{uv} \coloneqq
\begin{cases}
G_{uv} + \gamma G_{uw} G_{wv} \qif u \neq v; \\
G_{uv} \qq{otherwise.}
\end{cases}
\end{equation}

This operation is somewhat harder than local scaling to get a good intuition
for. It essentially operates on “cones” in \(G\) with summit \(w\). The
simplest example is the following:

\begin{equation}
\tikzfig{figures/local_complementation_triangle_lhs}
\quad \overset{\overset{\gamma}{\star} w}{\longmapsto} \quad
\tikzfig{figures/local_complementation_triangle_rhs} \quad.
\end{equation}

In a more complicated graph, local complementation about \(w\) performs this
simple operation for every such “cone” with summit \(w\). For example,

\begin{equation}
\tikzfig{figures/local_complementation_example_lhs}
\quad \overset{\overset{\gamma}{\star} w}{\longmapsto} \quad
\tikzfig{figures/local_complementation_example_rhs} \quad.
\end{equation}

Local complementation is derivable in \(\ZXeq\): for any graph \(G \in \Z_p^{N
\times N}\), \(\gamma \in \Z_p\) and \(w \in \{1,2,\cdots,N\}\), \(\ZXeq\)
proves that

\begin{equation}
\tikzfig{figures/equations/local_complementation} \quad,
\end{equation}

where in the LHS, the red phase is connected to vertex \(w\), and each
neighbour \(v\) of \(w\) is connected to a green phase \((0,-\gamma G_{vw}^2)\).

Combining this with propositions <ref> and
<ref>, we get

For any graph \(G \in \Z_p^{N \times N}\), \(w \in \{1,2,\cdots,N\}\) and
\(x,y \in \Z_p\), \(\ZXeq\) proves that

\begin{equation}
\tikzfig{figures/equations/GS_red_rotation} \quad,
\end{equation}

where in the LHS, the red phase is connected to vertex \(w\), and each
neighbour \(v\) of \(w\) is connected to a green phase with labels
proportional to the edge weight \(G_{vw}\).

§ COMPLETENESS

We now have all the necessary tools to show that our equational theory is
complete. The structure of our proof is similar to the one used to show the
completeness in the qubit case <cit.>. However, if the
overall scheme is very similar, each step separately can involve different
approaches more suited to the qupit situation. The plan is as follows. We
identify a family of scalars, called elementary scalars, which correspond
to those which appear when applying the rewrites of \(\ZXeq\). We first show the
completeness up to non-zero elementary scalars, which allows us to work with
simpler diagrams without taking care of all the invertible scalars appearing
along the way. Then, we show the completeness for elementary scalars
independently, leading to a general proof of completeness. The proof of
completeness up to non-zero elementary scalars, goes like this:

* Take two diagrams with the same interpretation.

* Put them in GS+LC form.

* Define the notion of rGS+LC form for a pair of diagrams in which some vertices are marked. Then show that in a rGS+LC pair if a vertex is marked on one side, it must also be marked on the other side, else the two diagrams cannot have the same interpretation.

* Show that two diagram forming an rGS+LC pair such that their marked vertices matches and having the same interpretation are equal modulo the equational theory.

§.§ Elementary scalars

The following is standard from categorical quantum mechanics:

If \(A,B \in \ZXp[0,0]\), then \(\interp{A \otimes B} = \interp{A} \cdot
\interp{B} = \interp{A \circ B}\), where \(\cdot\) is the usual multiplication
on \(\C\) restricted to the monoid \(\mathbb{G}\).

Now, as when we were defining the group of phases \(\mathbb{P}_p\), the set of
normal forms for phases must depend on the prime \(p\) in question:

An elementary scalar is a diagram \(A \in \ZXp[0,0]\) which is a tensor
product of diagrams from the collection \(O_p \cup P \cup Q\): where

* if \(p \equiv 1 \mod 4\),

\begin{equation}
O_p = \left\{
\tikzfig{figures/universality/empty},
\scalebox{1.4}{$\star$}
\right\} \quad,
\end{equation}

* if \(p \equiv 3 \mod 4\),

\begin{equation}
O_p = \left\{
\tikzfig{figures/universality/empty},
\tikzfig{figures/equations/imaginary_scalar_normal_form},
\scalebox{1.4}{$\star$},
\tikzfig{figures/equations/imaginary_scalar_minus_normal_form}
\right\} \quad,
\end{equation}

\begin{equation}
P = \left\{
\tikzfig{figures/universality/empty},
\tikzfig{figures/equations/omega_scalar_normal_form}
\mid s \in \Z_p^* \right\} \quad,
\end{equation}

\begin{equation}
Q = \left\{
\tikzfig{figures/universality/sqrt_d},
\tikzfig{figures/universality/empty},
\tikzfig{figures/universality/sqrt_d_inv}
\mid r \in \Z \right\} \quad.
\end{equation}

If \(A,B \in \ZXp\), we say that \(A\) and \(B\) are equal up to an
elementary scalar if there is an elementary scalar \(C\) such that \(A = B
\otimes C\). In that case, we write \(A \simeq B\).

Comparing with the definition of \(\mathbb{G}\), the interpretation of the
elements of \(P\) correspond to powers of \(\omega\), the elements of \(Q\) to
(possible negative) powers of \(\sqrt{p}\), and the elements of \(O_p\) to
powers of \(-1\) or \(i\) depending on the value of \(p\). This remark will
naturally lead to the normal for for scalars in a few sections.

Now, as written, equality up to an elementary scalar might seem like a relation
that is not symmetric and therefore not an equivalence relation.

Every elementary scalar \(C \in \ZXp[0,0]\) has a multiplicative inverse, i.e.
an elementary scalar \(C^{-1} \in \ZXp[0,0]\) such that

\begin{equation}
C \otimes C^{-1} = C \circ C^{-1} = \tikzfig{figures/universality/empty}\quad.
\end{equation}

This is the content of lemmas <ref>,
<ref>, <ref>, <ref>
and axioms (Gauss) and (M-One).

In light of this fact, if \(A \simeq B\), there is an elementary scalar \(C\)
such that \(A = B \otimes C\), and then \(B = B \otimes C \otimes C^{-1} = A
\otimes C^{-1}\), so that \(B \simeq A\).

Every equation in \(\ZXeq\) can be loosened to equality up an elementary
scalar by erasing every part of the LHS and RHS diagrams which is disconnected
from the inputs and outputs.

This comes from a straightforward structural induction, and noting that every
scalar diagram which appears in the axiomatisation (figure <ref>)
can be straightforwardly rewritten under \(\ZXeq\) to an elementary scalar,
and thus can be ignored.

Probably the most important case of equality up to elementary scalars is the
completeness of the single-qupit Clifford groups, on which the entire proof of
completeness of the calculus rests. The fragment of \(\ZXp\) which corresponds
to \(\mathscr{C}_1\) is that generated by the \(1 \to 1\) diagrams under
sequential composition only:

\begin{equation*}
\tikzfig{figures/generators/r-phase} \quad\quad
\tikzfig{figures/generators/g-phase} \quad\quad
\tikzfig{figures/generators/multiplier_generator} \quad\quad
\tikzfig{figures/generators/weighted_hadamard}
\end{equation*}

We call any such diagram a single-qupit Clifford diagram or
\(\mathscr{C}_1\)-diagram.

If \(A \in \ZXp[1,1]\) is a single-qupit Clifford diagram, then \(\ZXeq\)
proves that

\begin{equation}
\tikzfig{figures/equations/c1_normal_form}\quad,
\end{equation}

for some \(s,t,u,v \in \Z_p\) and \(w \in \Z_p^*\). Furthermore,
this form is unique.

§.§ Relating stabiliser diagrams to graphs

In order to use the preceding tools in our completeness proof for the whole
stabiliser fragment, we need to understand how an arbitrary stabiliser diagram
can be related to a graph state diagram. Firstly, we rewrite any stabiliser
diagram \(D\) to a state using the Choi-Jamiolkowski isomorphism:

\begin{equation}
\label{eq:choi_isomorphism}
\tikzfig{figures/equations/choi_stabiliser_graph_LHS}
\quad{\Large\rightsquigarrow}
\tikzfig{figures/equations/choi_stabiliser_graph_RHS}
\end{equation}

Any diagram \(0 \to n\) obtained from the Choi-Jamiolkowski isomorphism
can be rewritten to a graph state diagram, with single qupit Clifford operations
acting on its output wires:

A GS+LC diagram is a \(\ZXp\)-diagram which consists of a graph state
diagram with arbitrary single-qupit Clifford operations applied to each
output. These associated Clifford operations are called vertex

Every stabiliser state \(\ZXp\)-diagram can be rewritten, up to elementary
scalars, to GS+LC form under \(\ZXeq\).

In other words, \(\ZXeq\) proves that, for any stabiliser \(\ZXp\)-diagram \(D : m
\to n\), there is a graph \(G\) on \(m+n\) vertices and a set of vertex
operators \((v_k)_{k=1}^{m+n}\) such that

\begin{equation}
\tikzfig{figures/equations/stabiliser_graph_LHS}
\quad\simeq\quad
\tikzfig{figures/equations/stabiliser_graph_RHS}
\end{equation}

and we need only consider the question of whether \(\ZXeq\) can prove the
equality of two GS+LC diagrams.

§.§ Completeness modulo elementary scalars

Now, as a first step, we show that \(\ZXeq\) can normalise any pair of diagrams
with equal interpretations, up to elementary scalars. In particular, as was
shown in the previous section, we can relax \(\ZXeq\) to reason about equality up to
elementary scalars by simply ignoring the scalar part of each rule, and make free
use of the “scalarless” equational theory. We will take care of the resulting
scalars in the next section.

This part of the completeness proof follows the general ideas of
<cit.>. The first step on the way to completeness is
to note that, considering a diagram in GS+LC form, where the vertex operators
have been normalised, we can obtain a yet more reduced diagram by absorbing as
much as possible of the vertex operators into local scalings and local
complementations. We then obtain the following form for the vertex operators:

A \(\ZXp\)-diagram is in reduced GS+LC (or rGS+LC) form if it is in
GS+LC form, and furthermore:

* All vertex operators belong to the following set:

\begin{equation}
R = \left\{ \tikzfig{figures/equations/c1_reduced} \,\middle|\, s,t \in \Z_p \right\}.
\end{equation}

* Two adjacent vertices do not have vertex operators that both include red spiders.

If \(D \in \ZXp\) is a Clifford diagram, then there is a diagram \(G
\in \ZXp\) in rGS+LC form such that \(\ZXeq \vdash D \simeq G\).

Then, given two diagrams with equal interpretations, taking them both to rGS+LC
makes the task of comparing the diagrams considerably easier. In particular, we
can guarantee that the corresponding vertex operators in each diagram always
have matching forms:

A pair of rGS+LC diagrams of the same type (i.e. whose graphs have the same vertex set
\(V\)) is said to be simplified if there is no pair of vertices \(q,p
\in V\) such that \(q\) has a red vertex operator in the first diagram but not
the second, \(q\) has a red vertex operator in the second diagram but not the
first, and \(q\) and \(p\) are adjacent in at least one of the diagrams.

Any pair \(A,B\) of rGS+LC diagrams of the same type (i.e. on the same vertex
set) can be simplified.

For the sake of clarity, we shall say that the vertex operator (or equivalently,
the vertex itself) is marked if it contains a red spider (i.e. it belongs
to the right-hand form of definition <ref>). Then, two diagrams with
the same interpretation can always be rewriten so that the marked vertices

Let \(C,D \in \ZXp\) be a simplified pair in rGS+LC form, then \(\interp{C} =
\interp{D}\) only if the marked vertices in $C$ and $D$ are the same.

Finally, we have enough control over the pair of diagrams to finish the
completeness proof:

\(\ZXeq\) is complete for \(\interp{-}\), i.e. if for any pair of
diagrams \(A,B \in \ZXp [0,n]\) with $n\neq 0$ , \(\interp{A} = \interp{B}\), then \(\ZXeq
\vdash A \simeq B\).

§.§ Completeness of the scalar fragment

Finally, we are ready to leap-frog off of the previous section into the full
completeness (including scalars). First, we need to find a normal form for
diagrams which evaluate to \(0\). In fact, we need pick one normal form for each
type \(m \to n\):

The “zero” scalar “destroys” diagrams: for any \(m,n \in \N\) and \(D \in
\ZXp[m,n]\),

\begin{equation*}
\tikzfig{figures/equations/zero_normal_forms}
\end{equation*}

We take the RHS diagram to be the “zero” diagram of type \(m \to n\).

Now, we say that a scalar \(C \in \ZXp[0,0]\) is in normal form if it is
either the zero diagram, or it belongs to the set

\begin{equation}
\label{eq:scalar_normal_form_p1}
\left\{
\tikzfig{figures/universality/empty},
\scalebox{1.4}{$\star$}
\right\}
\otimes \left\{
\tikzfig{figures/universality/empty},
\tikzfig{figures/equations/omega_scalar_normal_form}
\mid s \in \Z_p^* \right\}
\otimes \left\{
\tikzfig{figures/universality/sqrt_d},
\tikzfig{figures/universality/empty},
\tikzfig{figures/universality/sqrt_d_inv}
\mid r \in \Z \right\},
\end{equation}

if \(p \equiv 1 \mod 4\), or to the set

\begin{equation}
\label{eq:scalar_normal_form_p3}
\left\{
\tikzfig{figures/universality/empty},
\tikzfig{figures/equations/imaginary_scalar_normal_form},
\scalebox{1.4}{$\star$},
\tikzfig{figures/equations/imaginary_scalar_minus_normal_form}
\right\}
\otimes \left\{
\tikzfig{figures/universality/empty},
\tikzfig{figures/equations/omega_scalar_normal_form}
\mid s \in \Z_p^* \right\}
\otimes \left\{
\tikzfig{figures/universality/sqrt_d},
\tikzfig{figures/universality/empty},
\tikzfig{figures/universality/sqrt_d_inv}
\mid r \in \Z \right\}.
\end{equation}

when \(p \equiv 3 \mod 4\). It is straightforward to see, by evaluating
\(\interp{-}\) on each element, that the sets in
equations (<ref>) or (<ref>)
contain exactly one diagram for each scalar in \(\mathbb{G}_p \setminus \{0\}\)
(and the zero diagram \(\tikzfig{figures/equations/zero_diagram}\) corresponds
to \(0 \in \mathbb{G}_p\)). Comparing with the definition of \(\mathbb{G}_p\) in
equations (<ref>)-(<ref>), the first factor in the tensor
product corresponds to powers of \(-1\) or powers of the imaginary unit \(i\);
the second factor corresponds to powers of \(\omega\); and the third factor
to powers of \(\sqrt{p}\).

\(\ZXeq\) proves any scalar diagram equal to a scalar from either
equations (<ref>) or (<ref>)
(depending on the congruence of \(p\) modulo \(4\)), or to the zero scalar
\(\tikzfig{figures/equations/zero_diagram}\).

The completeness for the whole stabiliser fragment follows immediately:

The equational theory \(\ZXeq\) is complete for \(\Stab\), i.e. for any
\(\ZXp\)-diagrams \(A\) and \(B\), if \(\interp{A} = \interp{B}\), then
\(\ZXeq \vdash A = B\). Put more formally, there is a commutative diagram

\begin{equation}
\begin{tikzcd}
\ZXp & {\ZXp / \ZXeq} \\
& \Stab
\arrow["{\interp{-}}"', from=1-1, to=2-2]
\arrow[from=1-2, to=2-2]
\arrow["p", twoheadrightarrow, from=1-1, to=1-2]
\end{tikzcd}
\end{equation}

where \(p\) is the projection \(\ZXp \to \ZXp / \ZXeq\) and the vertical arrow
is an isomorphism of categories.

§ MIXED STATES AND RELATIONS

In this last section we use the work of <cit.> to extend our completeness result to the mixed-state case. We then unravel the connection to the Lagrangian relation investigated in <cit.>.

§.§ A complete graphical language for $\textup{CPM}( \mathsf{Stab}_p )$

We now extend our completeness result form $ \mathsf{Stab}_p $ to $\textup{CPM}( \mathsf{Stab}_p )$, the category of completely positive maps corresponding to mixed state stabiliser quantum mechanics, see <cit.> for a formal definition. We will rely on the discard construction of <cit.> to define a graphical language \({(\ZXp)}^{\ground}\). It consists in adding to the equational theory one generator, the discard $\ground :1\to 0$ and equations stating that this generator erases all isometries. In \(\mathsf{Stab}_p \), the isometries are generated by the following diagrams:

The equations to add are then:

A new interpretation $\interp{\_}: {\ZXp}^{\ground} \to \textup{CPM}( \mathsf{Stab}_p )$ is defined as $\interp{\tikzfig{ground}}: \rho \mapsto \Tr(\rho)$ for the ground and for all \(\ZXp\)-diagram $D:n\to m$:

$\interp{\tikzfig{figures/D} }^{\ground} : \rho \mapsto \interp{\tikzfig{figures/D} }^{\dagger} \rho \interp{\tikzfig{figures/D} }$.

Corollary 22 of <cit.> provides a sufficient condition for the previous construction to extend to a universal and complete graphical language for $\mathsf{Stab}_p $ into a universal complete graphical language for $\textup{CPM}( \mathsf{Stab}_p )$. This condition is for $\mathsf{Stab}_p $ to have enough isometries, meaning (we use here a little stronger condition than in <cit.>) that for all maps $f:A \to B\otimes X$ and $g:A \to B\otimes Y$ such that:

there is an isometry $V: X\to Y$ in $\mathsf{Stab}_p $ such that:

To prove this, we will use arguments similar to the proof that $\mathsf{Stab}_2 $ has enough isometry. Everything relies on the following lemma:

Given any bipartition of the outputs of a $\ZXp$-diagram $D:0\to n+m$. We can find unitaries $A$ and $B$ in $\mathsf{Stab}_p $ such that:

Using this we can prove:

$\mathsf{Stab}_p $ has enough isometries.

The proof is exactly the same as the qubit case, see the proof of Proposition 18 in <cit.>. It then follows directly from <cit.> that:

\({(\ZXp)}^{\ground}\) is universal and complete for $\textup{CPM}( \mathsf{Stab}_p )$.

§.§ Co-isotropic relations

It has been shown in <cit.> that \(\textrm{CPM}(\Stab)\) is equivalent to the
category of affine co-isotropic relations up to scalars. More formally, we endow
\(\Z_p^2\) with the symplectic form

\begin{equation}
\omega\left(
\begin{bmatrix}
a \\ b
\end{bmatrix},
\begin{bmatrix}
c \\ d
\end{bmatrix}
\right) = ad - bc,
\end{equation}

and \(\Z_p^{2m} = \bigoplus_m \Z_p^2\) with the direct sum symplectic form.

The symmetric monoidal category \(\AffCoIsoRel\) has as objects \(\N\), and as
morphisms, relations \(R : \Z_p^{2m} \to \Z_p^{2n}\) such that \(R\) viewed as a
subset of \(\Z_p^m \times \Z_p^n\) is an affine co-isotropic subspace thereof.

Since <cit.> works in the scalarless ZX-calculus, we need
to add one extra axiom, which suffices to eliminate all remaining (non-zero)
scalars in \(\Stab\): we impose the rule (Mod) that \(p = 1\).
Diagrammatically, this amounts to quotienting \((\ZXp)^{\ground}\) by the
following rule:

\begin{equation}
\tikzfig{figures/scalarless_axiom}
\end{equation}

Then we can give an interpretation \(\left[ - \right]\) of
\({(\ZXp)}^{\ground}\) making it universal and complete for \(\AffCoIsoRel\),
and which is defined uniquely by the commutative diagram

\begin{equation}
\begin{tikzcd}
{(\ZXp)^{\ground}} & \AffCoIsoRel \\
{\mathrm{CPM}(\Stab)} & {\mathrm{CPM}(\Stab) / \textsc{(Mod)}}
\arrow[dashed,"{\left[ - \right]}", from=1-1, to=1-2]
\arrow["{\interp{-}}"', from=1-1, to=2-1]
\arrow[twoheadrightarrow, from=2-1, to=2-2]
\arrow[leftrightarrow, from=1-2, to=2-2]
\end{tikzcd}
\end{equation}

Explicitly, it is given by the identity on objects, \([m] = m\), and is defined
on morphisms by: for \(x,y \in \Z_p\) and \(z \in \Z_p^*\)

\begin{align*}
\left[ \tikzfig{figures/generators/r-spider_labelless} \right]
&= \left\{ \left(
\bigoplus_{k=1}^m \begin{bmatrix}
a \\ b_k
\end{bmatrix} ,
\bigoplus_{k=1}^n \begin{bmatrix}
-a \\ -c_k
\end{bmatrix}
\right) \,\middle|\, a,b_k,c_k \in \Z_p \qand \sum_k b_k = \sum_k c_k \right\} \\
\left[ \tikzfig{figures/generators/g-spider_labelless} \right]
&= \left\{ \left(
\bigoplus_{k=1}^m \begin{bmatrix}
a_k \\ c
\end{bmatrix} ,
\bigoplus_{k=1}^n \begin{bmatrix}
b_k \\ c
\end{bmatrix}
\right) \,\middle|\, a,b_k,c_k \in \Z_p \qand \sum_k a_k = \sum_k b_k \right\} \\
\left[ \tikzfig{figures/generators/r-unit} \right]
&= \left\{ \left(
\bullet,
\begin{bmatrix}
-1 & 0 \\
-y & -1
\end{bmatrix} \begin{bmatrix} v \\ 0 \end{bmatrix} + \begin{bmatrix} -x \\ 0 \end{bmatrix}
\right) \,\middle|\, v \in \Z_p \right\} \\
\left[ \tikzfig{figures/generators/g-unit} \right]
&= \left\{ \left(
\bullet,
\begin{bmatrix}
1 & -y \\
0 & 1
\end{bmatrix} \begin{bmatrix} 0 \\ v \end{bmatrix} + \begin{bmatrix} 0 \\ x \end{bmatrix}
\right) \,\middle|\, v \in \Z_p \right\} \\
\left[ \tikzfig{figures/generators/hadamard} \right]
&= \left\{ \left(
\vb{v},
\begin{bmatrix}
0 & -1 \\
1 & 0
\end{bmatrix} \vb{v}
\right) \,\middle|\, \vb{v} \in \Z_p^2 \right\} \\
\left[ \tikzfig{figures/generators/multiplier_generator_z} \right]
&= \left\{ \left(
\vb{v},
\begin{bmatrix}
z & 0 \\
0 & z^{-1}
\end{bmatrix} \vb{v}
\right) \,\middle|\, \vb{v} \in \Z_p^2 \right\}
\end{align*}

Note that all of these are actually affine Lagrangian relations. The only
generator which has a co-isotropic but not Lagrangian semantics is the discard

\begin{equation}
\left[ \tikzfig{ground} \right]
= \left\{ \left( \vb{v}, \bullet \right) \,\middle|\, \vb{v} \in \Z_p^2 \right\}
\end{equation}

As pointed out in <cit.>, the related category of affine Lagrangian relations
over the field \(\R[x,y]/(xy-1)\) can be used to represent a fragment of
electrical circuits. We expect that the axiomatisation of
figure <ref> can be adapted to that setting, but leave this for a
future article.

§.§ Geometrical interpretation

The previous interpretation corresponds to a geometric intuition. All Clifford gates can be interpreted as affine transformations of the torus $\mathbb{Z}_p \times \mathbb{Z}_p $. This torus can be identified as a phase space, the position and momentum coordinates, $q$ and $p$ corresponding respectively to the first and second wire in the previous section semantics. In this section we will take as an example the case $p=5$.

The red triangle here will allow us to illustrate the geometrical action of stab.

The Pauli phase gates, acts as translations along the vertical or horizontal axis. The multiplication gates acts as a scaling. The Hadamard gate corresponds to a $\frac{\pi}{2}$-rotation and the antipode to a $\pi$-rotation. Finally, the pure Clifford gates corresponds to shears.

§ CONCLUSION

We have constructed a ZX-calculus which captures the stabiliser fragment in odd
prime dimensions, whilst retaining many of the “nice” features of the qubit
ZX-calculus. Of course, there are a few obvious questions that we leave for
future work.

First amongst these is the question of whether a fully universal calculus can be
obtained from the ideas we used here. The spiders we have used here labelled
with elements \(a,b \in \Z_p \times \Z_p\) and which can be interpreted as
polynomials \(x \mapsto ax+bx^2\) which parametrise the phases of the spider.
Adding one additional term of degree \(3\) is already sufficient to obtain a
universal calculus in prime dimensions (strictly) greater than \(3\)
<cit.>. In fact, one might as well add all higher order of
polynomials (mod \(p\)) since access to such higher degrees will hopefully
prove useful in finding commutation relations for the resulting spiders.

Secondly, it remains to be seen how to formulate a universal ZX-calculus for
non-prime dimensions, even for just the stabiliser fragment. For this, the
methods in this article are clearly inadequate: for example local scaling is no
longer an invertible operation and thus certainly not in the Clifford group.

Finally, the set of axioms we provide here is probably not minimal. It would be
nice to see if a simplified version can be obtained, as was done in
<cit.> for the qubit case.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

titleCategorical Quantum Mechanics

titleProperties of the Extended Clifford Group with Applications to SIC-POVMs and MUBs

journaltitleNew Journal of Physics
shortjournalNew J. Phys.
titleThe ZX-calculus Is Complete for Stabilizer Quantum Mechanics

journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleMaking the Stabilizer ZX-calculus Complete for Scalars

journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity

titleCompleteness of the ZH-calculus

Verein zur Förderung des Open Access Publizierens in den Quantenwissenschaften

shorttitleThere and Back Again
titleThere and Back Again: A Circuit Extraction Tale

journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleA Simplified Stabilizer ZX-calculus

journaltitleTheory and Application of Categories
titleProps in Network Theory

journaltitleTheory and Application of Categories
titleA Compositional Framework for Passive Linear Networks

titleAn Efficient Algorithm to Recognize Locally Equivalent Graphs in Non-Binary Case

journaltitleIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
titleGraphical Calculus for Qutrit Systems

eprintclasscs, math
shorttitleString Diagram Rewrite Theory II
titleString Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure

annotationPUB27 New York, NY
journaltitleJournal of the ACM (JACM)
shorttitleString Diagram Rewrite Theory I
titleString Diagram Rewrite Theory I: Rewriting with Frobenius Structure

shorttitleString Diagram Rewrite Theory III
titleString Diagram Rewrite Theory III: Confluence with and without Frobenius

journaltitleJournal of Pure and Applied Algebra
shortjournalJournal of Pure and Applied Algebra
titleInteracting Hopf Algebras

titleWhen Only Topology Matters

Université de Lorraine

titleWielding the ZX-calculus, Flexsymmetry, Mixed States, and Scalable Notations

titleSZX-calculus: Scalable Graphical Quantum Reasoning

Schloss Dagstuhl - Leibniz-Zentrum für Informatik

booktitle46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece
titleCompleteness of Graphical Languages for Mixed States Quantum Mechanics

titleColored Props for Large Scale Graphical Reasoning

titleGraphical Structures for Design and Verification of Quantum Error Correction

issn0305-4470, 1361-6447
journaltitleJournal of Physics A: Mathematical and General
shortjournalJ. Phys. A: Math. Gen.
titleValence Bond Solid Formalism for D-Level One-Way Quantum Computation

journaltitleNew Journal of Physics
shortjournalNew J. Phys.
shorttitleInteracting Quantum Observables
titleInteracting Quantum Observables: Categorical Algebra and Diagrammatics

Cambridge University Press

shorttitlePicturing Quantum Processes
titlePicturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning

eventtitleWeekly Online ZX Meeting
titleA Symplectic Setting for Mixed Stabiliser Circuits

University of Oxford

titleRelational Semantics for Quantum Algorithms

* Entry 'comfort_relational_nodate' (style/bibliography.bib): Invalid format 'To Appear' of date field 'date' - ignoring

eprintclassmath-ph, physics:quant-ph
titleA Graphical Calculus for Lagrangian Relations

titleA Linearized Stabilizer Formalism for Systems of Finite Dimension

titleFast and Effective Techniques for T-count Reduction via Spider Nest Identities

titleThe ZX Calculus Is a Language for Surface Code Lattice Surgery

titleGraph-Theoretic Simplification of Quantum Circuits with the ZX-calculus

journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleVerifying the Steane Code with Quantomatic

Berlin, Heidelberg

Springer Berlin Heidelberg

booktitleAutomata, Languages and Programming
isbn978-3-642-14161-4 978-3-642-14162-1
titleRewriting Measurement-Based Quantum Computations with Generalised Flow

journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleVerifying the Smallest Interesting Colour Code with Quantomatic

journaltitlePhysics Letters A
titleStandard Form of Qudit Stabilizer Groups

journaltitleChaos, Solitons & Fractals
shortjournalChaos, Solitons & Fractals
titleFault-Tolerant Quantum Computation with Higher-Dimensional Systems

titleA Consolidating Review of Spekkens' Toy Theory

issn1050-2947, 1094-1622
journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleQudit Versions of the Qubit "Pi-over-Eight" Gate

titleA Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics

titleReducing T-count with the ZX-calculus

titleClassical Simulation of Quantum Circuits with Partial and Graphical Stabiliser Decompositions

journaltitleJournal of Lie Theory
titleAn Explicit Construction of the Metaplectic Representation over a Finite Field

titleA Universal Completion of the ZX-calculus

journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleDepicting Qudit Quantum Mechanics and Mutually Unbiased Qudit Theories

journaltitleElectron. Notes Theor. Comput. Sci.
titleDagger Compact Closed Categories and Completely Positive Maps: (Extended Abstract)

shorttitleClassifying Complexity with the ZX-Calculus
titleClassifying Complexity with the ZX-Calculus: Jones Polynomials and Potts Partition Functions

titleZX-calculus for the Working Quantum Computer Scientist

titleA Near-Optimal Axiomatisation of ZX-Calculus for Pure Qubit Quantum Mechanics

journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleQutrit ZX-calculus Is Complete for Stabilizer Quantum Mechanics

titleA Non-Anyonic Qudit ZW-calculus

shorttitleQufinite ZX-calculus
titleQufinite ZX-calculus: A Unified Framework of Qudit ZX-calculi

journaltitleElectronic Proceedings in Theoretical Computer Science
shortjournalElectron. Proc. Theor. Comput. Sci.
titleQutrit Dichromatic Calculus and Its Universality

journaltitleFrontiers in Physics
shortjournalFront. Phys.
titleQudits and High-Dimensional Quantum Computing

Ecole Normale Superieure de Lyon

shorttitleInteracting Hopf Algebras
titleInteracting Hopf Algebras: The Theory of Linear Systems

issn1050-2947, 1094-1622
journaltitlePhysical Review A
shortjournalPhys. Rev. A
titleQuantum Computation Based on D-Level Cluster States
Some lemmas from elementary number theory

\(-1\) is a square mod \(p\) if and only if \(p\) is congruent to \(1 \mod

For any odd prime \(p\) and \(x,y \in \Z_p\), if neither \(x\) nor \(y\) is
square, then \(xy\) is a square.

The map \(x \mapsto x^2\) is an endomorphism of \(\Z_p\) with kernel \(\{-1,
1\}\). In other words, the image of this map, the subgroup \(Q_p\) of squares
in \(\Z_p^*\), must have index \(2\), and then \(\Z_p^* / Q_p\) is a two
element group. If neither \(x\) nor \(y\) is square, \(xQ_p = yQ_p\) whence
\((xy)Q_p = (xQ_p)(yQ_p) = (xQ_p)^2 = Q_p\), so that \(xy \in Q_p\).

For any prime \(p\) and \(x \in \Z_p\), at least one of \(-1\), \(x\) or
\(-x\) is a square.

§ PROOF OF UNIVERSALITY

[of theorem <ref>]
By proposition <ref>, in odd prime dimensions the
generalised Clifford groups are generated by

\begin{equation}
\label{eq:C1_generators}
\interp{\tikzfig{figures/circuit/S}} = S\qc
\interp{\tikzfig{figures/circuit/hadamard}} = H \qand
\interp{\tikzfig{figures/circuit/CZ}} = E.
\end{equation}

Since computational basis states and effects are easily represented as:

\begin{equation}
\label{eq:stabiliser_states}
\interp{\tikzfig{figures/circuit/Z_state}} = \ket{x} \qand \interp{\tikzfig{figures/circuit/Z_effect}} = \bra{x},
\end{equation}

the standard interpretation is clearly universal for the stabiliser fragment
by the functoriality of \(\interp{-}\).

§ PROOF OF SOUNDNESS

§.§ Proof of soundness

[of theorem <ref>]
We prove that each of the equations in figure <ref> is sound, and
this extends to the entire equational theory by functoriality of
\(\interp{-}\).

Firstly, straightforward calculation shows that, for any \(x,y \in \Z_p\),

\begin{equation}
\label{eq:scalars}
\interp{\tikzfig{figures/equations/soundness/sqroot_d_inv}} = \frac{1}{\sqrt{p}}
\qc
\interp{\tikzfig{figures/equations/soundness/sqroot_d}} = \sqrt{p} \omega^{-2^{-2}xz},
\qand
\interp{\tikzfig{figures/equations/soundness/sqroot_d_phaseless}} = \sqrt{p}.
\end{equation}

We also have

\begin{equation}
\interp{\tikzfig{figures/equations/soundness/d_phase}} = \sum_{k\in\Z_p} \omega^{2^{-1}(xk+yk^2)},
\end{equation}

and using the harmonic series for the Kronecker delta,
\(\interp{\tikzfig{figures/equations/soundness/d_pauli_phase}} = p\delta_{x,0}\).

(Zero) and (One) then follow immediately from
equation (<ref>).

(Fusion) For any \(a,b,c,d \in \Z_p\),

\begin{align}
\interp{\,\tikzfig{figures/equations/soundness/Fusion_LHS}\,}
&=\left( \sum_{k\in\Z_p} \omega^{2^{-1}(ak+bk^2)} \ket{k}^{\otimes n}
\bra{k}^{\otimes m} \otimes \mathrm{id}_{m'-1} \right) \\
&\quad\quad\quad \circ \left( \mathrm{id}_{n-1}
\otimes \sum_{\ell\in\Z_p} \omega^{2^{-1}(c\ell+d\ell^2)}
\ket{\ell}^{\otimes n'} \bra{\ell}^{\otimes m'} \right) \nonumber \\
&= \sum_{k,\ell\in\Z_p} \omega^{2^{-1}(ak+bk^2)} \omega^{2^{-1}(c\ell+d\ell^2)} \ket{k}^{\otimes n}
\bra{k}^{\otimes m-1} \ip{k}{\ell} \ket{\ell}^{\otimes n'-1} \bra{\ell}^{\otimes m'} \\
&= \sum_{k,\ell\in\Z_p} \delta_{k,\ell} \omega^{2^{-1}(ak+bk^2)} \omega^{2^{-1}(c\ell+d\ell^2)} \ket{k}^{\otimes n}
\bra{k}^{\otimes m-1} \ket{\ell}^{\otimes n'-1} \bra{\ell}^{\otimes m'} \\
&= \sum_{k\in\Z_p} \omega^{2^{-1}((a+c)k+(b+d)k^2)} \ket{k}^{\otimes n+n'-1} \bra{k}^{\otimes m+m'-1} \\
&= \interp{\,\tikzfig{figures/equations/soundness/Fusion_RHS}}
\end{align}

(Colour) For any \(a,b\in\Z_p\),

\begin{align}
\interp{\tikzfig{figures/equations/soundness/Colour_LHS}}
&=\left( \sum_{j\in\Z_p} \dyad{j:X}{j:Z} \otimes \cdots \otimes
\sum_{j\in\Z_p} \dyad{j:X}{j:Z} \right) \\
&\quad\quad\quad \circ \sum_{k\in\Z_p} \omega^{2^{-1}(ak+bk^2)} \dyad{k:Z}{k:Z} \nonumber \\
&\quad\quad\quad \circ \left( \sum_{\ell\in\Z_p} \dyad{\ell:Z}{-\ell:X} \otimes \cdots \otimes
\sum_{\ell\in\Z_p} \dyad{\ell:Z}{-\ell:X} \right) \nonumber \\
&= \sum_{k\in\Z_p} \omega^{2^{-1}(ak+bk^2)} \dyad{k:X}{-k:X} \\
&= \interp{\tikzfig{figures/equations/soundness/Colour_RHS}}
\end{align}

(Shear) For any \(a,c,d\in\Z_p\),

\begin{align}
\interp{\tikzfig{figures/equations/soundness/Shear_LHS}}
&= \sqrt{p}\omega^{-2^{-2}ac} \sum_{j,k,\ell\in\Z_p} \omega^{2^{-1}aj} \omega^{2^{-1}(ck+dk^2)} \omega^{2^{-1}a\ell} \dyad{j}{j} \dyad{-k:X}{k:X} \dyad{\ell}{\ell} \\
&= \sqrt{p}\omega^{-2^{-2}ac} \sum_{j,k,\ell\in\Z_p} \omega^{2^{-1}aj} \omega^{2^{-1}(ck+dk^2)} \omega^{2^{-1}a\ell} \omega^{-jk} \omega^{-k\ell} \dyad{j}{\ell} \\
&= \sqrt{p}\omega^{-2^{-2}ac} \sum_{j,k,\ell\in\Z_p} \omega^{2^{-1}aj} \omega^{2^{-1}a\ell} \omega^{2^{-1}k(dk+c-2j-2\ell)} \dyad{j}{\ell} \\
&= \sqrt{p}\omega^{-2^{-2}ac} \sum_{j,k,\ell\in\Z_p} \omega^{2^{-1}aj} \omega^{2^{-1}a\ell} \omega^{2^{-1}(k+2^{-1}a)(d(k+2^{-1}a)+c-2j-2\ell)} \dyad{j}{\ell} \\
&= \sqrt{p}\omega^{2^{-3}da^2} \sum_{j,k,\ell\in\Z_p} \omega^{2^{-1}k(dk+ad+c-2j-2\ell)} \dyad{j}{\ell} \\
&= \sqrt{p}\omega^{2^{-3}da^2} \sum_{j,k,\ell\in\Z_p} \omega^{2^{-1}(ck+adk+dk^2)} \omega^{-jk} \omega^{-k\ell}\dyad{j}{\ell} \\
&= \sqrt{p}\omega^{2^{-3}da^2} \sum_{k\in\Z_p} \omega^{2^{-1}(ck+adk+dk^2)} \dyad{-k:X}{k:X} \\
&= \interp{\tikzfig{figures/equations/soundness/Shear_RHS}}
\end{align}

\begin{align}
\interp{\tikzfig{figures/equations/soundness/Char_LHS}}
&= \sqrt{p^p} \sum_{j,k\in\Z_p} \dyad{-k:X}{k:X}^{\otimes p} \ket{j}^{\otimes p} \bra{j} \\
&= \sum_{j,k\in\Z_p} \omega^{-pjk} \ket{-k:X} \bra{j} \\
&= \sum_{j,k\in\Z_p} \ket{-k:X} \bra{j} \\
&= \interp{\tikzfig{figures/equations/soundness/Char_RHS}}
\end{align}

\begin{align}
\interp{\tikzfig{figures/equations/soundness/Bigebra_LHS}}
&= p \sum_{i,j,k,\ell\in\Z_p} \ket{-k:X} \ket{-\ell:X} \ip{k:X}{i} \ip{\ell:X}{i} \ip{k:X}{j} \ip{\ell:X}{j} \bra{i} \bra{j} \\
&= \frac{1}{p} \sum_{i,j,k,\ell\in\Z_p} \omega^{-ik} \omega^{-i\ell} \omega^{-jk} \omega^{-j\ell} \ket{-k:X} \dyad{-\ell:X}{i} \bra{j} \\
&= \frac{1}{p^3} \sum_{\substack{ i,j,k,\ell \\ m,n,o,p }\in\Z_p} \omega^{-ik} \omega^{-i\ell} \omega^{-jk} \omega^{-j\ell}
\omega^{-km}\omega^{-n\ell}\omega^{io}\omega^{pj} \ket{m} \dyad{n}{o:X} \bra{p:X} \\
&= \frac{1}{p^3} \sum_{\substack{ i,j,k,\ell \\ m,n,o,p }\in\Z_p} \omega^{i(o-k-\ell)} \omega^{j(p-k-\ell)}
\omega^{-km}\omega^{-n\ell} \ket{m} \dyad{n}{o:X} \bra{p:X} \\
&= \frac{1}{p} \sum_{\substack{ k,\ell \\ m,n,o,p }\in\Z_p} \delta_{o,k+\ell} \delta_{p,k+\ell}
\omega^{-km}\omega^{-n\ell} \ket{m} \dyad{n}{o:X} \bra{p:X} \\
&= \frac{1}{p} \sum_{k,\ell,m,n\in\Z_p} \omega^{-km}\omega^{-n\ell} \ket{m} \dyad{n}{k+\ell:X} \bra{k+\ell:X} \\
&= \frac{1}{\sqrt{p}} \sum_{k,\ell,m,n\in\Z_p} \omega^{k(n-m)} \ket{m} \ket{n} \ip{n}{-k-\ell:X} \bra{k+\ell:X} \bra{k+\ell:X} \\
&= \sqrt{p} \sum_{k,\ell,m,n\in\Z_p} \delta_{n,m} \ket{m} \ket{n} \ip{n}{-\ell:X} \bra{\ell:X} \bra{\ell:X} \\
&= \sqrt{p} \sum_{m,\ell\in\Z_p} \ket{m} \dyad{m}{m} \dyad{-\ell:X}{\ell:X} \bra{\ell:X} \\
&= \interp{\tikzfig{figures/equations/soundness/Bigebra_RHS}}
\end{align}

\begin{align}
\interp{\tikzfig{figures/equations/soundness/Copy_LHS}}
&= \sqrt{p} \sum_{j,k\in\Z_p} \omega^{2^{-1}xj} \ip{k}{-j:X} \ket{k}\ket{k} \\
&= \sum_{j,k\in\Z_p} \omega^{2^{-1}xj} \omega^{-jk} \ket{k}\ket{k} \\
&= p \sum_{k\in\Z_p} \delta_{k,2^{-1}x} \ket{k}\ket{k} \\
&= p \ket{2^{-1}x}\ket{2^{-1}x} \\
&= \sum_{j\in\Z_p} \omega^{-2^{-1}xj} \ket{j:X} \sum_{k\in\Z_p} \omega^{-2^{-1}xk} \ket{k:X} \\
&= \sum_{j\in\Z_p} \omega^{2^{-1}xj} \ket{-j:X} \sum_{k\in\Z_p} \omega^{2^{-1}xk} \ket{-k:X} \\
&= \interp{\tikzfig{figures/equations/soundness/Copy_RHS}}
\end{align}

\begin{equation}
\interp{\tikzfig{figures/equations/soundness/G-Elim_LHS}}
\sum_{k\in\Z_p} \dyad{k}{k}
\interp{\tikzfig{figures/equations/soundness/G-Elim_RHS}}
\end{equation}

\begin{align}
\interp{\tikzfig{figures/equations/soundness/R-Elim_LHS}}
&= \sum_{k\in\Z_p} \dyad{-k:X}{k:X} \dyad{-j:X}{j:X}
= \sum_{k\in\Z_p} \delta_{k,-j} \dyad{-k:X}{j:X} \\
&= \sum_{k\in\Z_p} \dyad{j:X}{j:X}
= \interp{\tikzfig{figures/equations/soundness/R-Elim_RHS}}
\end{align}

(Mult) For any \(z \in \Z_p^*\),

\begin{align}
\interp{\tikzfig{figures/equations/soundness/Mult_RHS}}
% &= p \sum_{a,b,c,d\in\Z_p} \omega^{2^{-1}z^{-1}a^2} \omega^{2^{-1}zb^2} \omega^{2^{-1}z^{-1}c^2} \ip{a:Z}{-b:X} \ip{b:X}{c:Z} \ip{c:Z}{d:Z} \dyad{a:Z}{d:X} \\
&= \sum_{a,b,c,d\in\Z_p} \omega^{2^{-1}z^{-1}a^2} \omega^{2^{-1}zb^2} \omega^{2^{-1}z^{-1}c^2} \omega^{-ab} \omega^{-bc} \delta_{c,d} \dyad{a:Z}{d:X} \\
&= \sum_{a,b,c\in\Z_p} \omega^{2^{-1}z^{-1}a^2} \omega^{2^{-1}zb^2} \omega^{2^{-1}z^{-1}c^2} \omega^{-ab} \omega^{-bc} \dyad{a:Z}{c:X} \\
&= \sum_{a,b,c\in\Z_p} \omega^{2^{-1}z^{-1}(a-zb+c)^2} \omega^{-z^{-1}ac} \dyad{a:Z}{c:X} \\
&= \left( \sum_{b\in\Z_p} \omega^{2^{-1}z^{-1}b^2} \right) \sum_{a,c\in\Z_p} \omega^{-z^{-1}ac} \dyad{a:Z}{c:X} \\
&= \left( \sum_{b\in\Z_p} \omega^{2^{-1}z^{-1}b^2} \right) \sqrt{p} \sum_{a\in\Z_p} \dyad{a:Z}{z^{-1}a:Z} \\
&= \left( \sum_{b\in\Z_p} \omega^{2^{-1}z^{-1}b^2} \right) \sqrt{p} \sum_{a\in\Z_p} \dyad{za:Z}{a:Z} \\
&= \left( \sum_{b\in\Z_p} \omega^{2^{-1}z^{-1}b^2} \right) \sum_{a,c\in\Z_p} \omega^{-zac} \dyad{c:X}{a:Z} \\
&= \left( \sum_{b\in\Z_p} \omega^{2^{-1}z^{-1}b^2} \right) \sqrt{p^z} \sum_{a,c\in\Z_p} \dyad{c:X}{c:X}^{\otimes z} \ket{a:Z}^{\otimes z}\bra{a:Z} \\
&= \interp{\tikzfig{figures/equations/soundness/Mult_LHS}}.
\end{align}

follows using equation (73) of <cit.>:

\begin{equation}
\interp{\tikzfig{figures/equations/soundness/Gauss_LHS}}
= \sum_{j\in\Z_p} \omega^{2^{-1}zj^2}
= -i^{\frac{p+3}{2}} \ell_p(z)
= -i^{\frac{p+3}{2}} (-1)^{\chi_p(z)}
= \interp{\tikzfig{figures/equations/soundness/Gauss_RHS}}.
\end{equation}

where we have used the fact that \(\ell_p(1) = 1\) (the Legendre symbol mod
\(p\) of 1), and also that \(\ell_p(z) = (-1)^{\chi_p(z)}\) whenever \(z \neq

\begin{equation}
\interp{\tikzfig{figures/equations/soundness/M-One_LHS}}
= (-1) (-1)
= 1
= \interp{\tikzfig{figures/equations/soundness/M-One_RHS}}.
\end{equation}

\begin{align}
\interp{\tikzfig{figures/equations/soundness/M-Elim_LHS}}
&= \sum_{j,k\in\Z_p} \omega^{2^{-1}(ak+bk^2)} \bra{k:X}\ket{-zj}\bra{j} \\
&= \sum_{j,k\in\Z_p} \omega^{2^{-1}(ak+bk^2)} \frac{\omega^{2^{-1}k zj}}{\sqrt{p}} \bra{j} \\
&= \frac{1}{\sqrt{p}} \sum_{j,k\in\Z_p} \omega^{2^{-1}(ak+bk^2)} \omega^{2^{-1}k zj} \bra{j} \\
&= \sum_{k\in\Z_p} \omega^{2^{-1}(ak+bk^2)} \bra{-zk:X} \\
&= \sum_{k\in\Z_p} \omega^{2^{-1}(-az^{-1}k+bz^{-2}k^2)} \bra{k:X} \\
&= \interp{\tikzfig{figures/equations/soundness/M-Elim_RHS}}.
\end{align}

§ PROOF OF COMPLETENESS

§.§ Elementary derivations

Products of Hadamards are antipodes:

\begin{equation*}
\tikzfig{figures/equations/hadamard_product}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/hadamard_product_proof}
\end{equation*}

Hadamards and antipodes commute:

\begin{equation*}
\tikzfig{figures/equations/hadamard_antipode}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/hadamard_antipode_proof}
\end{equation*}

The inverse Hadamard is a product of Hadamards:

\begin{equation*}
\tikzfig{figures/equations/hadamard_inverse}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/hadamard_inverse_proof}
\end{equation*}

Units absorb antipodes:

\begin{equation*}
\tikzfig{figures/equations/antipode_unit}
\end{equation*}

The red equation is basically a subcase of (M-Elim):

\begin{equation*}
\tikzfig{figures/equations/antipode_unit_proof_red}
\end{equation*}

and the green rule is obtained using (Colour):

\begin{equation*}
\tikzfig{figures/equations/antipode_unit_proof_green}
\end{equation*}

The Hadamards admit simple Euler decompositions:

\begin{equation*}
\tikzfig{figures/equations/hadamard_euler}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/hadamard_euler_proof}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/hadamard_euler_proof_inverse}
\end{equation*}

The Hopf identity is derivable in \(\ZXeq\):

\begin{equation*}
\tikzfig{figures/equations/hopf}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/hopf_proof}
\end{equation*}

Then, the second rule follows using the colour change meta-rule.

The following rules hold between the “elementary” scalars:

\begin{equation*}
\tikzfig{figures/equations/scalar_elementary}
\end{equation*}

\begin{equation}
\tikzfig{figures/equations/scalar_elementary_proof}
\end{equation}

Self-loops on green spiders can be eliminated:

\begin{equation*}
\tikzfig{figures/equations/loop}
\end{equation*}

We include the colour-swapped version of this rule for completeness, even
though it no longer includes a genuine self-loop.

\begin{equation*}
\tikzfig{figures/equations/loop_proof}
\end{equation*}

The red version is obtained using (Colour).

The following rules hold between the “phase” scalars: for any \(a,b \in
\Z_p\),

\begin{equation*}
\tikzfig{figures/equations/scalar_phase}
\end{equation*}

\begin{equation}
\tikzfig{figures/equations/scalar_phase_proof}
\end{equation}

The rule \(\tikzfig{figures/equations/red_green_dot}\) is immediate using

Green units absorb red rotations and vice-versa:

\begin{equation*}
\tikzfig{figures/equations/unit_rotation_elim}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/unit_rotation_elim_proof_green}
\end{equation*}

The scalars in the bigebra law can be simplified to:

\begin{equation*}
\tikzfig{figures/equations/bigebra_simplified}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/bigebra_simplified_proof}
\end{equation*}

The green co-multiplication copies antipodes:

\begin{equation*}
\tikzfig{figures/equations/antipode_copy}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/antipode_copy_proof}
\end{equation*}

The bigebra law holds for arbitrary arities: for any \(m,n \in \N\),

\begin{equation*}
\tikzfig{figures/equations/bigebra_arbitrary}\quad,
\end{equation*}

where in the diagram on the LHS, there are \(m\) green and \(n\) red spiders,
and each green spider is connected to each red spider by a single wire.

The cases \(m=0\) or \(n=0\) correspond to the copy rules.
The case \(n=1\) is the antipode copy rule (lemma <ref>) and
the case \(m=1\) is trivial by the green identity rule.
The case \(n=2,m=2\) is lemma <ref>.
The general case follows from a straightforward induction (which furthermore
is analogous to the qubit case).

The antipode can be rewritten as a multiplication:

\begin{equation*}
\tikzfig{figures/equations/antipode_multiplier}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/antipode_multiplier_proof}
\end{equation*}

For any \(x,y \in \Z_p\),

\begin{equation*}
\tikzfig{figures/equations/antipode_phase}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/antipode_phase_proof_green}
\end{equation*}

The rule for red spiders is obtained from the green rule:

\begin{equation*}
\tikzfig{figures/equations/antipode_phase_proof_red}\quad.
\end{equation*}

For any \(x,y \in \Z_p\) and \(m,n \in \N\),

\begin{equation*}
\tikzfig{figures/equations/antipode_spider}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/antipode_spider_proof}
\end{equation*}

The rule for red spiders is obtained using (Colour) like in the proof
of lemma <ref>.

Green spiders copy red Pauli phases, and vice-versa: for any \(x \in
\Z_p\),

\begin{equation*}
\tikzfig{figures/equations/pauli_copy_phase}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/pauli_copy_phase_proof}
\end{equation*}

The other rule is obtained using (Colour).

§.§ Multipliers

Parallel multipliers sum: for any \(x,y \in \Z_p\):

\begin{equation*}
\tikzfig{figures/equations/multiplier_sum}
\end{equation*}

This is a straightforward consequence of (Spider).

For any \(z \in \Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/multiplier_elim}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/multiplier_elim_proof_green}
\end{equation*}

The right rule is obtained using (Colour) as previously.

For any \(x,y \in \N\),

\begin{equation*}
\tikzfig{figures/equations/multiplier_product}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/multiplier_product_proof}
\end{equation*}

For any \(x \in \Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/multiplier_inverse}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/multiplier_inverse_proof}
\end{equation*}

The second equality follows from the (Colour) meta-rule.

Lemmas <ref>-<ref> suffice to prove
proposition <ref> and <ref>, so we
consider those rules proved from this point on, and adopt the multiplier

Spiders copy invertible multipliers: for any \(x \in \Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/multiplier_copy}
\end{equation*}

(a) follows from direct calculation using the definition of multipliers:

\begin{equation*}
\tikzfig{figures/equations/multiplier_copy_proof_green}
\end{equation*}

Then (b) is obtained from (a) using already established properties of the

\begin{equation*}
\tikzfig{figures/equations/multiplier_copy_proof_red}
\end{equation*}

[of proposition <ref>]
This proposition now follows straightforwardly using
lemma <ref>, the definition of H-boxes (equation
(<ref>)) and proposition <ref>.

The action of multipliers on spiders is given by, for any \(x \in \Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/multiplier_spider}
\end{equation*}

This follows straightforwardly using lemma <ref> and

Any pure-Clifford states can be represented in both the red and green
fragment: for any \(x \in \Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/clifford_states}
\end{equation*}

Firstly, we prove the subcase \(x=1\) of (a):

\begin{equation*}
\tikzfig{figures/equations/clifford_states_proof_green}
\end{equation*}

Then the general case for any invertible \(x\) follows using
lemma <ref>.

(b) follows once again using (Colour).

\begin{equation*}
\tikzfig{figures/equations/scalar_i_elim}
\end{equation*}

Since \(1\) is always a square:

\begin{equation*}
\tikzfig{figures/equations/scalar_i_elim_proof}
\end{equation*}

For any \(z\in\Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/scalar_gauss_elim}
\end{equation*}

If \(z\) is a square, then there is some \(\alpha \in \Z_p\) such that

\begin{equation*}
\tikzfig{figures/equations/scalar_gauss_elim_proof}
\end{equation*}

If \(-z\) is a square, then there is again some \(\alpha \in \Z_p\) such that

\begin{equation*}
\tikzfig{figures/equations/scalar_gauss_elim_proof_2}
\end{equation*}

Now, if neither \(z\) nor \(-z\) is a square, then by
corollary <ref>, \(-1\) must be a square. We then

\begin{equation*}
\tikzfig{figures/equations/scalar_gauss_elim_proof_3}
\end{equation*}

For any \(z\in\Z_p\),

\begin{equation*}
\tikzfig{figures/equations/scalar_omega_elim}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/scalar_omega_elim_proof}
\end{equation*}

where we have freely used lemma <ref> to commute antipodes
and spiders throughout.

If \(p \equiv 3 \mod 4\),

\begin{equation*}
\tikzfig{figures/equations/scalar_imaginary_elim}
\end{equation*}

If \(p \equiv 3 \mod 4\), \(-1\) is not a square, so that

\begin{equation*}
\tikzfig{figures/equations/scalar_imaginary_elim_proof}
\end{equation*}

All the elementary “zero” diagrams are equal:

\begin{equation*}
\tikzfig{figures/equations/zero_elementary}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/zero_elementary_proof}
\end{equation*}

The “zero” diagram absorbs unlabelled elementary scalars:

\begin{equation*}
\tikzfig{figures/equations/zero_amplitudes}
\end{equation*}

First note that

\begin{equation*}
\tikzfig{figures/equations/zero_amplitudes_proof_1}
\end{equation*}

so that

\begin{equation*}
\tikzfig{figures/equations/zero_amplitudes_proof_2}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/zero_amplitudes_proof_3}
\end{equation*}

The zero diagram absorbs the phase scalars: for any \(x \in \Z_p\) and \(z \in
\Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/zero_phases}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/zero_phases_proof_1}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/zero_phases_proof_2}
\end{equation*}

Quadratic phases satisfy the following multiplication law: for any \(x,y \in
\Z_p^*\)

\begin{equation*}
\tikzfig{figures/equations/scalar_gauss_multiplication}
\end{equation*}

This follows from applications of (Gauss) and
lemma <ref>.

For any \(x,y\in\Z_p\),

\begin{equation*}
\tikzfig{figures/equations/scalar_omega_multiplication}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/scalar_omega_multiplication_proof}
\end{equation*}

where we have freely used lemma <ref> to commute antipodes
and spiders throughout.

The Euler decomposition of the Hadamards can be “improved” to:

\begin{equation*}
\tikzfig{figures/equations/hadamard_euler_better}
\end{equation*}

This follows from applying lemma <ref> to the
decomposition of lemma <ref>, then using
lemma <ref> to simplify the scalar.

Hadamard loops correspond to pure-Clifford operations: for any \(x \in \Z_p\)
and \(z \in \Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/H_loop}
\end{equation*}

The case \(x=0\) is clear by decomposing the H-box. We begin by proving the
case \(x=1\):

\begin{equation*}
\tikzfig{figures/equations/H_loop_proof_green}
\end{equation*}

The general case can be obtained by decomposing the weighted H-box into \(x\)
H-loops using the sum rule from proposition <ref>.
Then, under the assumption that the weight is invertible, the red version once
again follows using (Colour) and the equations of
proposition <ref>:

\begin{equation*}
\tikzfig{figures/equations/H_loop_proof_red}
\end{equation*}

[of proposition <ref>]

\begin{equation*}
\tikzfig{figures/equations/pauli_stabiliser_proof}
\end{equation*}

[of proposition <ref>]
This follows straightforwardly using proposition <ref>.

For any \(x,y \in \Z_p^*\),

\begin{equation*}
\tikzfig{figures/equations/local_complementation_triangle}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/local_complementation_triangle_proof}
\end{equation*}

and we can eliminate the \(\tikzfig{figures/equations/scalar_i}\) scalar using
lemma <ref>.

Let \(\Sigma\) be a \(\Z_p\)-weighted star graph on \(N \in \N\) vertices,
i.e.  it is a tree with \(N-1\) leaves. Order the vertices such that the
first vertex is the only internal vertex, and it follows that all of the edges
have weights \(\Sigma_{1w}\) for \(w\) ranging from \(2\) to \(N\). Then,

\begin{equation*}
\tikzfig{figures/equations/local_complementation_tree}
\end{equation*}

where \(\Sigma \overset{\gamma}{\star} 1\) is the graph obtained by adding an
edge weighted in \(\gamma \Sigma_{1m}\Sigma{1n}\) between the wires connected
to each pair of vertices \(m,n \neq 1\).

The proof is by induction on the size \(N\) of the tree. Assume the lemma is
true for any tree of size \(N-1\).
First, bend all the wires with green phases into inputs:

\begin{equation*}
\tikzfig{figures/equations/local_complementation_tree_proof_bent}
\end{equation*}

\begin{equation*}
\tikzfig{figures/equations/local_complementation_tree_proof_1}
\end{equation*}

Then, we recognise the subtree with head \(1\) and leaves \(3\) to \(N\),
which is thus a tree of size \(N-1\), to which we can apply the inductive

\begin{equation*}
\tikzfig{figures/equations/local_complementation_tree_proof_2}
\end{equation*}

In the last step, we have pulled out the “head” of the \(N-1\) tree before
applying lemma <ref>, since the \(\Sigma_{1w}\)-weighted
Hadamards on each edge to the head are left unchanged by the local

Then, copy each \(\Sigma_{1w}\)-weighted Hadamard through the corresponding
red spider on its right (which changes its colour and multiplies the weight by
\(-1\)), and copy the multiplier and antipode through the green spiders below
and to the left respectively. Fusing the resulting green spiders we get:

\begin{equation*}
\tikzfig{figures/equations/local_complementation_tree_proof_3}
\end{equation*}

Bending the inputs back to outputs completes the proof.

[of proposition <ref>]
The proof of this proposition is rather cumbersome to write in standard
\(\ZXp\). We give a sketch of the proof, and leave writing it out formally to
future work, since it has a much clearer form in the scalable
\(\ZXp\)-calculus.

The idea is to split out the subtree of \(G\) with head \(w\) and leaves each
of the neighbours of \(w\). Then, one applies
lemma <ref>, and adds the resulting edges into
\(G\) using the addivitity of parallel H-boxes
(proposition <ref>).

§.§ Main completeness proofs

[of proposition <ref>]
The single-qupit Clifford group is generated by the invertible generators
under sequential composition. It therefore suffices to show that the
composition of either of the above diagrams with such a generator can be
rewritten to the claimed form. Now, every rewrite rule, except (Zero)
can be interpreted as an equality up to an invertible scalar, if we simply
ignore the parts of the equations disconnected from both the inputs and the
outputs. Thus, we can freely use any of these rules in our proof of
normalisation up to invertible scalars, and any equation derivable without

For the multipliers this is very straightforward: for any
\(x \in \Z_d^*\),

\begin{equation*}
\tikzfig{figures/equations/c1_multiplier_forms}
\end{equation*}

We can ignore the weight since this can be extracted as
a multiplier and then the previous proof applies. Then, for the first normal

\begin{equation*}
\tikzfig{figures/equations/c1_hadamard_forms_10}
\end{equation*}

we need to split subcases based on the value of \(v\). If \(v=0\), then we

\begin{equation*}
\tikzfig{figures/equations/c1_hadamard_forms_11}
\end{equation*}

where in the last step we have used (Shear) and (Spider)
several times to commute the Paulis on the right back into the leftmost red
and green spiders.

If \(v \neq 0\), then,

\begin{equation*}
\tikzfig{figures/equations/c1_hadamard_forms_12}
\end{equation*}

The second normal form can be done in one go.

\begin{equation*}
\tikzfig{figures/equations/c1_hadamard_forms_2}
\end{equation*}

The red phase is once again very straightforward: let \(x,y \in \Z_d\), then,

\begin{equation*}
\tikzfig{figures/equations/c1_phase_forms_red}
\end{equation*}

The green phases are more involved. Firstly, note that we can ignore the
multiplier, since we have:

\begin{equation*}
\tikzfig{figures/equations/c1_phase_forms_green_multipliers}
\end{equation*}

and \(x,y\) are arbitrary. Then, the Pauli part can be straightforwardly taken
care of using (Shear) to commute it through to the green spider on
the right. Finally, we can view \(\tikzfig{figures/equations/green_phase_0y}\)
as the \(y\)-fold composition of
\(\tikzfig{figures/equations/green_phase_01}\), so that we have reduced the
proof to the normalisation of:

\begin{equation*}
\tikzfig{figures/equations/c1_phase_forms_green}
\end{equation*}

On the right (in dashed lines) we recognise the composition of a Hadamard and
a normal form, which we have already shown can be normalised. This done, we
obtain the composition of a red spider and a normal form, which we have also
already shown to be normalisable. Thus, we are done.

As for the second normal form, we have:

\begin{equation*}
\tikzfig{figures/equations/c1_phase_forms_green_2}
\end{equation*}

and we have again reduced to previously solved cases.

Unicity follows from the fact that none of these forms are equivalent, and
there are therefore \(p^3(p^2 - 1)\) distinct forms, which matches the
cardinality of the single qupit Clifford group.

[of proposition <ref>]
Assume w.l.o.g. that the diagram \(D\) has type \(0 \to n\) (i.e.  we
consider that the diagram has already been turned into a state via
equation (<ref>)), and furthermore that it contains no
multipliers (equivalently, they have been unpacked into the sugarless calculus
using equation (<ref>)). Then, transform \(D\) as

* Use (Colour) to change every red spider into a green one,
surrounded by Hadamards. The resulting diagram consists of only green
spiders and Hadamards.

* Use (G-Elim) to add a green spider between any two subsequent
Hadamards. The diagram now consists of only green spiders, connected either
by plain edges or H-edges.

* Use (Spider) to fuse any two spiders connected by plain edges,
to eliminate any loops, and use lemma <ref> to eliminate any
H-edge loops. The resulting diagram contains no loops, and furthermore
spiders are connected only by H-edges.

* Use the following rule from proposition <ref>:

\begin{equation}
\tikzfig{figures/equations/hadamard_sum}
\end{equation}

to fuse all H-edges between two spiders into a single weighted H-edge or no

* Use (G-Elim) and proposition <ref> to

\begin{equation}
\tikzfig{figures/equations/spider_graph_split}\quad,
\end{equation}

which allows one to split any spider connected to more than one output into
several green spiders, each connected to exactly one output.

The resulting diagram is nearly in GS+LC form, except it contains “internal”
vertices which are not connected to an output. Diagrams in this form have been
called graph-like in the literature. However, we can eliminate these
internal vertices as follows. Let \(u\) be such a vertex,, and let \((a,b)\)
be  its phase. If \(u\) has no neighbours, then it is an elementary scalar
diagram which we can ignore.

Otherwise, assume \(u\) has a neighbour \(v\) which is also connected to an
output of the diagram. Then, we can eliminate the phase at \(u\) through the
following manipulation. Throughout, we use local dilations
(proposition <ref>) and local complementations
(corollary <ref>) on the rest of the graph freely. We can
ignore the green spiders introduced by corollary <ref>
since they are absorbed into the phases of the graph vertices, and track only
the red spiders introduced which are the only “problematic” spiders that
take us away from GS+LC form.

Then, we can eliminate vertex \(u\) as follows:

\begin{equation*}
\tikzfig{figures/equations/eliminate_internal}
\end{equation*}

where in the second step we have used the Euler decomposition of the Hadamard
(lemma <ref>). The resulting green units are connected via
a normal wire to a single other green spider, to which they can be fused
using (Spider).

We still need to treat the case where \(u\) has only neighbours which are not
connected to an output. In that case, letting \(v\) be any neighbour of \(u\),
we can still eliminate \(u\) using a very similar argument and relying on the
normal form for single-qupit operators. The first step is analogous to the
previous case:

\begin{equation*}
\tikzfig{figures/equations/eliminate_internal_2}
\end{equation*}

Normalising the \(\mathscr{C}_1\)-diagram on \(v\) using
proposition <ref>, we obtain one of two forms which are
essentially equivalent since we have

\begin{equation*}
\tikzfig{figures/equations/eliminate_internal_3}
\quad \qand \quad
\tikzfig{figures/equations/eliminate_internal_4}
\end{equation*}

for some \(u,v,s,t \in \Z_p\) and \(w \in \Z_p^*\). Then, pulling the
multiplier and red spider into a local scaling and local complementation
acting on the rest of the graph, we get:

\begin{equation*}
\tikzfig{figures/equations/eliminate_internal_5}
\end{equation*}

As a result, by the end of this procedure, we have eliminated \(u\) without
reintroducing any new internal vertices, so we can repeat this process to
eliminate each internal vertex in the diagram. The resulting diagram will then
be in GS+LC form.

[of proposition <ref>]
By proposition <ref>, every stabiliser diagram is equivalent to
some GS+LC diagram, and furthermore, the vertex operators can be brought into
the normal form of proposition <ref>. Using
proposition <ref>, the multiplier part of this normal form
can immediately be absorbed into a local scaling of the graph.

We now need to eliminate the leftmost red spider of the normal form. Consider
the vertex operator acting on vertex \(u\) of the graph. If \(u\) has no
neighbours, we can use lemma <ref> to eliminate the red
spider (up to a scalar in \(\mathbb{G}\)). Otherwise, \(u\) has at least one
neighbour. In this case, we can use lemma <ref> to
“copy” the red spider into a green spider on each neighbour of \(u\).

As in the qubit case, the set \(R\) is not stable under pre-composition by a
green spider. However, by the proof of proposition <ref>,
we see that, after normalisation, this operation applied to any element of
\(R\) does not increase the number of red spiders. Thus, applying this
procedure at most \(2\abs{V}\) times maps every vertex operator to one of the
forms in \(R\).

In order to prove the second part of the simplification, assume that the
preceding procedure has been applied to the diagram, so that all vertex
operators are in \(R\). Let \(u,v\) be neighbouring vertices such that the
vertex operators of both \(u\) and \(v\) contain a red spider. We are going to
use a sequence of local complementations at \(u\) and \(v\) to eliminate the
red spiders on both \(u,v\). Since we have just shown that the green spider
these operations enact on neighbours can be corrected and the vertex operators
brought back to \(R\), and that local complementations and scalings preserve
the GS+LC form, we ignore this action and consider only the part of the
diagram connected to \(u\) and \(v\):

\begin{equation*}
\tikzfig{figures/equations/rGS+LC_paired_reds}
\end{equation*}

Then, normalising the vertex operators, we obtain

\begin{equation*}
\tikzfig{figures/equations/rGS+LC_paired_reds_2}
\end{equation*}

The red spiders can be eliminated using the previous strategy for mapping the
vertex operators to \(R\), and so we have removed the pair of neighbouring red
spiders. Repeating this process for each such pair renders a diagram in rGS+LC

[of proposition <ref>]
Suppose this is not the case, i.e. there are vertices \(u,v\) such that \(u\)
has a red vertex operator in \(A\) but not \(B\), \(v\) has a red vertex
operator in \(B\) but not \(A\), and \(u,v\) are neighbours in \(A\). Then we
perform a manipulation entirely analogous to the proof of
proposition <ref> in the diagram \(A\):

\begin{equation*}
\tikzfig{figures/equations/rGS+LC_simple}
\end{equation*}

Then, after normalisation (proposition <ref>) and using
proposition <ref> to bring the diagram back to rGS+LC form, the
vertex operator for \(u\) no longer contains a red vertex in \(A\) and the
vertex operator for \(v\) contains a red vertex. Since we can do this for any
pair of such red vertices in \(A\) and \(B\), it is clear that we can can
simplify the pair of diagrams.

[of theorem <ref>]
Let \(A \in \ZXp[0,0]\), then \(A\) consists of a tensor product of connected
scalar diagrams. We first show that \(A\) can be rewritten to a tensor product
of elementary scalars. If this is not already the case, pick some connected
scalar diagram \(A'\) contained in \(A\). This diagram \(A'\) contains at
least one red or green spider, from which we can extract a unit:

\begin{equation}
\tikzfig{figures/equations/scalar_normalisation_units}
\end{equation}

where \(B \in \ZXp[0,1]\). By theorem <ref> and the normal form for
the single-qupit Clifford group (proposition <ref>), we
can rewrite \(B\) to one of the forms

\begin{equation}
\tikzfig{figures/equations/scalar_normalisation_unit_forms}
\end{equation}

since we know that these forms cover all single qupit Clifford states.
Simplifying a bit, we therefore only need to consider the following forms:

\begin{equation}
\label{eq:scalar_normalisation_all_scalars}
\tikzfig{figures/equations/scalar_normalisation_all_scalars}
\end{equation}

The first of these is already an elementary scalar, and if \(s\) or \(t\) is
\(0\), the second is also. If \(s=0\), the third diagram is also elementary.
Thus, we can assume that \(t\neq 0 \neq s\) and treat both middle diagrams in
one go:

\begin{equation}
\tikzfig{figures/equations/scalar_normalisation_green}
\end{equation}

and both of these diagrams can be normalised using (M-Elim) and
Finally, the last scalar from
equation (<ref>) can be rewritten to:

\begin{equation}
\tikzfig{figures/equations/scalar_normalisation_last}.
\end{equation}

We have shown that \(A\) can be rewritten to a tensor product of elementary
scalars. If this tensor product contains a zero diagram, then the whole
diagram equal to the zero diagram by proposition <ref>.
Otherwise, \(A\) can further be rewritten to a scalar in normal form using the
multiplication rules for elementary scalars, which are given by
(M-One), lemmas <ref> and
<ref>, up to applying (Gauss) to
decompose quadratic scalars.

[of theorem <ref>]

First, $D$ can be put in GS-LC form. This allows to decompose $D$ in the following form:

Where $X$ and $Y$ are compositions of E-gates constituting the edges within the same partition together with local Clifford gates, and $G$ is a bipartite graph-state gathering all vertices having a neighbor in a different partition and all corresponding edges. Thus, we see that without loss of generality we can restrict to the case where $D$ is a bipartite graph-state.

Assuming that $D$ is a bipartite graph-state with partitions of size $n$ and $m$ with $n\leq m$ we show how to find $A$ and $B$ such that:

Let's start with $n$ Bell's pair. Plugging Generalized Hadamard boxes we get the following graph state:

Now, let's say we want to add an edge with weight $w$ between the vertices $x$ and $y$ of this graph, to do so we first add an edge of weight $1$ between $x'$ and $y$ and apply the right local complementation to $x'$ to obtain the desired edge. Finally we clean up all the unwanted edges inside the partition by using the conveniant $E$-gates. The process is sketched in the following diagrams:

At the end, when all desired edges have been obtained, we still have to take care of the edges between $x$ and $x'$, but since we only kept vertices which are linked to the other partition in the final $D$, we know there is a neighbor $t$ that can be use to take care of this edge in the same way we used $x'$ before, first we add an edge between $t$ and $x'$, then we apply the needed local complementation on $t$ and finally we clean up the edges internal to the partitions.

This give up the wanted bipartite graph-state $D$ which conclude the proof.

[of <ref>]
Let's assume that there is a marked vertices $v$ in $C$ which is not marked in $D$. If $v$ is isolated in $C$ and not in $D$ then the two interpretations are obviously different. The same goes if $v$ is isolated in both diagram since then we can clearly differentiate the two corresponding states. So the only case remaining is when $v$ has neighbors in both diagrams.

We then apply to both diagram the same unitary, first a green Clifford map on the chosen vertex and appropriate gates for each edges in the neighborhood of $v$ in $C$. In $C$ we have:

And in $D$:

Here we compute up to local Cliffords on the wires. Thus, we see that in $C$, $v$ is now disconnected while it isn't in $D$. Then $\interp{D}\neq \interp{C}$.

[of Theorem <ref>]
We only show it for state by map-state duality.

First we rewrite $A$ and $B$ into a simplified pair of rGS-LC diagrams $A'$ and $B'$. So, the marked vertices are the same. It only remain to show that the graph state part with . But if we apply the gates corresponding to the edges in $A'$ to both diagrams, then we obtain a completely disconected graph in $A'$. And the two interpretation can only be equals if $B'$ is also now completely disconnected. It then follows that the edges in both diagrams were the same.

Finally, the only way for the interpretations to be the same is that all phases in the green vertices are equals, and then $A'$ can be rewritten in $B'$. So \(\Stab
\vdash A = B\).