# Simpler Presentations for Many Fragments of Quantum Circuits

Colin Blake

► To cite this version:

Colin Blake. Simpler Presentations for Many Fragments of Quantum Circuits. 2026. hal-05502157

HAL Id: hal-05502157

https://hal.science/hal-05502157v1

Preprint submitted on 10 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Simpler Presentations for Many Fragments of Quantum Circuits

Colin Blake

Inria Mocqua and Université de Lorraine, CNRS, LORIA, F-54000 Nancy, France

## Abstract

Equational reasoning is central to quantum circuit optimisation and verification: one replaces subcircuits by provably equivalent ones using a fixed set of rewrite rules viewed as equations. We study such reasoning through finite equational theories, presenting restricted quantum gate fragments as symmetric monoidal categories (PROPs), where wire permutations are treated as structural and separated cleanly from fragment-specific gate axioms. For six widely used near-Clifford fragments: qubit Clifford, real Clifford, Clifford+T (up to two qubits), Clifford+CS (up to three qubits) and CNOT-dihedral, we transfer the completeness results of prior work into our PROP framework. Beyond completeness, we address minimality (axiom independence). Using uniform separating interpretations into simple semantic targets, we prove minimality for several fragments (including all arities for qubit Clifford, real Clifford, and CNOT-dihedral), and bounded minimality for the remaining cases. Overall, our presentations significantly reduce rule counts compared to prior work and provide a reusable categorical framework for constructing complete and often minimal rewrite systems for quantum circuit fragments.

**2012 ACM Subject Classification** Theory of computation → Quantum computation theory

**Keywords and phrases** Quantum circuits, Clifford group, qutrit, equational theories

**Digital Object Identifier** 10.4230/LIPIcs...

**Category** Regular research paper

**Funding** This work is supported by the Plan France 2030 through the PEPR integrated project EPiQ (ANR-22-PETQ-0007) and the HQI platform (ANR-22-PNCQ-0002); by the European Union through the MSCA Staff Exchanges project QCOMICAL (Grant Agreement ID: 101182520); and by the Maison du Quantique MaQuEst.

**Acknowledgements** I thank my PhD advisors Simon Perdrix and Miriam Backens for reviews of early versions of the article. I also thank Noé Delorme for many discussions, early presentations of the Clifford and Real Clifford fragments, and for trying to derive some rules with me.

## 1 Introduction

Optimisation and verification of quantum circuits are typically performed by *equational reasoning*: a circuit is transformed by replacing a subcircuit with another and justifying the replacement by a finite set of circuit identities [12, 10]. For a fixed gate signature, this practice is formalised as an *equational theory*, namely a set of well-typed equations between circuits, closed under sequential and parallel composition [11, 18, 14]. With respect to an intended interpretation in terms of unitary operators, a rule set is *complete* if it derives every equality between circuits that have the same denotation.

In addition to completeness, we study *axiom independence* and *minimality* [6, 2, 20]. An axiom is independent if it is not derivable from the other axioms of the same theory, and a finite presentation is minimal if all its axioms are independent. Minimal presentations are of foundational interest because they isolate the irreducible algebraic content of a fragment; they are also relevant for automated rewriting and proof search, where redundant rules increase the search space and complicate termination and confluence analysis [13, 9].

<figure><img src="image_2.png" /></figure>
## XX:2 Simpler Presentations for Many Fragments of Quantum Circuits

Finite, complete presentations are known for several fragments close to the Clifford group, including *n*-qubit Clifford operators [19], real Clifford [17], CNOT-dihedral [1], 2-qubits Clifford+T [3], 3-qubits Clifford+CS [4], and *n*-qutrits Clifford [15]. Moreover, for universal circuit languages, finite complete axiomatisations are known [8, 7] and require rules of unbounded arity [6]. This motivates a systematic study of fragments in which one can obtain presentations that are simultaneously finite, complete, and minimal.

To formalise equational reasoning, we work with a standard string-diagrammatic syntax in which a circuit has a fixed number of wires, and the two operations of sequential and parallel composition are primitive [11, 18]. Many circuit presentations treat permutations implicitly, allowing wire crossings implicitly without counting them as gates. We make this convention explicit by working in a setting in which swaps are available as *structural* morphisms and satisfy the usual coherence axioms for symmetric monoidal categories [16, 11, 18]. In Section 2 we formalise this distinction using the PRO/PROP terminology: a PRO has only sequential and parallel composition, while a PROP additionally provides symmetry as part of the ambient structure [16, 14, 11].

<table><caption>Table 1 Gate signatures studied in this paper.</caption><thead><tr><th>Fragment</th><th>Dimension</th><th>Non-structural generators</th></tr></thead><tbody><tr><td>Qubit Clifford</td><td>2</td><td>ω<sub>8</sub>: 0 → 0, [-H], [-S]: 1 → 1, ⊕: 2 → 2</td></tr><tr><td>Real Clifford</td><td>2</td><td>Ο: 0 → 0, [-H], [-Z]: 1 → 1, ⊕: 2 → 2</td></tr><tr><td>Clifford+T</td><td>2</td><td>ω<sub>8</sub>: 0 → 0, [-H], [-T]: 1 → 1, ⊕: 2 → 2</td></tr><tr><td>Clifford+CS</td><td>2</td><td>ω<sub>8</sub>: 0 → 0, [-H], [-S]: 1 → 1, ⊕: 2 → 2</td></tr><tr><td>CNOT-dihedral</td><td>2</td><td>ω<sub>8</sub>: 0 → 0, [-X], [-T]: 1 → 1, ⊕: 2 → 2</td></tr><tr><td>Qutrit Clifford</td><td>3</td><td>ω<sub>12</sub>: 0 → 0, [-H], [-S]: 1 → 1, ⊕: 2 → 2</td></tr></tbody></table>

**Contributions.** This paper revisits the six fragments listed in Table 1. Our starting point is that completeness is already established in the literature for these fragments, and our aim is not to re-prove fragment-specific normal-form theorems. Instead, we reduce the number of relations while preserving the same strict unitary semantics, and we then study the independence of the resulting axioms.

1. **Smaller finite presentations with unchanged semantics.** For each fragment we give in Section 2 a finite presentation with fewer non-structural axioms than the standard presentations, while preserving completeness for the strict unitary semantics defined in Section 3. Since the source presentations are already complete, completeness is treated as an invariant that our reductions must preserve, rather than as a new theorem about the semantics itself. We do so in Section 4.

2. **Independence and minimality.** In Section 5, we then analyse the resulting axiom sets and prove axiom independence where possible, establishing minimality of our presentations. Concretely, our presentations for qubit Clifford, real Clifford, and CNOT-dihedral are minimal (irredundant) in all arities; our Clifford+T presentation is minimal up to one qubit; our Clifford+CS presentation is minimal up to two qubits; and our qutrit Clifford presentation is minimal up to two qutrits. The independence arguments are uniform: for each axiom we exhibit a separating model [5], i.e. a strict symmetric monoidal interpretation into a small target PROP that satisfies all the other axioms but distinguishes the two sides of the chosen axiom.
<table><caption>Table 2 summarises the resulting axiom counts against previous presentations.</caption><thead><tr><th>Fragment</th><th>Previous Presentation</th><th>Our Presentation</th><th>Figure</th></tr></thead><tbody><tr><td>Qubit Clifford on <i>n</i> qubits</td><td>15 rules [19]</td><td>8 rules (minimal for <i>n</i> qubits)</td><td>2</td></tr><tr><td>Real Clifford on <i>n</i> qubits</td><td>16 rules [17]</td><td>10 rules (minimal for <i>n</i> qubits)</td><td>3</td></tr><tr><td>Qutrit Clifford on <i>n</i> qutrits</td><td>18 rules [15]</td><td>10 rules (minimal for 2 qutrits, conjectured for <i>n</i>)</td><td>4</td></tr><tr><td>Clifford+T on 2 qubits</td><td>18 rules [3]</td><td>11 rules (minimal for 1 qubit, simplified for 2)</td><td>5</td></tr><tr><td>Clifford+CS on 3 qubits</td><td>17 rules [4]</td><td>14 rules (minimal for 2 qubits, simplified for 3)</td><td>6</td></tr><tr><td>CNOT-dihedral on <i>n</i> qubits</td><td>13 rules [1]</td><td>11 rules (minimal for <i>n</i> qubits)</td><td>7</td></tr></tbody></table>

Table 2 Comparison of rule counts: previous work vs. our presentations. Several previous presentations work in a PRO setting where wire permutations are implicit. In our PROP setting these symmetries are structural and not counted as axioms, so raw rule counts are not strictly comparable.

## 2 Graphical languages for quantum circuits

This section fixes the categorical syntax and the proof notion used throughout the paper. Circuits are formalised as morphisms in strict symmetric monoidal categories whose objects are wire counts. A circuit fragment is specified by a gate signature together with a set of equations, yielding a presented PROP. Completeness will be formulated as faithfulness of an interpretation functor into a semantic PROP.

### 2.1 Graphical languages

We work with the one-object-per-wire formalisms PROs and PROPs in the sense of Joyal-Street [11, 18]. We adopt strictness throughout: associativity and unit constraints are treated as literal equalities, so parentheses can be omitted.

**Definition 1.** A PRO is a strict monoidal category $\mathbf{P}$ whose objects are the natural numbers $n \in \mathbb{N}$ and whose tensor on objects is addition $n \otimes m := n + m$ with unit 0. We write $\mathbf{P}(n, m)$ for morphisms $n \to m$, with sequential composition $\circ$ and parallel composition $\otimes$, subject to the usual strict monoidal axioms (Figures 1a–1e).

We write $f: n \to m$ when $f \in \mathbf{P}(n, m)$; $n$ and $m$ are the numbers of input and output wires of $f$. In particular $\mathrm{id}_n = \mathrm{id}_1^n$ for all $n \in \mathbb{N}$.

**Definition 2.** A PROP is a PRO $\mathbf{P}$ equipped with a symmetric monoidal structure, i.e. symmetry isomorphisms $\sigma_{n,m}: n+m \to m+n$ ($n,m \in \mathbb{N}$) generated by the basic swap $\sigma := \sigma_{1,1}$ and satisfying the axioms (1f)-(1g) in Figure 1. We write $\sigma_n := \sigma_{n,1}: n+1 \to 1+n$ for swapping one wire with a block of $n$ wires.

Thus in a PROP, swaps and permutations are part of the ambient structure. PROPs admit a convenient string-diagram representation: a morphism $f: n \to m$ is drawn as a box with $n$ incoming wires and $m$ outgoing wires. Sequential composition is drawn by stacking boxes, tensor by placing them side by side, and $\sigma_{n,m}$ by crossing a block of $n$ wires with a block of $m$ wires. With these conventions, the coherence axioms are exactly the diagrammatic moves that make deformation sound.
XX:4 Simpler Presentations for Many Fragments of Quantum Circuits

<figure><img src="image_3.png" /></figure>

From now on, equalities obtained solely by these coherence moves (including permutations)
are treated as *structural* and used implicitly in diagrammatic arguments.

<figure><img src="image_4.png" /></figure>

$$
(a) f \circ id_n = f = id_n \circ f
$$

<figure><img src="image_5.png" /></figure>

$$
(b) h \circ (g \circ f) = (h \circ g) \circ f
$$

<figure><img src="image_6.png" /></figure>

$$
(c) (f \otimes g) \otimes h = f \otimes (g \otimes h)
$$

<figure><img src="image_7.png" /></figure>

$$
(d) (g_1 \circ f_1) \otimes (g_2 \circ f_2) = (g_1 \otimes g_2) \circ (f_1 \otimes f_2)
$$

<figure><img src="image_8.png" /></figure>

$$
(e) f \otimes id_0 = f = id_0 \otimes f
$$

<figure><img src="image_9.png" /></figure>

$$
(f) \sigma \circ \sigma = id_2
$$

<figure><img src="image_10.png" /></figure>

$$
(g) \sigma_{|f|} \circ (f \otimes id_1) = (id_1 \otimes f) \circ \sigma_{|f|}
$$

Figure 1 Figures 1a–1e are the coherence laws for PROs and Figures 1f and 1g are the additional coherence laws for PROPs.

2.2 Free PROPs and presentations

Circuit fragments are specified by *generators and relations*. Generators represent primitive
gates (with fixed arity), and relations represent the rewrite rules (axioms) available for
equational reasoning.

► **Definition 3.** A (PROP) signature is a set Σ equipped with arity functions dom, cod :
Σ → N. An element g ∈ Σ is written as a generating morphism g : dom(g) → cod(g).

► **Definition 4.** Let $\Sigma$ be a signature. The free PROP on $\Sigma$, written $P_\Sigma$, is the PROP whose morphisms are string diagrams generated from:

■ the non-structural generators $g \in \Sigma$ (with their prescribed arities), and

■ the structural morphisms of a PROP (identities and symmetries),
quotiented by PROP coherence (i.e. the axioms of Figure 1).

Equations between diagrams are imposed by quotienting $\mathbf{P}_{\Sigma}$ by a congruence.

► **Definition 5.** Let $\Sigma$ be a signature and let $\mathcal{R}$ be a set of well-typed equations $L = R$ between morphisms of the free PROP $\mathbf{P}_{\Sigma}$. The presented PROP $\mathbf{P}_{\Sigma}/\mathcal{R}$ is the quotient of $\mathbf{P}_{\Sigma}$ by the smallest congruence that contains $\mathcal{R}$ and is closed under $\circ$, $\otimes$, and symmetry.

This quotient is the formal object that we treat as our *graphical language*: diagrams are equal exactly when their equality is derivable from the coherence axioms together with the chosen relations.
## 2.3 Monoidal functors and completeness

To connect a presented syntax to its intended meaning, we interpret generators as concrete operations and extend compositionally. Completeness will assert that the chosen relations capture exactly the equalities that hold in the intended semantics.

**Definition 6.** A PROP morphism is a strict symmetric monoidal functor $F : \mathbf{P}_1 \to \mathbf{P}_2$ between PROPs that is the identity on objects. Equivalently, $F$ preserves identities, symmetries, sequential composition and tensor.

**Definition 7.** Let $\mathbf{P}$ be a PROP. A subPROP of $\mathbf{P}$ is a wide strict symmetric monoidal subcategory $\mathcal{Q} \subseteq \mathbf{P}$. Concretely, since the objects of a PROP are fixed to be $\mathbb{N}$, this amounts to specifying subsets $\mathcal{Q}(n, m) \subseteq \mathbf{P}(n, m)$ $(n, m \in \mathbb{N})$ such that $\mathrm{id}_n \in \mathcal{Q}(n, n)$ for all $n$; $\sigma_{n,m} \in \mathcal{Q}(n+m, m+n)$ for all $n, m$; and $\mathcal{Q}$ is closed under $\circ$ and $\otimes$.

In this situation, the inclusion functor $\mathcal{Q} \to \mathbf{P}$ is a faithful PROP morphism.

**Definition 8.** Let $\mathbf{P}_{\Sigma}/\mathcal{R}$ be a presented PROP and let $\mathbf{C}$ be a symmetric monoidal category. An interpretation functor is a strict symmetric monoidal functor $[\cdot] : \mathbf{P}_{\Sigma} \to \mathbf{C}$ specified on generators $g \in \Sigma$ and extended monoidally to all diagrams.

If every equation in $\mathcal{R}$ holds in $\mathbf{C}$, then $[\cdot]$ factors uniquely through the quotient, yielding a functor $[\cdot] : \mathbf{P}_{\Sigma}/\mathcal{R} \to \mathbf{C}$.

**Definition 9.** Let $[\cdot] : \mathbf{P}_{\Sigma}/\mathcal{R} \to \mathbf{C}$ be such an interpretation. We say that the graphical language $\mathbf{P}_{\Sigma}/\mathcal{R}$ is complete for this semantics if, for all circuits $C_1, C_2$, $[C_1] = [C_2]$ implies $\mathbf{P}_{\Sigma}/\mathcal{R} \vdash C_1 = C_2$. Equivalently, the interpretation functor is faithful.

We will also use a bounded variant. Given $k \in \mathbb{N}$, we say that $\mathbf{P}_{\Sigma}/\mathcal{R}$ is complete up to $k$ wires if the implication holds whenever $C_1, C_2 : n \to m$ with $n, m \le k$. Equivalently, the interpretation functor is faithful on each hom-set $\mathbf{P}_{\Sigma}/\mathcal{R}(n, m)$ for $n, m \le k$.

Operationally, completeness says that semantic equality can always be witnessed by an explicit diagrammatic derivation from the chosen relations; the bounded form restricts this requirement to circuits of limited arity.

When $\mathbf{C}$ is (by definition) the symmetric monoidal subcategory of some ambient category generated by the images of the generators, the interpretation functor is also full; in that case $\mathbf{P}_{\Sigma}/\mathcal{R}$ is actually isomorphic to the semantic subPROP $\mathbf{C}$.

**Remark 10.** Several completeness results in the literature are stated for PROs. Since we work in PROPs, we record a uniform lifting principle.

Let $\mathbf{P}/\mathcal{R}$ be a complete presented PRO with an interpretation into a *symmetric* monoidal category $\mathbf{C}$. Assume there exists a PRO circuit $\tau : 2 \to 2$ such that $[\tau]$ is the symmetry $\sigma_{1,1}$ of $\mathbf{C}$. Form the free PROP on the same generators, and quotient it by $\mathcal{R}$ together with the single equation $\sigma_{1,1} = \tau$. Define a translation $T$ from PROP diagrams to PRO diagrams by recursively replacing each occurrence of the structural swap $\sigma_{1,1}$ by $\tau$ (leaving all generators unchanged). Then $[D] = [T(D)]$ for every PROP diagram $D$, and any semantic equality between PROP diagrams reduces to a semantic equality between their PRO translations. If the original PRO presentation is complete for $[\cdot]$, then the resulting PROP presentation is complete for the same semantics.

# 3 Quantum circuits and their relations

This section fixes the concrete circuit syntax and the strict unitary semantics used throughout the paper. For qubits, we introduce a single *master signature* containing all gates needed
XX:6 Simpler Presentations for Many Fragments of Quantum Circuits

across the qubit fragments; each fragment will then be obtained by restriction to a sub-
signature and by quotienting by a fragment-specific finite rule set. For qutrits, only the
Clifford fragment is considered, so we present it directly.

► **Definition 11.** The qubit master signature $\Sigma^{(2)}$ consists of the following non-structural generators:

$$
\langle \omega \rangle, \ominus : 0 \to 0, \quad \boxed{\text{H}}, \boxed{\text{Z}}, \boxed{\text{S}}, \boxed{\text{T}}, \boxed{\text{X}} : 1 \to 1, \quad \text{---} \xrightarrow{\bullet} \text{---} : 2 \to 2.
$$

We write $\mathbf{P}^{(2)} := \mathbf{P}_{\Sigma^{(2)}}$ for the free PROP on $\Sigma^{(2)}$. Structural morphisms $\mathrm{id}_n$ and $\sigma_{n,m}$ come from the ambient PROP structure.

Note that every generator $g \in \Sigma^{(2)}$ satisfies $\mathrm{dom}(g) = \mathrm{cod}(g)$. Hence every well-typed diagram in $\mathbf{P}^{(2)}$ has type $n \to n$ for some $n$, and equational derivations never change the wire count. We exploit this arity preservation in Section 5.

Let **FdHilb** be the symmetric monoidal category of finite-dimensional complex Hilbert spaces and linear maps, with tensor product $\otimes$, tensor unit $\mathbb{C}$, and symmetry given by swapping tensor factors. By Mac Lane's coherence theorem [16] we may regard **FdHilb** as strict monoidal.

**Definition 12.** Let $H, K$ be finite-dimensional Hilbert spaces. A linear map $U : H \to K$ is unitary if $U^\dagger U = \mathrm{id}_H$ and $UU^\dagger = \mathrm{id}_K$, where $U^\dagger$ denotes the Hilbert adjoint of $U$. We write $U(H, K)$ for the set of unitary maps $H \to K$, and $U(H) := U(H, H)$.

**Definition 13.** Define **Qubit** to be the PROP with objects $\mathbb{N}$ and hom-sets **Qubit**(n, m) := U((( $\mathbb{C}^2$ ) $\otimes^n$, ( $\mathbb{C}^2$ ) $\otimes^m$) (n, m ∈ $\mathbb{N}$), with composition, identities, tensor, and symmetry inherited from **FdHilb** (viewed as strict monoidal). Define **Qutrit** similarly, replacing $\mathbb{C}^2$ by $\mathbb{C}^3$.

We use the standard Dirac notation for computational basis states: for $x \in \{0,1\}$ we write $|x\rangle \in \mathbb{C}^2$, and for $x, y \in \{0,1\}$ we abbreviate $|x, y\rangle := |x\rangle \otimes |y\rangle$ (similarly, $|x_1, \dots, x_n\rangle := |x_1\rangle \otimes \dots \otimes |x_n\rangle$).

Both **Qubit** and **Qutrit** are endomorphism-only: there are no unitaries $n \to m$ for $n \neq m$.

By the universal property of the free PROP, there is a unique strict symmetric monoidal
functor $[\cdot]^{(2)} : \mathbf{P}^{(2)} \to \mathbf{Qubit}$ sending:

$$
\begin{align*}
\llbracket \omega \rrbracket^{(2)} : 1 &\mapsto e^{i\pi/4} & \llbracket \boxed{\text{H}} \rrbracket^{(2)} : |x\rangle &\mapsto \frac{1}{\sqrt{2}} \sum_{k=0}^{1} (-1)^{xk} |k\rangle \\
\llbracket \circ \rrbracket^{(2)} : 1 &\mapsto -1 & \llbracket \boxed{\text{S}} \rrbracket^{(2)} : |x\rangle &\mapsto i^x |x\rangle \\
\llbracket \boxed{\text{X}} \rrbracket^{(2)} : |x\rangle &\mapsto |1-x\rangle & \llbracket \boxed{\text{Z}} \rrbracket^{(2)} : |x\rangle &\mapsto (-1)^x |x\rangle \\
\llbracket \text{---} \boxplus \text{---} \rrbracket^{(2)} : |x, y\rangle &\mapsto |x, x \oplus y\rangle & \llbracket \boxed{\text{T}} \rrbracket^{(2)} : |x\rangle &\mapsto e^{i\pi x/4} |x\rangle \\
\llbracket \text{---} \boxplus \text{---} \rrbracket^{(2)} : |x, y\rangle &\mapsto i^{xy} |x, y\rangle
\end{align*}
$$

for $x, y \in \{0, 1\}$ and addition $\oplus$ modulo 2.

**3.1 Qubit circuit fragments as presented subPROPs**

Each qubit fragment in this paper is specified by a sub-signature of $\Sigma^{(2)}$ and by a finite
rule set. Syntactically, this yields a quotient of a free PROP; semantically, it yields the
corresponding subPROP of **Qubit** generated by the chosen gates.

Throughout the rest of this subsection, the placeholder • ranges over the five qubit fragments considered here: • ∈ {Cliff, RCliff, CliffT, CliffCS, CNOTdihe}.
**► Definition 14.** For any set $G$ of morphisms in $\mathbf{P}$, we write $\langle G \rangle \subseteq \mathbf{P}$ for the smallest subPROP containing all structural morphisms and all elements of $G$.

**► Definition 15.** Fix a sub-signature $\Sigma_\bullet \subseteq \Sigma^{(2)}$. Let $\mathbf{P}_\bullet := \mathbf{P}_{\Sigma_\bullet}$ be the free PROP on $\Sigma_\bullet$, and identify it with its canonical image in $\mathbf{P}^{(2)}$. A rule set for the fragment $\bullet$ is a finite set $C_\bullet$ of well-typed equations between morphisms of $\mathbf{P}_\bullet$. We write $\mathbf{QCirc}_\bullet := \mathbf{P}_\bullet/C_\bullet$ for the presented PROP obtained by quotienting by the congruence generated by $C_\bullet$.

Thus $\mathbf{QCirc}_\bullet$ is the syntax of the fragment: morphisms are circuits built from $\Sigma_\bullet$, quotiented by the chosen equations $C_\bullet$ (with PROP structure and symmetries treated as structural).

For each fragment $\bullet$ we first fix its intended unitary semantics as the subPROP $\mathbf{Qubit}_\bullet := \langle \llbracket g \rrbracket^{(2)} \mid g \in \Sigma_\bullet \rangle \subseteq \mathbf{Qubit}$, generated by the interpretations of the gates in $\Sigma_\bullet$; equivalently, this is the intended semantic category of the fragment. Since the master interpretation $\llbracket \cdot \rrbracket^{(2)}$ restricts to $\mathbf{P}_\bullet$ and lands in $\mathbf{Qubit}_\bullet$, and since every equation of $C_\bullet$ holds semantically, it factors uniquely through the quotient to a well-defined strict symmetric monoidal functor $\llbracket \cdot \rrbracket_\bullet : \mathbf{QCirc}_\bullet \to \mathbf{Qubit}_\bullet$.

When $\llbracket \cdot \rrbracket_\bullet$ is faithful we say that the presentation $\mathbf{QCirc}_\bullet$ is complete for the corresponding fragment (in the sense of Definition 9).

We now instantiate this scheme for each qubit fragment.

**► Definition 16.** The five qubit fragments treated in this paper are specified by the following sub-signatures and rule sets:

<table><thead><tr><th>Fragment</th><th>Σ<sub>•</sub> ⊆ Σ<sup>(2)</sup></th><th>Rule set C<sub>•</sub></th></tr></thead><tbody><tr><td>Clifford</td><td>Σ<sub>Cliff</sub> := {⟨ω<sub>8</sub⟩, [H], [S], [⊕<sub>2</sub>]}<br>C<sub>Cliff</sub> := Cliff<sub>2</sub> (Figure 2)</td></tr><tr><td>Real Clifford</td><td>Σ<sub>RCliff</sub> := {⟨○⟩, [H], [Z], [⊕<sub>2</sub>]}<br>C<sub>RCliff</sub> := RCliff<sub>2</sub> (Figure 3)</td></tr><tr><td>Clifford+T</td><td>Σ<sub>CliffT</sub> := {⟨ω<sub>8</sub⟩, [H], [T], [⊕<sub>2</sub>]}<br>C<sub>CliffT</sub> := CliffT<sub>2</sub> (Figure 5)</td></tr><tr><td>Clifford+CS</td><td>Σ<sub>CliffCS</sub> := {⟨ω<sub>8</sub⟩, [H], [S], [⊕<sub>2</sub>]}<br>C<sub>CliffCS</sub> := CliffCS<sub>2</sub> (Figure 6)</td></tr><tr><td>CNOT-dihedral</td><td>Σ<sub>CNOTdihe</sub> := {⟨ω<sub>8</sub⟩, [X], [T], [⊕<sub>2</sub>]}<br>C<sub>CNOTdihe</sub> := CNOTdihe<sub>2</sub> (Figure 7)</td></tr></tbody></table>

These data determine the five presented PROPs $\mathbf{QCirc}_\bullet$ (cf. Definition 15). For each fragment $\bullet$, restricting the fixed interpretation $\llbracket \cdot \rrbracket^{(2)}$ yields the PROP morphism $\llbracket \cdot \rrbracket_\bullet : \mathbf{QCirc}_\bullet \to \mathbf{Qubit}_\bullet$ defined above.

## 3.2 The qutrit Clifford fragment

For qutrits, we only consider the Clifford fragment. We therefore present it directly, without introducing a separate “qutrit master signature”. We use the computational basis $\{|0\rangle, |1\rangle, |2\rangle\}$ of $\mathbb{C}^3$ (and the induced tensor-product basis of $(\mathbb{C}^3)^{\otimes n}$).

**► Definition 17.** The qutrit Clifford fragment is generated by the signature

$$ \Sigma_{Cliff3} := \{\omega_{12} : 0 \to 0, [H], [S] : 1 \to 1, \oplus : 2 \to 2\}. $$

Let $\mathbf{P}_{Cliff3} := \mathbf{P}_{\Sigma_{Cliff3}}$ be the free PROP on $\Sigma_{Cliff3}$. Let $C_{Cliff3} := \text{Cliff}_3$ be the rule set given in Figure 4. We then define $\mathbf{QCirc}_{Cliff3} := \mathbf{P}_{Cliff3}/C_{Cliff3}$.

By the universal property of the free PROP, there is a unique strict symmetric monoidal functor $\llbracket \cdot \rrbracket_{Cliff3} : \mathbf{QCirc}_{Cliff3} \to \mathbf{Qutrit}_{Cliff3}$ determined by

$$ \begin{align*} \llbracket \omega_{12} \rrbracket_{Cliff3} : 1 &\mapsto e^{i\pi/6} & \llbracket [H] \rrbracket_{Cliff3} : |x\rangle &\mapsto \frac{1}{\sqrt{3}} \sum_{k=0}^{2} e^{2\pi i x k / 3} |k\rangle \\ \llbracket \oplus \rrbracket_{Cliff3} : |x, y\rangle &\mapsto |x, (x+y) \mod 3\rangle & \llbracket [S] \rrbracket_{Cliff3} : |x\rangle &\mapsto e^{i\pi x(x-1)/3} |x\rangle \end{align*} $$
## XX:8 Simpler Presentations for Many Fragments of Quantum Circuits

for $x, y \in \{0, 1, 2\}$. Here $\mathbf{Qutrit}_{Cliff^3} := \langle [[g]]_{Cliff^3} | g \in \Sigma_{Cliff^3} \rangle$ is the semantic subPROP generated by the qutrit Clifford gates.

<figure><img src="image_11.png" /><figcaption>Figure 2 Set of relations $Cliff_2$.</figcaption></figure>

<figure><img src="image_12.png" /><figcaption>Figure 3 Set of relations $RCliff_2$.</figcaption></figure>

## 4 Completeness: from PROs to PROPs

For each fragment • introduced in Section 3 we have a presented PROP QCirc. = P./C. and a strict symmetric monoidal interpretation functor [[•]]• : QCirc. → Qubit. (or Qutrit$_{Cliff^3}$ in the qutrit case). Completeness means faithfulness of [[•]]• in the sense of Definition 9.

Complete equational theories for the same fragments are already available in the literature [19, 17, 15, 3, 4, 1]. The purpose of this section is to explain how completeness of our presentations QCirc. is derived from those results without re-proving fragment-specific normal-form theorems. The argument is uniform across the six fragments: for each fragment we relate our syntax to a known complete source syntax by explicit translations and then transfer faithfulness.

Since we work in PROPs, whenever a source theorem is formulated in a PRO setting we implicitly replace it by its PROP lift obtained by making the symmetry structural, using the lifting principle of Remark 10. From this point on, all syntactic categories considered in this section are PROPs and all translations are PROP morphisms in the sense of Definition 6; in particular they are strict symmetric monoidal and are the identity on objects.
<figure><img src="image_13.png" /><figcaption>Figure 7 Set of relations CNOTdihe₂, where the non-generator gates are defined in Figure 9.</figcaption></figure>

**Definition 18.** A pair of PROP morphisms $E : \mathbf{P} \to \mathbf{P}^{\text{src}}$, $D : \mathbf{P}^{\text{src}} \to \mathbf{P}$ is an encoding/decoding pair if, for all circuits $C \in \mathbf{P}$ and $C' \in \mathbf{P}^{\text{src}}$, $[[C]] = [[E(C)]]_{\text{src}}$ and $[[C')]_{\text{src}} = [[D(C')]]$.

The next two lemmas provide a finite checklist for proving that translations can be used to transport derivations. The first lemma shows that it suffices to check $D \circ E = \text{id}$ on generators.

**Lemma 19.** Assume $\mathbf{P}$ is presented by generators $\Sigma$ and relations $\mathcal{R}$. If for every non-structural generator $g \in \Sigma$, $\mathbf{P}/\mathcal{R} \vdash D(E(g)) = g$, then for every circuit $C$ built from $\Sigma$, $\mathbf{P}/\mathcal{R} \vdash D(E(C)) = C$.

**Proof.** By structural induction on $C$, using that $E$ and $D$ preserve $\circ$ and $\otimes$ and fix all structural morphisms. ◀

The second lemma ensures that decoding is compatible with the source congruence, so that any derivation in the source theory can be transported into the target theory.

**Lemma 20.** Assume that for every axiom $L = R$ in $\mathcal{R}^{\text{src}}$, $\mathbf{P}/\mathcal{R} \vdash D(L) = D(R)$. Then $D$ induces a PROP morphism $\bar{D} : \mathbf{P}^{\text{src}}/\mathcal{R}^{\text{src}} \to \mathbf{P}/\mathcal{R}$, and for all circuits $C_1, C_2 \in \mathbf{P}^{\text{src}}$, $\mathbf{P}^{\text{src}}/\mathcal{R}^{\text{src}} \vdash C_1 = C_2 \implies \mathbf{P}/\mathcal{R} \vdash D(C_1) = D(C_2)$.

**Proof.** The hypothesis states that $D$ equalises all relations in $\mathcal{R}^{\text{src}}$, hence $D$ factors through the quotient. ◀

**Remark 21.** In applications, $E$ and $D$ are specified on generators and extended uniquely to PROP morphisms by the universal property of free PROPs. The hypotheses of Lemmas 19 and 20 then reduce to a finite list of equalities: one equation for each target generator and one equation for each source axiom.

**Theorem 22.** Assume $\mathbf{P}^{\text{src}}/\mathcal{R}^{\text{src}}$ is complete for $[[\cdot]]_{\text{src}}$. Suppose there exists an encoding/decoding pair $(E, D)$ in the sense of Definition 18 satisfying the hypotheses of Lemmas 19 and 20. Then $\mathbf{P}/\mathcal{R}$ is complete for $[[\cdot]]$.
XX:12 Simpler Presentations for Many Fragments of Quantum Circuits

**Proof.** Let $C_1, C_2 \in \mathbf{P}$ be circuits of the same type with $[[C_1]] = [[C_2]]$. By Definition 18, $[[E(C_1)]]_{\text{src}} = [[E(C_2)]]_{\text{src}}$. Since the source presentation is complete, this implies $\mathbf{P}^{\text{src}}/\mathcal{R}^{\text{src}} \vdash E(C_1) = E(C_2)$. Applying $\bar{D}$ from Lemma 20 yields $\mathbf{P}/\mathcal{R} \vdash D(E(C_1)) = D(E(C_2))$. Finally, Lemma 19 rewrites both sides to obtain $\mathbf{P}/\mathcal{R} \vdash C_1 = C_2$. ◀

## 4.3 Fragment-wise completeness

For each fragment, the appendices provide: a source presentation from the literature, explicit definitions of $E$ and $D$ on generators, and the verification of the checklists in Lemmas 19 and 20. The source presentations are recalled in Figures 12–17. The encoding/decoding functors are specified on generators in Table 3. The generator equalities required for Lemma 19 and the axiom checks required for Lemma 20 are proved in Appendices F and G.

For qutrit Clifford and Clifford+CS we first apply the scalar refinements described in Section 4.1 so that source and target are interpreted in the same semantic subPROP. We then instantiate Theorem 22 with the encoding/decoding pairs of Table 3.

► **Theorem 23.** 1. The graphical language $\mathbf{QCirc}_{Cliff}$ is complete for $\mathbf{Qubit}_{Cliff}$.

2. The graphical language $\mathbf{QCirc}_{RCliff}$ is complete for $\mathbf{Qubit}_{RCliff}$.

3. The graphical language $\mathbf{QCirc}_{CliffT}$ is complete up to 2 qubits for $\mathbf{Qubit}_{CliffT}$.

4. The graphical language $\mathbf{QCirc}_{Cliff3}$ is complete for $\mathbf{Qutrit}_{Cliff3}$.

5. The graphical language $\mathbf{QCirc}_{CliffCS}$ is complete up to 3 qubits for $\mathbf{Qubit}_{CliffCS}$.

For the CNOT-dihedral fragment, the known complete equational theory is already formulated as a PROP with the same scalar generator as in our master signature [1]. Thus no scalar refinement or encoding/decoding step is required. Completeness of our smaller axiom set is obtained by showing that the axioms omitted from [1] are derivable from CNOTdihe₂; this derivability is proved in Appendix H.

► **Theorem 24.** The graphical language $\mathbf{QCirc}_{CNOTdihe}$ is complete for $\mathbf{Qubit}_{CNOTdihe}$.

# 5 Minimality

Completeness of a rule set $C_•$ means that every semantic equality between circuits of the fragment can be derived using $C_•$ together with the structural equalities of PROPs. In this section we study the complementary question of non-redundancy: whether the axioms of $C_•$ are all necessary for completeness.

Throughout, fix a fragment $•$ with free PROP $\mathbf{P}•$ and finite rule set $C_•$. All non-structural generators are endomorphisms, hence every well-typed circuit has type $n \to n$, and equational derivations preserve the wire count.

## 5.1 Independence and minimality

For an axiom $\rho$ in $C_•$ we write $C_• \setminus \{\rho\}$ for the remaining axioms, and we let $\mathbf{QCirc}_•^{-\rho} := \mathbf{P}•/(C_• \setminus \{\rho\})$ denote the presented PROP obtained by removing $\rho$ and closing under congruence (Definition 5).

► **Definition 25.** Let $\rho$ be an axiom $C_1 = C_2$ in $C_•$ (with $C_1, C_2 : n \to n$). We say that $\rho$ is independent of the other axioms of the same fragment if $\mathbf{QCirc}_•^{-\rho} \nvdash C_1 = C_2$. We say that $C_•$ is minimal if every $\rho \in C_•$ is independent.
**Remark 26.** Assume $C_{\bullet}$ is sound for an intended semantics $[\cdot]_{\bullet}$. Then an axiom $\rho \in C_{\bullet}$ is necessary for completeness (removing it destroys faithfulness of $[\cdot]_{\bullet}$) if and only if it is independent in the sense of Definition 25. Indeed, if $\rho$ were derivable from $C_{\bullet} \setminus \{\rho\}$ then removing $\rho$ would not change the induced congruence; conversely, if $C_{\bullet} \setminus \{\rho\}$ were still complete, then the semantic validity of $\rho$ would force $\rho$ to be derivable.

Since derivations preserve arity, it is natural to state bounded minimality results by truncating to a fixed number of wires.

**Definition 27.** Let $k \in \mathbb{N}$. Define $C_{\bullet, \le k} := \{\rho \in C_{\bullet} \mid \rho \text{ has type } n \to n \text{ with } n \le k\}$. We say that $C_{\bullet}$ is minimal up to $k$ wires if every $\rho \in C_{\bullet, \le k}$ is independent relative to $C_{\bullet, \le k}$ (i.e. independent in the sense of Definition 25 after replacing $C_{\bullet}$ by $C_{\bullet, \le k}$).

**Remark 28.** Let $n \in \mathbb{N}$. Any equation derivable in the hom-set $P_{\bullet}(n, n)$ uses only axioms of type $m \to m$ with $m \le n$. This follows because both $\circ$ and $\otimes$ preserve the wire count and every generator is an endomorphism. Thus, to prove independence of a relation $\rho : n \to n$, it suffices to work in the truncated system $C_{\bullet, \le n}$.

## 5.2 Separation by alternative interpretations

Our independence proofs are semantic: to show that an axiom $\rho$ is not derivable from the others, we construct a strict symmetric monoidal interpretation into a small target PROP that validates all axioms except $\rho$.

**Lemma 29.** Let $\rho : C_1 = C_2$ be an axiom in $C_{\bullet}$. Assume there exist a PROP $P_{\text{alt}}$ and a PROP morphism $F : P_{\bullet} \to P_{\text{alt}}$ such that $\forall (L = R) \in (C_{\bullet} \setminus \{\rho\})$, $F(L) = F(R)$, but $F(C_1) \neq F(C_2)$. Then $\rho$ is independent.

**Proof.** Since $F$ equalises every axiom in $C_{\bullet} \setminus \{\rho\}$, it factors through the quotient $\mathcal{Q}\text{Circ}_{\bullet}^{-\rho}$, yielding a PROP morphism $\bar{F} : \mathcal{Q}\text{Circ}_{\bullet}^{-\rho} \to P_{\text{alt}}$. If $\mathcal{Q}\text{Circ}_{\bullet}^{-\rho} \vdash C_1 = C_2$ then applying $\bar{F}$ gives $F(C_1) = F(C_2)$, a contradiction. ◀

**Remark 30.** All morphisms of $P_{\bullet}$ are already quotiented by PROP coherence (Definition 4). Thus, once $F$ is a PROP morphism, it automatically respects all structural equalities. In practice, to apply Lemma 29 it suffices to check the non-structural axioms of the fragment.

## 5.3 Families of separating interpretations

We now define the basic target PROPs and interpretation schemes used throughout the independence arguments collected in Figure 8. In figures, some gates may be displayed using syntactic abbreviations; these abbreviations stand for fixed morphisms of the free PROP, and every separating interpretation is applied to the expanded morphisms.

**Definition 31.** Let $(M, \oplus, 0)$ be a commutative monoid and let $\epsilon \in M$ satisfy $\epsilon \oplus \epsilon = 0$. Define $\text{End}_{\epsilon}(M)$ to be the PROP with objects $\mathbb{N}$ and hom-sets $\text{End}_{\epsilon}(M)(n, n) := M(n \in \mathbb{N})$, $\text{End}_{\epsilon}(M)(n, m) := \emptyset$ ($n \neq m$). Composition and tensor are given by $\oplus$, identities by 0, and the symmetry is defined by $\sigma_{1,1} := \epsilon \in M$.

**Remark 32.** The condition $\epsilon \oplus \epsilon = 0$ implies $\sigma_{m,n} \circ \sigma_{n,m} = \text{id}_{n+m}$. All other PROP coherence axioms hold because every structural map is interpreted as an element of the commutative monoid $M$ and both $\circ$ and $\otimes$ are interpreted as $\oplus$.
XX:14 Simpler Presentations for Many Fragments of Quantum Circuits

**Definition 33.** For $k \ge 2$ define **Count**$_k := \text{End}_0(\mathbb{Z}_k, +, 0)$ and **Has := End}_0(\mathbb{B}, \lor, 0)$ with $\mathbb{B} = \{0, 1\}$. When we want to record the parity of the structural swap, we also use **Count**$_2^{\text{swap}} := \text{End}_1(\mathbb{Z}_2, +, 0)$, so that the basic symmetry $\sigma_{1,1}$ is interpreted as $1 \in \mathbb{Z}_2$.

**Definition 34.** Let $k \ge 2$. Given a finite list $(g_1, \dots, g_r)$ of generators in $\Sigma_\bullet$ (not necessarily distinct), define $w : \Sigma_\bullet \to \mathbb{Z}_k$ by $w(g) := |\{i \in \{1, \dots, r\} | g_i = g\}| \bmod k (g \in \Sigma_\bullet)$.

We then write $\#\{g_1, \dots, g_r\}_{[k]} := F_{w,k} : \mathbf{P}_\bullet \to \mathrm{Count}_k$. When $k=2$, we use the symbol $\mathcal{X}$ inside the braces only as a mnemonic that swaps are counted: $\#\{g_1, \dots, g_r, \mathcal{X}\}_{[2]} := F_w^{\mathrm{swap}} : \mathbf{P}_\bullet \to \mathrm{Count}_2^{\mathrm{swap}}$. In particular, $\#\{\mathcal{X}\}_{[2]}$ denotes the functor $\mathbf{P}_\bullet \to \mathrm{Count}_2^{\mathrm{swap}}$ that sends every non-structural generator to 0.

**Definition 35.** Let $g \in \Sigma_\bullet$. By the universal property of the free PROP, there exists a unique PROP morphism $?g : \mathbf{P}_\bullet \to \mathbf{Has}$ such that $?g(g) = 1$ and $?g(h) = 0$ for every generator $h \in \Sigma_\bullet$ with $h \ne g$. Equivalently, for any circuit $C$, one has $?g(C) = 1$ if and only if $g$ occurs at least once in $C$.

Projective interpretations are used to forget global phases while keeping the remaining unitary content.

**Definition 36.** Let $\mathrm{PU}_d$ be the PROP of projective unitaries on $d$-dimensional systems (unitaries modulo global phase), and let $\pi_d$ denote the quotient map from unitaries to their projective classes. For each fragment $\bullet$, define the projective interpretation $J^\bullet_{\text{proj}} := \pi_d \circ [\cdot]_\bullet$, with $d=2$ in the qubit case and $d=3$ in the qutrit case.

Given a generator $g : n \to n$ and a circuit $C : n \to n$, we write $g \mapsto C$ for the PROP morphism $\mathbf{P}_\bullet \to \mathrm{PU}_d$ obtained by sending $g$ to $J^\bullet_{\text{proj}}(C)$ and sending every other generator $h \ne g$ to $J^\bullet_{\text{proj}}(h)$.

The last family of separators records a scaled determinant phase, chosen so as to be strictly monoidal on a bounded number of wires.

**Definition 37.** Fix $k \in \mathbb{N}$ and write $\arg \det(U) \in \mathbb{R}/2\pi\mathbb{Z}$ for the phase of $\det(U)$. Set $\epsilon_k := 2^{k-2}\pi \mod 2\pi$, so $\epsilon_2 = \pi$ and $\epsilon_k = 0$ for $k > 2$.

Define a PROP morphism $\arg \det_k : \mathbf{P}_\bullet \to \text{End}_{\epsilon_k}(\mathbb{R}/2\pi\mathbb{Z}, +, 0)$ on generators $g : n \to n$ by $(\arg \det_k)(g) := 2^{k-n} \cdot \arg \det([g]) \mod 2\pi$, and extend it to all circuits using preservation of $\circ$, $\otimes$, and symmetries.

**Remark 38.** The scaling factor $2^{k-n}$ is chosen so that $\arg \det_k$ is compatible with tensoring on arities $\le k$, using $\det(U \otimes V) = \det(U)^{2^m} \det(V)^{2^n}$ for $U$ on $n$ qubits and $V$ on $m$ qubits. The choice of $\epsilon_k$ ensures that the image of the structural swap $\sigma_{1,1}$ coincides with its determinant phase after scaling: it contributes $\pi$ when $k=2$ and becomes 0 for $k > 2$.

5.4 Minimality statements

**Theorem 39.** The following rule sets are minimal for the indicated fragment-circuits:

1. $\text{Cliff}_2$ is minimal for $\mathbf{P}_{\text{Cliff}}$-circuits (all arities).

2. $\text{RCliff}_2$ is minimal for $\mathbf{P}_{\text{RCliff}}$-circuits (all arities).

3. $\text{Cliff}_3$ is minimal for $\mathbf{P}_{\text{Cliff3}}$-circuits up to 2 qutrit wires. $^1$

4. $\text{CliffT}_2$ is minimal for $\mathbf{P}_{\text{CliffT}}$-circuits up to 1 qubit wire.

5. $\text{CliffCS}_2$ is minimal for $\mathbf{P}_{\text{CliffCS}}$-circuits up to 2 qubit wires.

<footnote n="1">¹ The only missing case is separating the 3-qutrit axiom Equation (I); we conjecture full minimality.</footnote>
6. CNOTdihe₂ is minimal for $\mathbf{P}_{CNOTdihe}$-circuits (all arities).

Moreover:

- In CliffT₂, the 2-qubit axioms (CPh), (B) and (CZ) are independent.

- In CliffCS₂, the 3-qubit axiom (I) is independent.

**Proof.** For each axiom $\rho$ covered by the statement, Figure 8 provides a PROP morphism $F_{\rho}$ that equalises all other axioms of the same or lower arity but distinguishes the two sides of $\rho$. ◀

<table><caption>(a) Clifford</caption><thead><tr><th>Rel.</th><th>Interpretation</th></tr></thead><tbody><tr><td>(ω<sup>8</sup>)</td><td>?ω<sub>8</sub></td></tr><tr><td>(H<sup>2</sup>)</td><td>?-[H]-</td></tr><tr><td>(S<sup>4</sup>)</td><td>?-[S]-</td></tr><tr><td>(E)</td><td>#{-[H]}<sub>[2]</sub></td></tr><tr><td>(CPh)</td><td>? ⊕</td></tr><tr><td>(B)</td><td>#{○<sub>1</sub>}<sub>[2]</sub></td></tr><tr><td>(CZ)</td><td>#{○<sub>2</sub>,○<sub>3</sub>}<sub>[2]</sub></td></tr><tr><td>(I)</td><td>arg det<sub>2</sub></td></tr></tbody></table>

<table><caption>(b) Real Clifford</caption><thead><tr><th>Rel.</th><th>Interpretation</th></tr></thead><tbody><tr><td>(-<sup>2</sup>)</td><td>?-○</td></tr><tr><td>(H<sup>2</sup>)</td><td>?-[H]-</td></tr><tr><td>(Z<sup>2</sup>)</td><td>?-[Z]-</td></tr><tr><td>(F)</td><td>#{ω<sub>8</sub>}<sub>[2]</sub></td></tr><tr><td>(CX<sup>2</sup>)</td><td>? ⊕</td></tr><tr><td>(B)</td><td>#{○<sub>1</sub>}<sub>[2]</sub></td></tr><tr><td>(ZC)</td><td>#{-[Z]}<sub>[2]</sub></td></tr><tr><td>(CF)</td><td>[Z] ↦ —</td></tr><tr><td>(CZr)</td><td>[H] ↦ —</td></tr><tr><td>(I)</td><td>arg det<sub>2</sub></td></tr></tbody></table>

<table><caption>(c) Qutrit Clifford</caption><thead><tr><th>Rel.</th><th>Interpretation</th></tr></thead><tbody><tr><td>(ω<sup>12</sup>)</td><td>?ω<sub>12</sub></td></tr><tr><td>(H<sup>4</sup>)</td><td>?-[H]-</td></tr><tr><td>(S<sup>3</sup>)</td><td>?-[S]-</td></tr><tr><td>(E)</td><td>#{-[H]}<sub>[2]</sub></td></tr><tr><td>(SS')</td><td>[S] ↦ [S]-[X]<sup>a</sup></td></tr><tr><td>(CPh)</td><td>? ⊕</td></tr><tr><td>(B)</td><td>#{○<sub>1</sub>}<sub>[2]</sub></td></tr><tr><td>(CZ)</td><td>#{-[S]}<sub>[3]</sub></td></tr><tr><td>(KC)</td><td>#{○<sub>2</sub>}<sub>[2]</sub></td></tr><tr><td>(I)</td><td>—</td></tr></tbody></table>

<sup>a</sup> See Proposition 40

<table><caption>(d) Clifford+T</caption><thead><tr><th>Rel.</th><th>Interpretation</th></tr></thead><tbody><tr><td>(ω<sup>8</sup>)</td><td>?ω<sub>8</sub></td></tr><tr><td>(H<sup>2</sup>)</td><td>?-[H]-</td></tr><tr><td>(T<sup>8</sup>)</td><td>?-[T]-</td></tr><tr><td>(E)</td><td>#{-[H]}<sub>[2]</sub></td></tr><tr><td>(TX)</td><td>#{-[H],-[T],ω<sub>8</sub>}<sub>[2]</sub></td></tr><tr><td>(CPh)</td><td>? ⊕</td></tr><tr><td>(B)</td><td>#{○<sub>1</sub>}<sub>[2]</sub></td></tr><tr><td>(CZ)</td><td>#{○<sub>2</sub>,○<sub>3</sub>}<sub>[2]</sub></td></tr><tr><td>(CSH)</td><td>—</td></tr><tr><td>(HT<sup>2</sup>)</td><td>—</td></tr><tr><td>(HTH)</td><td>—</td></tr></tbody></table>

<table><caption>(e) Clifford+CS</caption><thead><tr><th>Rel.</th><th>Interpretation</th></tr></thead><tbody><tr><td>(ω<sup>8</sup>)</td><td>?ω<sub>8</sub></td></tr><tr><td>(H<sup>2</sup>)</td><td>?-[H]-</td></tr><tr><td>(S<sup>4</sup>)</td><td>?-[S]-</td></tr><tr><td>(E)</td><td>#{-[H]}<sub>[2]</sub></td></tr><tr><td>(CPh)</td><td>? ⊕</td></tr><tr><td>(B)</td><td>#{○<sub>1</sub>}<sub>[2]</sub></td></tr><tr><td>(XCS)</td><td>#{-[S],-[H]}<sub>[2]</sub></td></tr><tr><td>(CSr)</td><td>[S] ↦ [Z]</td></tr><tr><td>(CE)</td><td>[S] ↦ [Z]</td></tr><tr><td>(I)</td><td>arg det<sub>2</sub></td></tr><tr><td>(SH<sub>k</sub>)</td><td>—</td></tr></tbody></table>

<table><caption>(f) CNOT-dihedral</caption><thead><tr><th>Rel.</th><th>Interpretation</th></tr></thead><tbody><tr><td>(ω<sup>8</sup>)</td><td>?ω<sub>8</sub></td></tr><tr><td>(T<sup>8</sup>)</td><td>?-[T]-</td></tr><tr><td>(X<sup>2</sup>)</td><td>?-[X]-</td></tr><tr><td>(TX)</td><td>#{ω<sub>8</sub>}<sub>[2]</sub></td></tr><tr><td>(XC)</td><td>#{-[X]}<sub>[2]</sub></td></tr><tr><td>(CPh)</td><td>? ⊕</td></tr><tr><td>(B)</td><td>#{○<sub>1</sub>}<sub>[2]</sub></td></tr><tr><td>(ZC)</td><td>#{-[T],ω<sub>8</sub>,ω<sub>8</sub>}<sub>[8]</sub></td></tr><tr><td>(I)</td><td>#{○<sub>2</sub>,○<sub>3</sub>}<sub>[2]</sub></td></tr><tr><td>(C<sup>2</sup>T)</td><td>#{-[T],ω<sub>8</sub>,ω<sub>8</sub>}<sub>[4]</sub></td></tr><tr><td>(C<sup>3</sup>T)</td><td>arg det<sub>3</sub></td></tr></tbody></table>

■ **Figure 8** Separating interpretations used to witness axiom independence. For each relation, the right column gives a strict symmetric monoidal functor into a simple target PROP that equalises all other axioms of the same fragment but distinguishes the two sides of this relation (via Lemma 29). Entries marked ‘—’ are relations for which we provide no separating interpretation.

References

1 Matthew Amy, Jianxin Chen, and Neil J. Ross. A Finite Presentation of CNOT-Dihedral Operators. *Electronic Proceedings in Theoretical Computer Science*, 266:84–97, February 2018. URL: http://dx.doi.org/10.4204/EPTCS.266.5, doi:10.4204/eptcs.266.5.
XX:16 Simpler Presentations for Many Fragments of Quantum Circuits

2 Miriam Backens, Simon Perdrix, and Quanlong Wang. Towards a Minimal Stabilizer ZX-calculus. *Logical Methods in Computer Science*, Volume 16, Issue 4, December 2020. URL: http://dx.doi.org/10.23638/LMCS-16(4:19)2020, doi:10.23638/lmcs-16(4:19)2020.

3 Xiaoning Bian and Peter Selinger. Generators and Relations for 2-Qubit Clifford+T Operators. *Electronic Proceedings in Theoretical Computer Science*, 394:13–28, November 2023. URL: http://dx.doi.org/10.4204/EPTCS.394.2, doi:10.4204/eptcs.394.2.

4 Xiaoning Bian and Peter Selinger. Generators and Relations for 3-Qubit Clifford+CS Operators. *Electronic Proceedings in Theoretical Computer Science*, 384:114–126, August 2023. URL: http://dx.doi.org/10.4204/EPTCS.384.7, doi:10.4204/eptcs.384.7.

5 Garrett Birkhoff. On the Structure of Abstract Algebras. *Mathematical Proceedings of the Cambridge Philosophical Society*, 31(4):433–454, 1935. doi:10.1017/S0305004100013463.

6 Alexandre Clément, Noé Delorme, and Simon Perdrix. Minimal Equational Theories for Quantum Circuits. In *Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science*, LICS '24, New York, NY, USA, 2024. Association for Computing Machinery. doi:10.1145/3661814.3662088.

7 Alexandre Clément, Noé Delorme, Simon Perdrix, and Renaud Vilmart. Quantum Circuit Completeness: Extensions and Simplifications. In Aniello Murano and Alexandra Silva, editors, *32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)*, volume 288 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 20:1–20:23, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/ entities/document/10.4230/LIPIcs.CSL.2024.20, doi:10.4230/LIPIcs.CSL.2024.20.

8 Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Benoît Valiron. A Complete Equational Theory for Quantum Circuits. In *2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, page 1–13. IEEE, June 2023. URL: http:// dx.doi.org/10.1109/LICS56636.2023.10175801, doi:10.1109/lics56636.2023.10175801.

9 Nachum Dershowitz and Jean-Pierre Jouannaud. *Rewrite systems*, page 243–320. MIT Press, Cambridge, MA, USA, 1991.

10 Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for Quantum circuits. *Proceedings of the ACM on Programming Languages*, 5(POPL):1–29, January 2021. URL: http://dx.doi.org/10.1145/3434318, doi:10.1145/3434318.

11 André Joyal and Ross Street. The geometry of tensor calculus, I. *Advances in Mathematics*, 88(1):55–112, 1991. URL: https://www.sciencedirect.com/science/article/pii/ 000187089190003P, doi:10.1016/0001-8708(91)90003-P.

12 Aleks Kissinger and John van de Wetering. PyZX: Large Scale Automated Diagrammatic Reasoning. *Electronic Proceedings in Theoretical Computer Science*, 318:229–241, May 2020. URL: http://dx.doi.org/10.4204/EPTCS.318.14, doi:10.4204/eptcs.318.14.

13 D. E. Knuth and P. B. Bendix. *Simple Word Problems in Universal Algebras*, pages 342–376. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983. doi:10.1007/978-3-642-81955-1_23.

14 Stephen Lack. Composing PROPs. *Theory and Applications of Categories*, 13(9):147–163, 2004.

15 Sarah Meng Li, Michele Mosca, Neil J. Ross, John van de Wetering, and Yuming Zhao. A Complete and Natural Rule Set for Multi-Qutrit Clifford Circuits. *Electronic Proceedings in Theoretical Computer Science*, 426:23–78, August 2025. URL: http://dx.doi.org/10.4204/ EPTCS.426.2, doi:10.4204/eptcs.426.2.

16 Saunders Mac Lane. Categorical Algebra. *Bulletin of the American Mathematical Society*, 71(1):40–106, 1965. doi:10.1090/S0002-9904-1965-11234-4.

17 Justin Makary, Neil J. Ross, and Peter Selinger. Generators and Relations for Real Stabilizer Operators. *Electronic Proceedings in Theoretical Computer Science*, 343:14–36, September 2021. URL: http://dx.doi.org/10.4204/EPTCS.343.2, doi:10.4204/eptcs.343.2.

18 P. Selinger. A Survey of Graphical Languages for Monoidal Categories. In *New Structures for Physics*, page 289–355. Springer Berlin Heidelberg, 2010. URL: http://dx.doi.org/10. 1007/978-3-642-12821-9_4, doi:10.1007/978-3-642-12821-9_4.
19 Peter Selinger. Generators and relations for n-qubit Clifford operators. *Logical Methods in Computer Science*, Volume 11, Issue 2, June 2015. URL: http://dx.doi.org/10.2168/LMCS-11(2:10)2015, doi:10.2168/LMCS-11(2:10)2015.

20 Renaud Vilmart. A Near-Minimal Axiomatisation of ZX-Calculus for Pure Qubit Quantum Mechanics. In *2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–10, 2019. doi:10.1109/LICS.2019.8785765.
XX:18 Simpler Presentations for Many Fragments of Quantum Circuits

<figure><img src="image_14.png" /><figcaption>Figure 9 Summary of Shortcuts used for all considered fragments.</figcaption></figure>

A Auxiliary derivations for Cliff<sub>2</sub>

Derivation A.1.

<figure><img src="image_15.png" /></figure>
Shortcuts for $P_{Cliff}^{source}$-circuits.

$$ (\omega_8^\dagger) := (\omega_8^7) \quad (\omega^\dagger) $$

Shortcuts for $P_{Cliff3}^{source}$-circuits.

<figure><img src="image_16.png" /></figure>

(CNOT)

<figure><img src="image_17.png" /></figure>

(SWAP)

Shortcuts for $P_{CliffT}^{source}$-circuits.

$$ \boxed{S} := \boxed{T^2} \quad (S) $$

$$ \boxed{Z} := \boxed{S^2} \quad (Z) $$

$$ \boxed{X} := \boxed{H} \quad (X) $$

$$ \boxed{T^\dagger} := \boxed{T^6} \quad (S^\dagger) $$

$$ \bigoplus_i \boxed{X} \quad (0CX) $$

$$ \boxed{H} := \boxed{S} \quad \boxed{H} \quad \boxed{T} \quad \bigoplus_i \boxed{T^i} \quad \boxed{H} \quad \boxed{S^\dagger} $$

$$ \boxed{CH} \quad (0CH) $$

Shortcuts for $P_{CliffCS}^{source}$-circuits.

$$ \boxed{Z} := \boxed{S^2} \quad (Z) $$

$$ (\omega_8^\dagger) := (\omega_8^7) \quad (\omega^\dagger) $$

$$ \bigoplus_i \boxed{K} \quad \bigoplus_j \boxed{K} \quad \bigoplus_i \boxed{K} \quad \bigoplus_j \boxed{K} $$

(oldCX)

Common shorthand notations

$$ (\alpha^k) := \alpha \alpha \dots \alpha \quad (\omega^k) \quad \text{k times} $$

$$ \boxed{U^k} := \boxed{U} \quad \boxed{U} \quad \dots \quad \boxed{U} \quad (U^k) \quad \text{k times} $$

<figure><img src="image_18.png" /></figure>

(3)

<figure><img src="image_19.png" /></figure>

(4)

<caption>Figure 10 Summary of Shortcuts used for all considered fragments used in the original PROs.</caption>

## Derivation A.2.

<figure><img src="image_20.png" /></figure>

## Derivation A.3.

<figure><img src="image_21.png" /></figure>

## Derivation A.4.

<figure><img src="image_22.png" /></figure>
Derivation A.5.

<figure><img src="image_23.png" /></figure>

Derivation A.6.

<figure><img src="image_24.png" /></figure>

Derivation A.7.

<figure><img src="image_25.png" /></figure>

Derivation A.8.

<figure><img src="image_26.png" /></figure>

Derivation A.9.

<figure><img src="image_27.png" /></figure>

Derivation A.10.

<figure><img src="image_28.png" /></figure>
Derivation A.11.

<figure><img src="image_29.png" /></figure>

<figure><img src="image_30.png" /></figure>

<figure><img src="image_31.png" /></figure>

<figure><img src="image_32.png" /></figure>

<figure><img src="image_33.png" /></figure>

<figure><img src="image_34.png" /></figure>

<figure><img src="image_35.png" /></figure>

<figure><img src="image_36.png" /></figure>

<figure><img src="image_37.png" /></figure>

Derivation A.12.

<figure><img src="image_38.png" /></figure>

<figure><img src="image_39.png" /></figure>

Derivation A.13.

<figure><img src="image_40.png" /></figure>
Derivation A.14.

<figure><img src="image_41.png" /></figure>

Derivation A.15.

<figure><img src="image_42.png" /></figure>

Derivation A.16.

<figure><img src="image_43.png" /></figure>

Derivation A.17.

<figure><img src="image_44.png" /></figure>

Derivation A.18.

<figure><img src="image_45.png" /></figure>

Derivation A.19.

<figure><img src="image_46.png" /></figure>

Derivation A.20.

<figure><img src="image_47.png" /></figure>
Derivation A.21.

<figure><img src="image_48.png" /></figure>

Derivation A.22.

<figure><img src="image_49.png" /></figure>

Derivation A.23.

<figure><img src="image_50.png" /></figure>
<figure><img src="image_51.png" /><figcaption>Derivation A.24.</figcaption></figure>

<figure><img src="image_52.png" /></figure>

<figure><img src="image_53.png" /></figure>

<figure><img src="image_54.png" /></figure>

<figure><img src="image_55.png" /><figcaption>Derivation A.25.</figcaption></figure>

<figure><img src="image_56.png" /></figure>

<figure><img src="image_57.png" /><figcaption>Derivation A.26.</figcaption></figure>

<figure><img src="image_58.png" /></figure>

<figure><img src="image_59.png" /></figure>

<figure><img src="image_60.png" /></figure>

<figure><img src="image_61.png" /></figure>
<figure><img src="image_62.png" /></figure>

<figure><img src="image_63.png" /></figure>

<figure><img src="image_64.png" /></figure>

<figure><img src="image_65.png" /></figure>

<figure><img src="image_66.png" /></figure>

<figure><img src="image_67.png" /></figure>

<figure><img src="image_68.png" /></figure>

Derivation A.27.

<figure><img src="image_69.png" /></figure>

<figure><img src="image_70.png" /></figure>

<figure><img src="image_71.png" /></figure>
<figure><img src="image_72.png" /></figure>

Derivation A.28.

<figure><img src="image_73.png" /></figure>

B Auxiliary derivations for RCliff₂

Derivation B.1.

<figure><img src="image_74.png" /></figure>

Derivation B.2.

<figure><img src="image_75.png" /></figure>

Derivation B.3.

<figure><img src="image_76.png" /></figure>
Derivation B.4.

<figure><img src="image_77.png" /></figure>

Derivation B.5.

<figure><img src="image_78.png" /></figure>

Derivation B.6.

<figure><img src="image_79.png" /></figure>

Derivation B.7.

<figure><img src="image_80.png" /></figure>

Derivation B.8.

<figure><img src="image_81.png" /></figure>
<figure><img src="image_82.png" /></figure>

Derivation B.9.

<figure><img src="image_83.png" /></figure>

Derivation B.10.

<figure><img src="image_84.png" /></figure>

C Auxiliary derivations for Cliff₃

Derivation C.1.

<figure><img src="image_85.png" /></figure>

Derivation C.2.

<figure><img src="image_86.png" /></figure>
**Derivation C.3.**

<figure><img src="image_87.png" /></figure>

**Derivation C.4.**

<figure><img src="image_88.png" /></figure>

**Derivation C.5.**

<figure><img src="image_89.png" /></figure>

**Derivation C.6.**

<figure><img src="image_90.png" /></figure>

**Derivation C.7.**

<figure><img src="image_91.png" /></figure>

**Derivation C.8.**

<figure><img src="image_92.png" /></figure>

**Derivation C.9.**

<figure><img src="image_93.png" /></figure>

**Derivation C.10.**

<figure><img src="image_94.png" /></figure>

**Derivation C.11.**

<figure><img src="image_95.png" /></figure>
XX:30 Simpler Presentations for Many Fragments of Quantum Circuits

Derivation C.12.

<figure><img src="image_96.png" /></figure>

Derivation C.13.

<figure><img src="image_97.png" /></figure>

Derivation C.14.

<figure><img src="image_98.png" /></figure>

Derivation C.15.

<figure><img src="image_99.png" /></figure>

Derivation C.16.

<figure><img src="image_100.png" /></figure>

Derivation C.17.

<figure><img src="image_101.png" /></figure>
Derivation C.18.

<figure><img src="image_102.png" /></figure>

Derivation C.19.

<figure><img src="image_103.png" /></figure>

Derivation C.20.

<figure><img src="image_104.png" /></figure>

Derivation C.21.

<figure><img src="image_105.png" /></figure>

Derivation C.22.

<figure><img src="image_106.png" /></figure>
Derivation C.23.

<figure><img src="image_107.png" /></figure>

Derivation C.24.

<figure><img src="image_108.png" /></figure>

Derivation C.25.

<figure><img src="image_109.png" /></figure>
Derivation C.26.

<figure><img src="image_110.png" /></figure>

Derivation C.27.

<figure><img src="image_111.png" /></figure>

Derivation C.28.

<figure><img src="image_112.png" /></figure>
**D** Auxiliary derivations for CliffT<sub>2</sub>

Derivation D.1.

<figure><img src="image_113.png" /></figure>

Derivation D.2.

<figure><img src="image_114.png" /></figure>

Derivation D.3.

<figure><img src="image_115.png" /></figure>

Derivation D.4.

<figure><img src="image_116.png" /></figure>

Derivation D.5.

<figure><img src="image_117.png" /></figure>

Derivation D.6.

<figure><img src="image_118.png" /></figure>

Derivation D.7.

<figure><img src="image_119.png" /></figure>

Derivation D.8.

<figure><img src="image_120.png" /></figure>
Derivation D.9.

<figure><img src="image_121.png" /></figure>

Derivation D.10.

<figure><img src="image_122.png" /></figure>

Derivation D.11.

<figure><img src="image_123.png" /></figure>

Derivation D.12.

<figure><img src="image_124.png" /></figure>
<figure><img src="image_125.png" /></figure>

Derivation D.13.

<figure><img src="image_126.png" /></figure>

Derivation D.14.

<figure><img src="image_127.png" /></figure>

Derivation D.15.

<figure><img src="image_128.png" /></figure>
XX:38 Simpler Presentations for Many Fragments of Quantum Circuits

<figure><img src="image_129.png" /></figure>

Derivation D.16.

<figure><img src="image_130.png" /></figure>

Derivation D.17.

<figure><img src="image_131.png" /></figure>
Derivation D.18.

<figure><img src="image_132.png" /></figure>

Derivation D.19.

<figure><img src="image_133.png" /></figure>

Derivation D.20.

<figure><img src="image_134.png" /></figure>

Derivation D.21.

<figure><img src="image_135.png" /></figure>
XX:40 Simpler Presentations for Many Fragments of Quantum Circuits

<figure><img src="image_136.png" /></figure>

<figure><img src="image_137.png" /></figure>

<figure><img src="image_138.png" /></figure>

<figure><img src="image_139.png" /></figure>

<figure><img src="image_140.png" /></figure>

Derivation D.22.

<figure><img src="image_141.png" /></figure>

<figure><img src="image_142.png" /></figure>

<figure><img src="image_143.png" /></figure>

Derivation D.23.

<figure><img src="image_144.png" /></figure>

<figure><img src="image_145.png" /></figure>

<figure><img src="image_146.png" /></figure>

<figure><img src="image_147.png" /></figure>

<figure><img src="image_148.png" /></figure>

<figure><img src="image_149.png" /></figure>
<figure><img src="image_150.png" /></figure>

<figure><img src="image_151.png" /></figure>

<figure><img src="image_152.png" /></figure>

<figure><img src="image_153.png" /></figure>

<figure><img src="image_154.png" /></figure>

<figure><img src="image_155.png" /></figure>

Derivation D.24.

<figure><img src="image_156.png" /></figure>

Derivation D.25.

<figure><img src="image_157.png" /></figure>

Derivation D.26.

<figure><img src="image_158.png" /></figure>

<figure><img src="image_159.png" /></figure>

<figure><img src="image_160.png" /></figure>

Derivation D.27.

<figure><img src="image_161.png" /></figure>

<figure><img src="image_162.png" /></figure>
<figure><img src="image_163.png" /><figcaption>Derivation D.29.</figcaption></figure>

<figure><img src="image_164.png" /></figure>
Derivation D.30.

<figure><img src="image_165.png" /></figure>

Derivation D.31.

<figure><img src="image_166.png" /></figure>
<figure><img src="image_167.png" /><figcaption>Derivation D.32.</figcaption></figure>

<figure><img src="image_168.png" /></figure>
<figure><img src="image_169.png" /></figure>

<figure><img src="image_170.png" /></figure>

<figure><img src="image_171.png" /></figure>

<figure><img src="image_172.png" /></figure>

<figure><img src="image_173.png" /></figure>

<figure><img src="image_174.png" /></figure>

<figure><img src="image_175.png" /></figure>

<figure><img src="image_176.png" /></figure>

<figure><img src="image_177.png" /></figure>

<figure><img src="image_178.png" /></figure>

<figure><img src="image_179.png" /></figure>

<figure><img src="image_180.png" /></figure>

<figure><img src="image_181.png" /></figure>

<figure><img src="image_182.png" /></figure>

<figure><img src="image_183.png" /></figure>

<figure><img src="image_184.png" /></figure>

<figure><img src="image_185.png" /></figure>
<figure><img src="image_186.png" /></figure>

<figure><img src="image_187.png" /></figure>

<figure><img src="image_188.png" /></figure>

<figure><img src="image_189.png" /></figure>

<figure><img src="image_190.png" /></figure>

<figure><img src="image_191.png" /></figure>

Derivation D.33.

<figure><img src="image_192.png" /></figure>

<figure><img src="image_193.png" /></figure>

<figure><img src="image_194.png" /></figure>

E Auxiliary derivations for CliffCS₂

Derivation E.1.

<figure><img src="image_195.png" /></figure>

<figure><img src="image_196.png" /></figure>

Derivation E.2.

<figure><img src="image_197.png" /></figure>

<figure><img src="image_198.png" /></figure>

<figure><img src="image_199.png" /></figure>

<figure><img src="image_200.png" /></figure>
<figure><img src="image_201.png" /></figure>

Derivation E.3.

<figure><img src="image_202.png" /></figure>

Derivation E.4.

<figure><img src="image_203.png" /></figure>

Derivation E.5.

<figure><img src="image_204.png" /></figure>

Derivation E.6.

<figure><img src="image_205.png" /></figure>
Derivation E.7.

<figure><img src="image_206.png" /></figure>

Derivation E.8.

<figure><img src="image_207.png" /></figure>

Derivation E.9.

<figure><img src="image_208.png" /></figure>

Derivation E.10.

<figure><img src="image_209.png" /></figure>
<figure><img src="image_210.png" /></figure>

Derivation E.11.

<figure><img src="image_211.png" /></figure>

Derivation E.12.

<figure><img src="image_212.png" /></figure>
**Proof of the decoding of Equation (C1), Equation (C2), Equation (C3).** Since the decoding only affects the ⊥ gate, these are trivial.

**Proof of the decoding of Equation (C4).**

$$D\left(\begin{array}{cccc} \text{---S---H---S---H---S---H---} \\ \text{(A.17)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{cccc} \text{---S---H---S---H---S---H---} \\ \text{(A.18)} \\ \hline \omega_8 \end{array}\right)$$

**Proof of the decoding of Equation (C5).**

$$D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.19)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.18)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.20)} \\ \hline \omega_8 \end{array}\right)$$

**Proof of the decoding of Equation (C6).**

$$D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.19)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.18)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.20)} \\ \hline \omega_8 \end{array}\right)$$

**Proof of the decoding of Equation (C7).**

$$D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.21)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.20)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.19)} \\ \hline \omega_8 \end{array}\right)$$

**Proof of the decoding of Equation (C8).**

$$D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.21)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.20)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.19)} \\ \hline \omega_8 \end{array}\right)$$

**Proof of the decoding of Equation (C9).**

$$D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.22)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.19)} \\ \hline \omega_8 \end{array}\right) = D\left(\begin{array}{c} \text{---S---H---S---H---S---H---} \\ \text{(A.18)} \\ \hline \omega_8 \end{array}\right)$$
Proof of the decoding of Equation (C10).

$$
\begin{align*}
D \left( \left[ \begin{smallmatrix} H \\ H \end{smallmatrix} \right] \right) &= \left[ \begin{smallmatrix} H \\ H \oplus H \\ H \\ H \end{smallmatrix} \right] \\
(A.23) \quad &\stackrel{\omega_8^\dagger}{=} \left[ \begin{smallmatrix} S & H \\ H & S \end{smallmatrix} \right] \left[ \begin{smallmatrix} S & H \\ H & S \end{smallmatrix} \right] = D \left( \left[ \begin{smallmatrix} S & H \\ H & S \end{smallmatrix} \right] \left[ \begin{smallmatrix} S & H \\ S & H \end{smallmatrix} \right] \right)
\end{align*}
$$

Proof of the decoding of Equation (C11).

$$
\begin{align*}
D \left( \left[ \begin{smallmatrix} H \\ H \end{smallmatrix} \right] \right) &= \left[ \begin{smallmatrix} H \\ H \oplus H \\ H \\ H \end{smallmatrix} \right] \\
(A.24) \quad &\stackrel{\omega_8^\dagger}{=} \left[ \begin{smallmatrix} S \\ S & H \\ H & S \end{smallmatrix} \right] = D \left( \left[ \begin{smallmatrix} S \\ S & H \\ H & S \end{smallmatrix} \right] \right)
\end{align*}
$$

Proof of the decoding of Equation (C12).

$$
D \left( \left[ \begin{smallmatrix} H \\ H \end{smallmatrix} \right] \right) = \left[ \begin{smallmatrix} H \\ H \oplus H \\ H \\ H \end{smallmatrix} \right] \quad (A.25) \quad \stackrel{(A.24)}{=} \left[ \begin{smallmatrix} H \\ H \oplus H \\ H \\ H \end{smallmatrix} \right] = D \left( \left[ \begin{smallmatrix} H \\ H \end{smallmatrix} \right] \right)
$$

Proof of the decoding of Equation (C13).

$$
\begin{align*}
& D \left( \left[ \begin{smallmatrix} H \\ H \\ H \\ H \\ H \end{smallmatrix} \right] \right) \\
&= \left[ \begin{smallmatrix} H \\ H \oplus H \\ H \\ H \oplus H \\ H \end{smallmatrix} \right] \\
&\stackrel{(A.26)}{=} \left[ \begin{smallmatrix} H \\ H \oplus H \\ H \\ H \oplus H \\ H \end{smallmatrix} \right] \\
&= D \left( \left[ \begin{smallmatrix} H \\ H \\ H \\ H \\ H \end{smallmatrix} \right] \right)
\end{align*}
$$
### Proof of the decoding of Equation (C14).

<figure><img src="image_213.png" /></figure>

### Proof of the decoding of Equation (C15).

<figure><img src="image_214.png" /></figure>

## G.2 Real-Clifford decoding

### Proof of the decoding of Equation (R1), Equation (R2), Equation (R3). Since the decoding only affects the ⊕ gate, these are trivial.

### Proof of the decoding of Equation (R4).

$$ \begin{gathered} D (\text{---}|\text{---}|\text{---}|\text{---}|\text{---}|\text{---}) = \text{---}|\text{---}|\text{---}|\text{---}|\text{---}|\text{---} \\ \stackrel{(\text{B.2})}{=} \text{---} = D (\text{---}) \end{gathered} $$

### Proof of the decoding of Equation (R5).

$$ D (\text{---}) = \text{---}|\text{---}|\text{---}|\text{---}|\text{---} \stackrel{(\text{B.3})}{=} \text{---} = D (\text{---}) $$
Proof of the decoding of Equation (R6).

$$D\left(\frac{\text{Z}}{\text{H}}\right) = \frac{\text{Z}}{\text{H}} \underset{(B.4)}{\overset{(B.5)}{\bigoplus}} \text{Z} = \frac{\text{Z}}{\text{H}} \underset{(B.4)}{\overset{(B.5)}{\bigoplus}} \text{H} = D\left(\frac{\text{Z}}{\text{H}}\right)$$

Proof of the decoding of Equation (R7).

$$D\left(\frac{\text{Z}}{\text{H}}\right) = \frac{\text{Z}}{\text{H}} \underset{(B.5)}{\overset{(B.4)}{\bigoplus}} \text{H} = \frac{\text{H}}{\text{H}} \underset{(B.5)}{\overset{(B.4)}{\bigoplus}} \text{Z} = D\left(\frac{\text{Z}}{\text{H}}\right)$$

Proof of the decoding of Equation (R8).

$$D\left(\frac{\text{H}}{\text{H}}\right) = \frac{\text{H}}{\text{H}} \underset{(B.6)}{\overset{(B.5)}{\bigoplus}} \text{H} = D\left(\frac{\text{H}}{\text{H}}\right)$$

Proof of the decoding of Equation (R9).

$$D\left(\frac{\text{H}}{\text{H}}\right) = \frac{\text{H}}{\text{H}} \underset{(B.7)}{\overset{(B.6)}{\bigoplus}} \text{H} = D\left(\frac{\text{H}}{\text{H}}\right)$$

Proof of the decoding of Equation (R10).

$$D\left(\frac{\text{H}}{\text{H}}\right) = \frac{\text{H}}{\text{H}} \underset{(B.8)}{\overset{(B.7)}{\bigoplus}} \text{H} = D\left(\frac{\text{H}}{\text{H}}\right)$$

Proof of the decoding of Equation (R11).

$$D\left(\frac{\text{H}}{\text{H}}\right) = \frac{\text{H}}{\text{H}} \underset{(B.9)}{\overset{(B.8)}{\bigoplus}} \text{H} = D\left(\frac{\text{H}}{\text{H}}\right)$$
**Proof of the decoding of Equation (R12).**

$$D\left(\left(\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right)\right) = \left(\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right) = D\left(\left(\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right)\right)$$

<figure><img src="image_215.png" /></figure>

**Proof of Equations (S) (R13), (R14), (R15) and (R16). Equations (S), (R13), (R14), (R15) and (R16) of RCliff² source respectively correspond to Equations (S), (C12), (C13), (C14) and (C15) of Cliff² source. One could straightforwardly mimic the proofs of Equations Cᵢ to prove Equations Rⱼ.**

<figure><img src="image_216.png" /></figure>

### G.3 Qutrit-Clifford decoding

**Proof of the decoding of Equation (C1).**

$$D\left(\left(\begin{array}{c}(-\omega)^{6} \\ \hline \end{array}\right)\right) = \left(\begin{array}{c}\omega^{60} \\ \hline\end{array}\right) \stackrel{(\omega^{12})}{=} \left(\begin{array}{c}1 \\ \hline\end{array}\right) = D\left(\left(\begin{array}{c}1 \\ \hline\end{array}\right)\right)$$

<figure><img src="image_217.png" /></figure>

**Proof of the decoding of Equation (C2).**

$$D\left(-\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right) = -\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array} \stackrel{(H^4)(\omega^{12})}{=} \text{---} = D(\text{---})$$

<figure><img src="image_218.png" /></figure>

**Proof of the decoding of Equation (C3).**

$$D\left(-\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right) = -\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array} \stackrel{(S^3)(\omega^{12})}{=} \text{---} = D(\text{---})$$

<figure><img src="image_219.png" /></figure>

**Proof of the decoding of Equation (C4).**

$$D\left(-\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right) = -\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array} \stackrel{(C.30)}{=} \left(\begin{array}{c}\omega^{51} \\ \hline\end{array}\right) = D\left(-\begin{array}{c}(-\omega) \\ \hline\end{array}\right)$$

<figure><img src="image_220.png" /></figure>

**Proof of the decoding of Equation (C5).**

$$D\left(-\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right) = -\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array} \stackrel{(SS')}{=} -\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array} \stackrel{(\omega^{44})}{=} D\left(-\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right)$$

<figure><img src="image_221.png" /></figure>

**Proof of the decoding of Equation (C6).**

$$D\left(\left(\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right)\right) = \left(\begin{array}{ccccccccc}
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\hline
& & & & & & & & & \\
& & & & & & & & & \\
& & & & & & & & & \\
\end{array}\right) \stackrel{(H^4)(C.21)}{=} \text{---} = D(\text{---})$$

<figure><img src="image_222.png" /></figure>
Proof of the decoding of Equation (C8).

$$D\left(\left[\begin{array}{c|c} \text{S} & \text{S}^{2} \\ \text{H}^{\dagger} & \text{H} \end{array}\right]\right) = \left(\begin{array}{c|c} \text{S}^{2} & \text{S}^{2} \\ \text{H}^{\dagger} & \text{H} \end{array}\right) \stackrel{\left(\text{C.18}\right)}{=} \left(\begin{array}{c|c} \text{S}^{2} & \text{S}^{2} \\ \text{H}^{\dagger} & \text{H} \end{array}\right) \stackrel{\left(\text{C.18}\right)}{=} D\left(\left[\begin{array}{c|c} \text{S} & \text{S}^{2} \\ \text{H}^{\dagger} & \text{H} \end{array}\right]\right)$$

Proof of the decoding of Equation (C9).

$$D\left(\left[\begin{array}{c|c} \text{H}^{2} & \text{H}^{2} \\ \text{H}^{\dagger} & \text{H} \end{array}\right]\right) = \left(\begin{array}{c|c} \text{H}^{2} & \text{H}^{2} \\ \text{H}^{\dagger} & \text{H} \end{array}\right) \stackrel{\left(\text{C.18}\right)}{=} \stackrel{\left(\text{KC}\right)}{=} \left(\begin{array}{c|c} \text{H}^{2} & \text{H}^{2} \\ \text{H}^{\dagger} & \text{H} \end{array}\right) \stackrel{\left(\text{KC}\right)}{=} D\left(\left[\begin{array}{c|c} \text{H}^{2} & \text{H}^{2} \\ \text{H}^{\dagger} & \text{H} \end{array}\right]\right)$$

Proof of the decoding of Equation (C13).

$$D\left(\left[\begin{array}{c|c} \text{S} & \text{S}^{2} \text{H}^{4} \text{H}^{4} \\ \text{H}^{\dagger} & \text{H}^{4} \text{H}^{4} \text{S}^{2} \text{S}^{2} \end{array}\right]\right) = \left(\begin{array}{c|c} \text{S}^{2} \text{H}^{4} \text{H}^{4} & \text{H}^{4} \text{H}^{4} \text{S}^{2} \\ \text{H}^{\dagger} \text{H}^{\dagger} & \text{H}^{4} \text{H}^{4} \text{S}^{2} \text{S}^{2} \end{array}\right) \stackrel{\left(\text{C.25}\right)}{=} \stackrel{\left(\text{KC}\right)}{=} \left(\begin{array}{c|c} \text{H}^{4} \text{H}^{4} \text{S}^{2} & \text{S}^{2} \\ \text{H}^{\dagger} \text{H}^{\dagger} \text{S}^{2} \text{S}^{2} & \text{H}^{4} \text{H}^{4} \text{S}^{2} \text{S}^{2} \end{array}\right) \stackrel{\left(\text{KC}\right)}{=} D\left(\left[\begin{array}{c|c} \text{S} & \text{S}^{2} \\ \text{S}^{\prime} & \text{S}^{\prime} \end{array}\right]\right)$$

Proof of the decoding of Equation (C14).

$$D\left(\left[\begin{array}{c|c} \text{H}^{4} & \text{H}^{4} \\ \text{H}^{\dagger} & \text{H} \end{array}\right]\right) = \left(\begin{array}{c|c} \text{H}^{4} & \text{H}^{4} \\ \text{H}^{\dagger} & \text{H} \end{array}\right) \stackrel{\left(\text{C.26}\right)}{=} \stackrel{\left(\text{KC}\right)}{=} \left(\begin{array}{c|c} \text{H}^{4} & \text{H}^{4} \\ \text{H}^{\dagger} & \text{H}^{\prime 2} \text{S}^{2} \text{S}^{2} \end{array}\right) \stackrel{\left(\text{KC}\right)}{=} D\left(\left[\begin{array}{c|c} \text{H}^{4} & \text{H}^{\prime 2} \text{S}^{2} \\ \text{H}^{\dagger} & \text{H}^{\prime 2} \text{S}^{2} \text{S}^{2} \end{array}\right]\right)$$

Proof of the decoding of Equation (C15).

$$D\left(\left[\begin{array}{c|c} \text{H} & \text{H}^{\dagger} \\ \text{H}^{\dagger} & \text{H} \end{array}\right]\right) = \left(\begin{array}{c|c} \text{H} & \text{H}^{\dagger} \\ \text{H}^{\dagger} & \text{H} \end{array}\right) \stackrel{\left(\text{C.29}\right)}{=} \left(\begin{array}{c|c} \text{H} & \text{H}^{\dagger} \\ \text{H}^{\dagger} & \text{H} \end{array}\right) = D\left(\left[\begin{array}{c|c} \text{H} & \text{H}^{\dagger} \\ \text{H}^{\dagger} & \text{H} \end{array}\right]\right)$$
Proof of the decoding of Equation (C8).

$$D\left(\left[\begin{array}{c|c|c}\text{S} & \text{S} & \text{S} \\ \text{H} & \text{H} & \text{H}\end{array}\right]\right) = \left[\begin{array}{c|c|c}\text{S} & \text{S} & \text{S} \\ \text{H} & \text{H} & \text{H}\end{array}\right] \stackrel{(\text{D.6})}{=} \left[\begin{array}{c|c|c}\text{S} & \text{S} & \text{S} \\ \text{H} & \text{H} & \text{H}\end{array}\right] = D\left(\left[\begin{array}{c|c|c}\text{S} & \text{S} & \text{S} \\ \text{H} & \text{H} & \text{H}\end{array}\right]\right)$$

Proof of the decoding of Equation (C9).

$$D\left(\left[\begin{array}{c|c|c}\text{S} & \text{S} & \text{S} \\ \text{H} & \text{H} & \text{H}\end{array}\right]\right) = \left[\begin{array}{c|c|c}\text{S} & \text{S} & \text{S} \\ \text{H} & \text{H} & \text{H}\end{array}\right] \stackrel{(\text{D.6})(\text{D.10})}{=} \left[\begin{array}{c|c|c}\text{H} & \text{H} & \text{H} \\ \text{S} & \text{S} & \text{S}\end{array}\right] = D\left(\left[\begin{array}{c|c|c}\text{S} & \text{S} & \text{S} \\ \text{H} & \text{H} & \text{H}\end{array}\right]\right)$$

Proof of the decoding of Equation (C10).

$$D\left(\left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{S} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{H}\end{array}\right]\right) = \left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{S} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{H}\end{array}\right] \stackrel{(\text{D.26})}{=} \left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{S} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{S}\end{array}\right] = D\left(\left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{S} & \text{H} \\ \text{S} & \text{S} & \text{S} & \text{H}\end{array}\right]\right)$$

Proof of the decoding of Equation (C11).

$$D\left(\left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{S} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{H}\end{array}\right]\right) = \left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{S} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{H}\end{array}\right] \stackrel{(\text{D.27})}{=} \left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{S} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{S}\end{array}\right] = D\left(\left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{S} & \text{H} \\ \text{H} & \text{S} & \text{S} & \text{H}\end{array}\right]\right)$$

Proof of the decoding of Equation (C12).

$$D\left(\left[\begin{array}{c|c|c|c}\text{H} & \text{H} & \text{H} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{H}\end{array}\right]\right) = \left[\begin{array}{c|c|c|c}\text{H} & \text{H} & \text{H} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{H}\end{array}\right] \stackrel{(\text{D.28})}{=} \left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{H} & \text{S} \\ \text{H} & \text{H} & \text{H} & \text{S}\end{array}\right] = D\left(\left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{H} & \text{S} \\ \text{H} & \text{S} & \text{H} & \text{S}\end{array}\right]\right)$$

Proof of the decoding of Equation (C13).

$$D\left(\left[\begin{array}{c|c|c|c}\text{H} & \text{H} & \text{H} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{H}\end{array}\right]\right) = \left[\begin{array}{c|c|c|c}\text{H} & \text{H} & \text{H} & \text{H} \\ \text{H} & \text{H} & \text{H} & \text{H}\end{array}\right] \stackrel{(\text{D.29})}{=} \left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{H} & \text{S} \\ \text{S} & \text{H} & \text{H} & \text{S}\end{array}\right] = D\left(\left[\begin{array}{c|c|c|c}\text{H} & \text{S} & \text{H} & \text{S} \\ \text{S} & \text{H} & \text{H} & \text{S}\end{array}\right]\right)$$
Proof of the decoding of Equation (S).

<figure><img src="image_223.png" /></figure>

◀

## G.5 Clifford+CS decoding

Proof of the decoding of Equation (S).

<figure><img src="image_224.png" /></figure>

◀

Proof of the decoding of Equation (C3). Since the decoding does not affect the $\bar{s}$- and $\bar{i}$-gates, this is trivial. ▶

Proof of the decoding of Equation (C1).

$$D(\stackrel{\omega^8}{\otimes}) = \stackrel{(\omega^8)}{\otimes} = D(\otimes)$$

◀

Proof of the decoding of Equation (C2).

$$D(-\bar{K^2}) = -\bar{H}\bar{H} - \stackrel{(\bar{H^2})(\omega^8)}{\otimes} = \stackrel{\bar{\omega}^6}{\otimes} = D(\bar{\omega}^6)$$

◀

Proof of the decoding of Equation (C4).

$$D(-\bar{S}\bar{K}\bar{S}\bar{K}\bar{S}\bar{K}-) = -\bar{S}\bar{H}\bar{S}\bar{H}\bar{S}\bar{H}-\stackrel{(\bar{\omega}^8)}{\otimes} = D(\bar{\omega}^6)$$

◀

Proof of the decoding of Equation (C5).

$$D(\bar{\otimes}) = \bar{\otimes} \stackrel{(\text{E.2})}{=} \bar{\otimes} = D(\bar{\otimes})$$

◀

Proof of the decoding of Equation (C6).

$$D(-\bar{S}\bar{\otimes}) = -\bar{S}\bar{\otimes} \stackrel{(\text{E.3})}{=} \bar{S}\bar{\otimes} = D(\bar{S}\bar{\otimes})$$

◀
Proof of the decoding of Equation (C7).

$$D\left(\boxed{S}\right) = \boxed{S} \stackrel{(\text{E.4})}{\equiv} \boxed{S} = D\left(\boxed{S}\right)$$

Proof of the decoding of Equation (C8).

$$\begin{array}{c} D\left(\boxed{K \ Z \ K} \quad \boxed{H \ Z \ H} \quad \boxed{\omega_8^{14}}\right) \\ \stackrel{(\text{E.5})}{\equiv} \boxed{H \ Z \ H} \quad \boxed{\omega_8^{14}} = D\left(\boxed{K \ Z \ K} \quad \boxed{H \ Z \ K} \quad \boxed{S}\right) \end{array}$$

Proof of the decoding of Equation (C9).

$$\begin{array}{c} D\left(\boxed{K \ Z \ K} \quad \boxed{H \ Z \ H} \quad \boxed{\omega_8^{14}}\right) \\ \stackrel{(\text{E.6})}{\equiv} \boxed{S} \quad \boxed{H \ Z \ H} \quad \boxed{\omega_8^{14}} = D\left(\boxed{S} \quad \boxed{K \ Z \ K} \quad \boxed{H}\right) \end{array}$$

Proof of the decoding of Equation (C10).

$$\begin{array}{c} D\left(\boxed{S \ K} \quad \boxed{H \ H} \quad \boxed{\omega_8^{14}}\right) \\ \stackrel{(\text{CE})}{\equiv} \boxed{H} \quad \boxed{H \ S} \quad \boxed{\omega_8^{14}} = D\left(\boxed{K} \quad \boxed{K \ S} \quad \boxed{H}\right) \end{array}$$

Proof of the decoding of Equation (C11).

$$\begin{array}{c} D\left(\boxed{S \ K} \quad \boxed{H \ H} \quad \boxed{\omega_8^{14}}\right) \\ \stackrel{(\text{E.7})}{\equiv} \boxed{H} \quad \boxed{H \ S} \quad \boxed{\omega_8^{14}} = D\left(\boxed{K} \quad \boxed{K \ S} \quad \boxed{H}\right) \end{array}$$

Proof of the decoding of Equation (C12).

$$D\left(\boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \right) = D\left(\boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \quad \boxed{S} \right)$$
Proof of the decoding of Equation (C13).

$$ \begin{array}{ccc} \begin{array}{c} D \left( \begin{array}{|c|c|c} \bullet & \bullet & \bullet \\ \bullet & \bullet & \bullet \\ \bullet & \bullet & \bullet \end{array} \right) \\ \begin{array}{c} \xrightarrow{\text{(E.9)}} \\ \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{64}$}; \end{tikzpicture} \end{array} \end{array} & = & \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{64}$}; \end{tikzpicture} \\ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{64}$}; \end{tikzpicture} \end{array} \end{array} $$

Proof of the decoding of Equation (C14).

$$ \begin{array}{ccc} \begin{array}{c} D \left( \begin{array}{|c|c|c} \bullet & \bullet & \bullet \\ \bullet & \bullet & \bullet \\ \bullet & \bullet & \bullet \end{array} \right) \\ \begin{array}{c} \xrightarrow{\text{(E.10)}} \\ \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{32}$}; \end{tikzpicture} \end{array} \end{array} & = & \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{32}$}; \end{tikzpicture} \\ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{32}$}; \end{tikzpicture} \end{array} \end{array} $$

Proof of the decoding of Equation (C15).

$$ \begin{array}{ccc} \begin{array}{c} D \left( \begin{array}{|c|c|c} \bullet & \bullet & \bullet \\ \bullet & \bullet & \bullet \\ \bullet & \bullet & \bullet \end{array} \right) \\ \begin{array}{c} \xrightarrow{\text{(E.11)}} \\ \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{64}$}; \end{tikzpicture} \end{array} \end{array} & = & \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{64}$}; \end{tikzpicture} \\ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{64}$}; \end{tikzpicture} \end{array} \end{array} $$

Proof of the decoding of Equation (C16).

$$ \begin{array}{ccc} \begin{array}{c} D \left( \begin{array}{|c|c|c} \text{K} & \text{K} & \text{K} \\ \text{H} & \text{H} & \text{H} \\ \text{SH}_k & \text{H} & \text{H} \end{array} \right) \\ \begin{array}{c} \xrightarrow{\text{(SH}_k)} \\ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{21}$}; \end{tikzpicture} \end{array} & = & \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{21}$}; \end{tikzpicture} \\ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (top) at (0,0) {\begin{tikzpicture}[baseline=-0.5ex, scale=0.7] \draw (0,0) circle (0.4); \node at (0,0) {\textcircled{0}}; \draw (0,0) -- (0.4,0); \draw (0,0) -- (-0.4,0); \draw (0,0) -- (0,0.4); \draw (0,0) -- (-0.4,0.4); \node at (0,0.2) {\textcircled{1}}; \draw (0,0.4) circle (0.4); \node at (0,0.4) {\textcircled{2}}; \draw (0,0.4) -- (0.4,0.4); \draw (0,0.4) -- (-0.4,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) circle (0.4); \node at (0,0.2) {\textcircled{3}}; \draw (0,0.2) -- (0,0.4); \draw (0,0.4) -- (0,0.2); \draw (0,0.2) -- (0,0.2) node right {$\omega_8^{21}$}; \end{tikzpicture} \end{array} \end{array} $$
Proof of the decoding of Equation (C17).

<figure><img src="image_225.png" /></figure>

<figure><img src="image_226.png" /></figure>

H CNOT-dihedral circuits

This appendix supplies the fragment-specific proof obligations for the CNOT-dihedral completeness statement in Section 4. Unlike the other fragments, we do not need an encoding/decoding transfer here: the source presentation of 16 already lives in a PROP setting with the same scalar convention as our master signature.

What *does* need to be checked is that our smaller rule set CNOTdihe₂ is conservative with respect to the original one: every axiom of 16 that we omit must be derivable from CNOTdihe₂. The lemmas below provide exactly these derivations, so that the imported completeness theorem applies unchanged.

► **Remark 41.** Equation (R4) follows by the same rewriting used in the section for Clifford+T.

**Derivation H.1. Equation (R2)**

<figure><img src="image_227.png" /></figure>

**Derivation H.2. Equation (R3)**

<figure><img src="image_228.png" /></figure>

**Derivation H.3. Equation (R5)**

<figure><img src="image_229.png" /></figure>

**Derivation H.4. Equation (R8)**

<figure><img src="image_230.png" /></figure>
**Derivation H.5. Equation (R11)**

<figure><img src="image_231.png" /></figure>

## I Scalar refinement

This appendix justifies the scalar-refinement step used in Section 4.1. The short version is the following: in the strict semantics adopted in this paper, global phases are part of the data of the fragment. Consequently, two syntactic presentations of the same gate fragment may nevertheless denote different semantic subPROPs if they generate different subgroups of global phases. When importing completeness theorems stated with a different scalar convention, we therefore first align scalar subgroups by conservatively extending the syntax with an additional scalar generator.

The main technical claim proved here is that, under mild assumptions satisfied by all our unitary fragments, adjoining a new root-of-unity scalar and relating it to an existing one is a conservative extension: it does not introduce any new equalities between circuits that do not mention the new scalar. Equivalently, the induced interpretation remains faithful.

**Definition 42.** Let $\mathbf{P}$ be a PROP. Its scalars are the endomorphisms of the tensor unit, $S(\mathbf{P}) := \mathbf{P}(0,0)$. Since 0 is the monoidal unit, both $\circ$ and $\otimes$ restrict to binary operations $S(\mathbf{P}) \times S(\mathbf{P}) \to S(\mathbf{P})$, and they coincide by interchange. In particular, $S(\mathbf{P})$ is a commutative monoid (and a group whenever $\mathbf{P}$ is a groupoid).

**Definition 43.** Let $\mathbf{C}$ be a (strict) symmetric monoidal subcategory of FdHilb and assume $\mathbf{C}$ is endomorphism-only: $\mathbf{C}(n, m) = \emptyset$ for $n \neq m$. For $n \in \mathbb{N}$, a unitary $U \in \mathbf{C}(n, n)$ is a global phase on $n$ wires if it is a scalar multiple of the identity:

$$ U = \lambda \mathrm{id}_n \quad \text{for some } \lambda \in U(1) = \{z \in \mathbb{C} \mid |z| = 1\}. $$

In words: $U$ acts trivially on all states and only contributes a phase factor $\lambda$.

**Definition 44.** Let $\mathbf{C} \subseteq \mathrm{FdHilb}$ be a symmetric monoidal subcategory. The visible scalar subgroup of $\mathbf{C}$ is $S(\mathbf{C}) := \mathbf{C}(0,0) \subseteq U(1)$. Every element $\lambda \in S(\mathbf{C})$ yields a global phase on $n$ wires by tensoring: $\lambda \otimes \mathrm{id}_n = \lambda \mathrm{id}_n \in \mathbf{C}(n, n)$.

**Definition 45.** Let $\mathbf{C} \subseteq \mathrm{FdHilb}$ be an endomorphism-only symmetric monoidal category. A phase $\lambda \in U(1)$ is called a hidden phase of $\mathbf{C}$ if there exists some arity $n \ge 1$ such that $\lambda \mathrm{id}_n \in \mathbf{C}(n, n)$ while $\lambda \notin S(\mathbf{C})$.

Equivalently, $\lambda$ is hidden if it occurs as a global phase at some positive wire count, but cannot be produced as a scalar morphism $0 \to 0$ inside $\mathbf{C}$.

**Example 46.** Consider the subgroup $\mathbf{C} \subseteq \mathrm{Qubit}$ generated (as a symmetric monoidal subcategory) by a single 1-qubit gate $R_X(2\pi)$, but with no scalar generators. Semantically, $R_X(2\pi) = -\mathrm{id}_1$, hence $-\mathrm{id}_1 \in \mathbf{C}(1, 1)$. However, $S(\mathbf{C}) = \{1\}$ because there are no nontrivial $0 \to 0$ morphisms available. Thus $\lambda = -1$ is a hidden phase in the sense of Definition 45.

If we were to adjoin a new scalar generator $\omega$ interpreted as $-1$, then $\omega \otimes \mathrm{id}_1$ and the existing circuit $R_X(2\pi)$ would have the same semantics; without additional axioms linking them, this would typically destroy faithfulness of the interpretation. The “no hidden phases” assumption used below precisely rules out this situation.

The conservativity argument relies on the observation that scalars commute with all endomorphisms, so new scalar generators can always be “pulled out” as a single global phase factor.
**Lemma 47.** Let $\mathcal{C}$ be a strict symmetric monoidal category. For any scalar $a: 0 \to 0$ and any endomorphism $f: n \to n$ one has

$$ (a \otimes \mathrm{id}_n) \circ f = f \circ (a \otimes \mathrm{id}_n). \qquad (5) $$

Moreover, for scalars $a, b: 0 \to 0$, composition and tensor coincide: $a \circ b = a \otimes b$.

**Proof.** Since the tensor is bifunctorial and the category is strict,

$$ (a \otimes \mathrm{id}_n) \circ f = (a \circ \mathrm{id}_0) \otimes (\mathrm{id}_n \circ f) = (\mathrm{id}_0 \circ a) \otimes (f \circ \mathrm{id}_n) = f \circ (a \otimes \mathrm{id}_n), $$

using the interchange law. For scalars, the same computation with $n = 0$ yields $a \circ b = a \otimes b$. ◀

We now formalise the scalar-refinement step as an extension of a presentation by adjoining a new scalar generator of higher order.

**Definition 48.** For $m \ge 1$ write $\mu_m := \{e^{2\pi ik/m} | 0 \le k < m\} \subseteq U(1)$ for the cyclic group of $m$-th roots of unity.

**Definition 49.** Let $\mathbf{P}^{\mathrm{src}}/\mathcal{R}^{\mathrm{src}}$ be a presented PROP and let $s: 0 \to 0$ be a chosen scalar in the src signature. Fix integers $m \ge 1$ and $\ell \ge 1$. Define $\mathbf{P}^{\mathrm{src},\#}/\mathcal{R}^{\mathrm{src},\#}$ to be the presentation obtained by adjoining a new scalar generator $\omega: 0 \to 0$ and adding the two relations

$$ \omega^{ml} = \mathrm{id}_0, \qquad \omega^r = s, \qquad (6) $$

where $\omega^k$ denotes the $k$-fold composite of $\omega$ (equivalently, $k$-fold tensor), and $r$ is an integer chosen so that semantically $\omega^r$ matches $s$ (see below).

**Remark 50.** The relations (6) assert that $\omega$ has order dividing $ml$, and that the src scalar $s$ is the $r$-th power of $\omega$. Concretely, this is the standard “adjoin a root” construction at the level of scalars. The point of Lemma 52 below is that, in a PROP setting, adjoining such a root is conservative provided there are no hidden phases.

The centrality of scalars yields a simple normal form in the refined syntax: all occurrences of $\omega$ can be extracted into a single scalar factor.

**Lemma 51.** In the refined PROP $\mathbf{P}^{\mathrm{src},\#}/\mathcal{R}^{\mathrm{src},\#}$, every morphism $C: n \to n$ is derivably equal to one of the form

$$ C = \omega^a \otimes C', \qquad (7) $$

where $a \in \{0, 1, \dots, ml-1\}$ and $C'$ is a morphism built using only the src generators (i.e. $C'$ contains no occurrence of $\omega$).

**Proof.** Work in the free PROP on the refined signature, modulo PROP coherence and the relations $\mathcal{R}^{\mathrm{src}}$ and (6). Because $\omega$ is a scalar, every occurrence of $\omega$ in a diagram is a $0 \to 0$ component tensored somewhere with an endomorphism. By Lemma 47, we can slide each such component past all other boxes and past all compositions/tensors so as to collect all $\omega$-factors together as a single power $\omega^a$ tensored with a diagram $C'$ that contains no $\omega$. Finally, use $\omega^{ml} = \mathrm{id}_0$ to reduce a modulo $ml$ into the stated range. ◀

We can now state and prove the main lemma used in Section 4.1.

**Lemma 52.** Let $\mathbf{P}^{\mathrm{src}}/\mathcal{R}^{\mathrm{src}}$ be a graphical language equipped with a faithful (i.e. complete) strict symmetric monoidal interpretation $[\cdot]_{\mathrm{src}}: \mathbf{P}^{\mathrm{src}}/\mathcal{R}^{\mathrm{src}} \to \mathbf{C}^{\mathrm{src}} \subseteq \mathbf{FdHilb}$. Assume the following semantic properties.
1. (finite cyclic visible scalars) The scalar group $S(\mathbf{C}^{\text{src}}) = \mathbf{C}^{\text{src}}(0,0)$ is finite cyclic of order $m$ and generated by $\llbracket s \rrbracket_{\text{src}}$ for some chosen src scalar $s: 0 \to 0$. Equivalently, $S(\mathbf{C}^{\text{src}}) \cong \mu_m$.

2. (no hidden phases) $\mathbf{C}^{\text{src}}$ has no hidden phases: for all $n \in \mathbb{N}$ and all $\lambda \in \mathcal{U}(1)$, if $\lambda \text{id}_n \in \mathbf{C}^{\text{src}}(n, n)$ then $\lambda \in S(\mathbf{C}^{\text{src}})$ (cf. Definition 45).

3. (invertibility) Every morphism in $\mathbf{C}^{\text{src}}$ is invertible, i.e. each hom-set $\mathbf{C}^{\text{src}}(n, n)$ is a group under composition.<fnref n="2" />

Fix $\ell \ge 1$ and choose a root of unity $\zeta \in \mathcal{U}(1)$ of order $m\ell$. Choose an integer $r$ such that

$$ \zeta^r = \llbracket s \rrbracket_{\text{src}}. \qquad (8) $$

Form the scalar-refined presentation $\mathbf{P}^{\text{src},\#}/\mathcal{R}^{\text{src},\#}$ as in Definition 49.

Let $\mathbf{C}^{\#} \subseteq \mathbf{FdHilb}$ be the subPROP generated by $\mathbf{C}^{\text{src}}$ together with the scalar $\zeta: 0 \to 0$ (viewed as the unitary map $\mathbb{C} \to \mathbb{C}$, $1 \mapsto \zeta$).

Then the interpretation functor extends uniquely to a strict symmetric monoidal functor $\llbracket \cdot \rrbracket^{\#}: \mathbf{P}^{\text{src},\#}/\mathcal{R}^{\text{src},\#} \to \mathbf{C}^{\#}$ sending $\omega$ to $\zeta$, and $\llbracket \cdot \rrbracket^{\#}$ is faithful.

In particular, the refined language is complete for $\mathbf{C}^{\#}$ and $S(\mathbf{C}^{\#}) \cong \mu_{m\ell}$.

**Proof.** (1) Soundness and existence of the refined interpretation. By construction, $\llbracket \cdot \rrbracket^{\#}$ agrees with $\llbracket \cdot \rrbracket_{\text{src}}$ on all src generators. We interpret the new generator $\omega$ by the scalar $\zeta$. The additional relations (6) hold semantically because $\zeta^{m\ell} = 1$ and $\zeta^r = \llbracket s \rrbracket_{\text{src}}$ by (8). Therefore the universal property of presented PROPs yields a unique induced functor $\llbracket \cdot \rrbracket^{\#}$ into $\mathbf{C}^{\#}$.

(2) Scalar extraction in the refined syntax. By Lemma 51, every refined circuit $C: n \to n$ is derivably equal to $\omega^a \otimes C'$ with $0 \le a < m\ell$ and $C'$ an src circuit.

(3) Faithfulness. Let $C_1, C_2: n \to n$ be refined circuits such that $\llbracket C_1 \rrbracket^{\#} = \llbracket C_2 \rrbracket^{\#}$. Write both in scalar-extraction normal form: $C_i = \omega^{a_i} \otimes C'_i$ ($0 \le a_i < m\ell$), with $C'_i$ containing no $\omega$. Let $U_i := \llbracket C'_i \rrbracket_{\text{src}} \in \mathbf{C}^{\text{src}}(n, n)$. The semantic equality becomes

$$ \zeta^{a_1} U_1 = \zeta^{a_2} U_2. \qquad (9) $$

By invertibility 3, we can right-multiply by $U_2^{-1}$ to obtain

$$ \zeta^{a_2-a_1} \text{id}_n = U_1 \circ U_2^{-1} \in \mathbf{C}^{\text{src}}(n, n). \qquad (10) $$

Thus $\zeta^{a_2-a_1}$ appears as a global phase in $\mathbf{C}^{\text{src}}$ on $n$ wires. By the no-hidden-phases assumption 2, this implies $\zeta^{a_2-a_1} \in S(\mathbf{C}^{\text{src}})$. By 1, there exists $t \in \{0, \dots, m-1\}$ such that

$$ \zeta^{a_2-a_1} = \llbracket s \rrbracket_{\text{src}}^t. \qquad (11) $$

Combining (9) with (11) gives $\llbracket C'_1 \rrbracket_{\text{src}} = \llbracket s^t \otimes C'_2 \rrbracket_{\text{src}}$. Since $\llbracket \cdot \rrbracket_{\text{src}}$ is faithful by hypothesis, $\mathbf{P}^{\text{src}}/\mathcal{R}^{\text{src}} \vdash C'_1 = s^t \otimes C'_2$. The refined presentation contains all src relations, so the same derivation is valid in $\mathbf{P}^{\text{src},\#}/\mathcal{R}^{\text{src},\#}$. Now use the refinement relation $\omega^r = s$ to rewrite $s^t = \omega^{rt}$, yielding $C_1 = \omega^{a_1} \otimes C'_1 = \omega^{a_1} \otimes \omega^{rt} \otimes C'_2 = \omega^{a_1+rt} \otimes C'_2$.

It remains to compare the exponents. From (11) and (8) we have $\zeta^{a_2-a_1} = \zeta^{rt}$, so $\zeta^{a_2-a_1-rt} = 1$. Since $\zeta$ has order $m\ell$, this implies $a_2 - a_1 - rt \equiv 0 \pmod{m\ell}$. Using $\omega^{m\ell} = \text{id}_0$ in the refined syntax, we conclude $\omega^{a_1+rt} = \omega^{a_2}$, hence $C_1 = \omega^{a_2} \otimes C'_2 = C_2$. Therefore $\llbracket \cdot \rrbracket^{\#}$ is faithful.

(4) Scalars of $\mathbf{C}^{\#}$. By definition, $S(\mathbf{C}^{\#})$ is generated by $S(\mathbf{C}^{\text{src}}) = \langle \llbracket s \rrbracket_{\text{src}} \rangle$ together with $\zeta$. Since $\llbracket s \rrbracket_{\text{src}} = \zeta^r \in \langle \zeta \rangle$, we obtain $S(\mathbf{C}^{\#}) = \langle \zeta \rangle \cong \mu_{m\ell}$. ◀

<footnote n="2">² In all applications in this paper, $\mathbf{C}^{\text{src}}$ consists of unitaries, hence this holds automatically.</footnote>
**► Corollary 53.** With the hypotheses of Lemma 52, let $C_1, C_2$ be src circuits (i.e. containing no occurrence of $\omega$). If $\mathbf{P}^{\text{src},\#}/\mathcal{R}^{\text{src},\#} \vdash C_1 = C_2$, then already $\mathbf{P}^{\text{src}}/\mathcal{R}^{\text{src}} \vdash C_1 = C_2$.

**Proof.** If the refined theory derives $C_1 = C_2$, then in particular $[[C_1]]_{\text{src}} = [[C_2]]_{\text{src}}$ (because the refined interpretation restricts to the src one on src syntax). Faithfulness of $[[\cdot]]_{\text{src}}$ implies the src derivability. ◀

We now record the two scalar refinements applied in the main text.

- **Qutrit Clifford.** The imported presentation of [15] uses an order-6 scalar $(-\omega)$. Our strict qutrit convention uses an order-12 scalar subgroup (Section 3). We refine the source syntax by adjoining an order-12 scalar generator $(\omega_{12})$ and adding the relations

$$(\omega_{12})^{12} = \text{id}_0, \quad (\omega_{12})^{10} = (-\omega).$$

This is the $\mu_6 \to \mu_{12}$ refinement referenced in Section 4.1.

- **Clifford+CS.** The imported presentation of [4] uses an order-4 scalar $(i)$, whereas our strict qubit convention uses an order-8 scalar subgroup. We refine the source syntax by adjoining an order-8 scalar generator $(\omega_*)$ and adding the relations

$$(\omega_8)^8 = \text{id}_0, \quad (\omega_8)^2 = (i).$$

This is the $\mu_4 \to \mu_8$ refinement referenced in Section 4.1.

In both cases, the hypotheses of Lemma 52 are satisfied for the unitary semantics considered in this paper (invertibility is automatic, visible scalars are finite cyclic by construction, and the imported fragments do not exhibit hidden phases relative to their chosen scalar conventions). Therefore, scalar refinement preserves faithfulness, and the refined imported presentations may be treated as complete presentations for the strict semantics used throughout.
<table><caption>Table 3 Encoding/decoding pairs used in the completeness transfer arguments. For the qutrit Clifford and Clifford+CS rows, the “src” presentation is the scalar-refined one (cf. Lemma 52). Convention: omitted generators are fixed by $E_{•}$ and $D_{•}$.</caption><thead><tr><th>Fragment</th><th>Encoding E<sub>•</sub> (new → src)</th><th>Decoding D<sub>•</sub> (src → new)</th></tr></thead><tbody><tr><td>Cliff, RCliff</td><td>E<sub>•</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div></td><td>D<sub>•</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div></td></tr><tr><td>CliffT</td><td>E<sub>CliffT</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div></td><td>D<sub>CliffT</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div><br>D<sub>CliffT</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div></td></tr><tr><td>Cliff3</td><td>E<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>4</sup><sub>12</sub>)<br>E<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>3</sup><sub>12</sub>)<br>E<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>1</sup><sub>12</sub>)<br>D<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>4</sup><sub>12</sub>)<br>D<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>9</sup><sub>12</sub>)<br>D<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>1</sup><sub>12</sub>)<br>D<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>10</sup><sub>12</sub>)</td><td>D<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>2</sup><sub>12</sub>)<br>D<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>9</sup><sub>12</sub>)<br>D<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>1</sup><sub>12</sub>)<br>D<sub>Cliff3</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>10</sup><sub>12</sub>)</td></tr><tr><td>CliffCS</td><td>E<sub>CliffCS</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>8</sup>)<br>E<sub>CliffCS</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>8</sup>)</td><td>D<sub>CliffCS</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>7</sup>)<br>D<sub>CliffCS</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>8</sup>)<br>D<sub>CliffCS</sub>(<div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>) = <div style="display: flex; align-items: center; justify-content: center;"><span style="font-size: 2em; line-height: 1;">|</span><span style="font-size: 2em; line-height: 1;">&harr;</span><span style="font-size: 2em; line-height: 1;">|</span></div>(ω<sup>8</sup>)</td></tr></tbody></table>
<table><thead><tr><th>Interpretation</th><th>Cliff</th><th>Real Cliff</th><th>Qutrit Cliff</th><th>Cliff+T</th><th>Cliff+CS</th><th>CNOT-dih</th><th>Arity</th></tr></thead><tbody><tr><td>?(ω<sup>8</sup>)</td><td>(ω<sup>8</sup>)</td><td>—</td><td>—</td><td>(ω<sup>8</sup>)</td><td>(ω<sup>8</sup>)</td><td>(ω<sup>8</sup>)</td><td>0</td></tr><tr><td>?(ω<sup>12</sup>)</td><td>—</td><td>(-2)</td><td>—</td><td>—</td><td>—</td><td>—</td><td>0</td></tr><tr><td>?{H}</td><td>(H<sup>2</sup>)</td><td>(H<sup>2</sup>)</td><td>(H<sup>4</sup>)</td><td>(H<sup>2</sup>)</td><td>(H<sup>2</sup>)</td><td>—</td><td>1</td></tr><tr><td>?{S}</td><td>(S<sup>4</sup>)</td><td>—</td><td>(S<sup>3</sup>)</td><td>—</td><td>(S<sup>4</sup>)</td><td>—</td><td>1</td></tr><tr><td>?{Z}</td><td>—</td><td>(Z<sup>2</sup>)</td><td>—</td><td>—</td><td>—</td><td>—</td><td>1</td></tr><tr><td>?{T}</td><td>—</td><td>—</td><td>—</td><td>(T<sup>8</sup>)</td><td>—</td><td>(T<sup>8</sup>)</td><td>1</td></tr><tr><td>?{X}</td><td>—</td><td>—</td><td>—</td><td>—</td><td>—</td><td>(X<sup>2</sup>)</td><td>1</td></tr><tr><td>#{H}<sub>2</sub></td><td>(E)</td><td>—</td><td>(E)</td><td>(E)</td><td>(E)</td><td>—</td><td>1</td></tr><tr><td>#{ω<sup>8</sup>}<sub>2</sub></td><td>—</td><td>(F)</td><td>—</td><td>—</td><td>—</td><td>(TX)</td><td>1</td></tr><tr><td>#{H, ω<sup>8</sup>}<sub>2</sub></td><td>—</td><td>—</td><td>—</td><td>(TX)</td><td>—</td><td>—</td><td>1</td></tr><tr><td>#{X}<sub>2</sub></td><td>—</td><td>—</td><td>—</td><td>—</td><td>—</td><td>(XC)</td><td>1</td></tr><tr><td>[S] &rarr; [S, X]</td><td>—</td><td>—</td><td>(SS')<sup>a)</sup></td><td>—</td><td>—</td><td>—</td><td>1</td></tr><tr><td>?{⊕}</td><td>(CPh)</td><td>(CX<sup>2</sup>)</td><td>(CPh)</td><td>(CPh)</td><td>(CPh)</td><td>(CPh)</td><td>2</td></tr><tr><td>#{○}<sub>2</sub></td><td>(B)</td><td>(B)</td><td>(B)</td><td>(B)</td><td>(B)</td><td>(B)</td><td>2</td></tr><tr><td>#{⊕, ○}<sub>2</sub></td><td>(CZ)</td><td>—</td><td>—</td><td>(CZ)</td><td>—</td><td>—</td><td>2</td></tr><tr><td>#{S}<sub>3</sub></td><td>—</td><td>—</td><td>(CZ)</td><td>—</td><td>—</td><td>—</td><td>2</td></tr><tr><td>#{Z}<sub>2</sub></td><td>—</td><td>(ZC)</td><td>—</td><td>—</td><td>—</td><td>—</td><td>2</td></tr><tr><td>[Z] &rarr; —</td><td>—</td><td>(CF)</td><td>—</td><td>—</td><td>—</td><td>—</td><td>2</td></tr><tr><td>[H] &rarr; —</td><td>—</td><td>(CZr)</td><td>—</td><td>—</td><td>—</td><td>—</td><td>2</td></tr><tr><td>#{⊕}<sub>2</sub></td><td>—</td><td>—</td><td>(KC)</td><td>—</td><td>—</td><td>—</td><td>2</td></tr><tr><td>#{S, H}<sub>2</sub></td><td>—</td><td>—</td><td>—</td><td>—</td><td>(XCS)</td><td>—</td><td>2</td></tr><tr><td>⊕ &rarr; ⊕<br>⊕ &rarr; ⊕<br>⊕ &rarr; ⊕</td><td>—</td><td>—</td><td>—</td><td>—</td><td>(CSr)</td><td>—</td><td>2</td></tr><tr><td>#{T, ω<sup>8</sup>, ω<sup>8</sup>}<sub>8</sub></td><td>—</td><td>—</td><td>—</td><td>—</td><td>(CE)</td><td>—</td><td>2</td></tr><tr><td></td><td></td><td></td><td></td><td></td><td></td><td>(ZC)</td><td>2</td></tr><tr><td>arg det<sub>3</sub></td><td>(I)</td><td>(I)</td><td>—</td><td>—</td><td>(I)</td><td>—</td><td>3</td></tr><tr><td>#{⊕, ○}<sub>2</sub></td><td>—</td><td>—</td><td>—</td><td>—</td><td>—</td><td>(I)</td><td>3</td></tr><tr><td>#{T, ω<sup>8</sup>, ω<sup>8</sup>}<sub>4</sub></td><td>—</td><td>—</td><td>—</td><td>—</td><td>—</td><td>(C<sup>2</sup>T)</td><td>3</td></tr><tr><td>arg det<sub>4</sub></td><td>—</td><td>—</td><td>—</td><td>—</td><td>—</td><td>(C<sup>3</sup>T)</td><td>4</td></tr></tbody></table>

a) See Proposition 40.

<caption>Figure 11 Summary of minimality interpretations across all fragments</caption>
$$ (\omega_8^S) = \text{[]}(C1) \quad \text{H} \text{H}^- = \text{---}(C2) \quad \text{S} \text{S}^- \text{S} \text{S}^- = \text{---}(C3) $$

$$ \text{S} \text{H} \text{S} \text{H} \text{S} \text{H}^- = (\omega_8) \quad \text{---}(C4) \quad \text{H} \text{H}^- = \text{---}(C5) $$

$$ \text{S}^- \text{S}^- = \text{---}(C6) \quad \text{S}^- \text{S}^- = \text{---}(C7) $$

$$ \text{H} \text{S} \text{S} \text{H}^- = \text{---}(C8) \quad \text{H} \text{S} \text{S} \text{H}^- = \text{---}(C8) $$

$$ \text{H} \text{S} \text{S} \text{H}^- = \text{---}(C9) \quad \text{H} \text{S} \text{S} \text{H}^- = \text{---}(C9) $$

$$ \text{H}^- \text{H}^- = (\omega_8^\dagger) \text{---}(C10) \quad \text{S}^- \text{H}^- \text{S}^- \text{H}^- = \text{---}(C10) $$

$$ \text{H}^- \text{H}^- = (\omega_8^\dagger) \text{---}(C11) \quad \text{S}^- \text{H}^- \text{S}^- \text{H}^- = \text{---}(C12) $$

$$ \text{H}^- \text{H}^- \text{H}^- \text{H}^- = \text{---}(C13) \quad \text{H}^- \text{H}^- \text{H}^- \text{H}^- = \text{---}(C13) $$

$$ \text{H}^- \text{H}^- \text{H}^- \text{H}^- = \text{---}(C14) \quad \text{H}^- \text{H}^- \text{H}^- \text{H}^- = \text{---}(C14) $$

$$ \text{H}^- \text{H}^- \text{H}^- \text{H}^- = \text{---}(C15) \quad \text{H}^- \text{H}^- \text{H}^- \text{H}^- = \text{---}(C15) $$

$$ \mathcal{X} = \text{---}(S) $$

<caption>■ **Figure 12** Set of relations Cliff<sub>2</sub><sup>source</sup>. Equations (C<sub>i</sub>) are the ones of the complete set of relations for the pro considered in [19].</caption>
$$ \circled{0} = \llbracket \circled{0} \rrbracket \quad (\text{R1}) $$

$$ \boxed{\phantom{H}} \boxed{\phantom{H}} = \boxed{\phantom{H}} \quad (\text{R2}) $$

$$ \boxed{H} \boxed{H} = \boxed{\phantom{H}} \quad (\text{R3}) $$

$$ \boxed{Z} \boxed{H} \boxed{Z} \boxed{H} \boxed{Z} \boxed{H} \boxed{Z} \boxed{H} = \circled{0} \quad (\text{R4}) $$

$$ \boxed{\phantom{H}} \boxed{\phantom{H}} = \boxed{\phantom{H}} \quad (\text{R5}) $$

$$ \boxed{Z} \boxed{\phantom{H}} = \boxed{\phantom{H}} \quad (\text{R6}) $$

$$ \boxed{\phantom{H}} \boxed{Z} = \boxed{\phantom{H}} \quad (\text{R7}) $$

$$ \boxed{H} \boxed{Z} \boxed{H} = \boxed{\phantom{H}} \boxed{Z} \boxed{H} \quad (\text{R8}) $$

$$ \boxed{H} \boxed{Z} \boxed{H} = \boxed{\phantom{H}} \boxed{Z} \boxed{H} \quad (\text{R9}) $$

$$ \boxed{H} \boxed{H} = \boxed{\phantom{H}} \boxed{H} \quad (\text{R10}) $$

$$ \boxed{H} \boxed{H} = \boxed{\phantom{H}} \boxed{Z} \quad (\text{R11}) $$

$$ \boxed{H} \boxed{H} \boxed{H} = \boxed{\phantom{H}} \boxed{H} \boxed{H} \boxed{H} \quad (\text{R12}) \qquad \boxed{\phantom{H}} \boxed{H} = \boxed{\phantom{H}} \quad (\text{R13}) $$

$$ \boxed{H} \boxed{H} \boxed{H} \boxed{H} = \boxed{\phantom{H}} \boxed{H} \boxed{H} \boxed{H} \boxed{H} \quad (\text{R14}) $$

$$ \boxed{H} \boxed{H} \boxed{H} \boxed{H} = \boxed{\phantom{H}} \boxed{H} \boxed{H} \quad (\text{R15}) $$

$$ \boxed{H} \boxed{H} \boxed{H} \boxed{H} = \boxed{\phantom{H}} \boxed{H} \boxed{H} \quad (\text{R16}) $$

$$ \mathcal{X} = \boxed{H} \boxed{H} \boxed{H} \boxed{H} \quad (S) $$

<caption>■ **Figure 13** Set of relations RCliff<sub>2</sub><sup>source</sup>. Equations (R<sub>i</sub>) are the ones of the complete set of relations for the pro considered in [17].</caption>
$$ (\omega_8^S) = \text{[]}(C3) \quad \text{H-H-} = \text{---}(C4) \quad \text{S-S-S-S-} = \text{---}(C5) $$

$$ \text{S-H-S-H-S-H-} = (\omega_8) \quad \text{---}(C6) \quad \text{S-} = \text{---T}^2 \quad (C14) $$

$$ \text{---T-X-} = \text{---X-T}\dagger \quad (\omega_8) \quad \text{C15} \quad \text{[]--} = \text{---}(C7) $$

$$ \text{---S-} = \text{---S-} \quad (C8) $$

$$ \text{---S-} = \text{---S-} \quad (C9) $$

$$ \text{---H-S-S-H-} = \text{---H-S-S-H-} \quad (C10) $$

$$ \text{---H-S-S-H-} = \text{---H-S-S-H-} \quad (C11) $$

$$ \text{---H-} = (\omega_8^\dagger) \quad \text{---S-H-S-H-S-} \quad (C12) $$

$$ \text{---H-} = (\omega_8^\dagger) \quad \text{---S-H-S-H-S-} \quad (C13) $$

$$ \text{---T-} = \text{---T-} \quad (C16) $$

$$ \text{---H-H-T-} = \text{---H-H-T-} \quad (C17) $$

$$ \text{---T-H-T}\dagger \text{---T-H-T}\dagger = \text{---T-H-T}\dagger \text{---T-H-T}\dagger \quad (C18) $$

$$ \text{---T-H-T-H}\dagger \text{---T-H-T}\dagger \text{---T-H}\dagger \text{---T-H}\dagger = \text{---T-H}\dagger \text{---T-H}\dagger \text{---T-H}\dagger \quad (C19) $$

$$ \text{---H-T-H-} = \text{---H-T-H-} \quad (C20) $$

$$ \mathcal{X} = \text{---H-H-H-} \quad (S) $$

<caption>■ **Figure 15** Set of relations CliffT<sub>2</sub><sup>source</sup> on two qubits. Equations (C<sub>i</sub>) are the ones of the complete set of relations for the pro considered in [3].</caption>
$$ \textcircled{4} = \textcircled{3} \quad (\text{C1}) \quad \boxed{K^2} = \textcircled{3} \quad (\text{C2}) \quad \boxed{S} \boxed{S} \boxed{S} \boxed{S} = \textcircled{3} \quad (\text{C3}) $$

$$ \boxed{S} \boxed{K} \boxed{S} \boxed{K} \boxed{S} \boxed{K} = \textcircled{3} \quad (\text{C4}) \quad \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} = \textcircled{3} \quad (\text{C5}) $$

$$ \boxed{S} \boxed{\phantom{S}} = \boxed{S} \boxed{\phantom{S}} \quad (\text{C6}) \quad \boxed{S} \boxed{\phantom{S}} = \boxed{S} \boxed{\phantom{S}} \quad (\text{C7}) $$

$$ \boxed{K} \boxed{Z} \boxed{K} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{K} \boxed{Z} \boxed{K} \quad (\text{C8}) $$

$$ \boxed{K} \boxed{Z} \boxed{K} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{K} \boxed{Z} \boxed{K} \quad (\text{C9}) $$

$$ \boxed{S} \boxed{K} \boxed{K} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{K} \boxed{S} \quad (\text{C10}) $$

$$ \boxed{S} \boxed{K} \boxed{K} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{K} \boxed{S} \quad (\text{C11}) \quad \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{S} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{S} \quad (\text{C12}) $$

$$ \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \quad (\text{C13}) $$

$$ \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \quad (\text{C14}) $$

$$ \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \quad (\text{C15}) $$

$$ \boxed{K} \boxed{K} \boxed{K} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{K} \boxed{K} \boxed{K} \quad (\text{C16}) $$

$$ \boxed{K} \boxed{K} \boxed{K} = \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{\phantom{S}} \boxed{K} \boxed{K} \boxed{K} \quad (\text{C17}) $$

$$ \mathcal{X} = \boxed{K} \boxed{K} \boxed{K} \boxed{K} \textcircled{4} \quad (\text{B}) $$

<caption>■ **Figure 16** Set of relations CliffCS<sub>2</sub><sup>source</sup> on three qubits. Equations (C<sub>i</sub>) are the ones of the complete set of relations for the pro considered in [4].</caption>
$$ \overline{\text{X}}\text{X} = \text{---} \quad \text{(R1)} \qquad \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{(R2)} \qquad \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{(R3)} $$

$$ \text{---}\text{---}\text{---}\text{---} = \text{---} \quad \text{(R4)} \qquad \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} = \mathcal{X} \quad \text{(R5)} $$

$$ \text{---}\text{---}\text{---}\text{---} = \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{(R6)} \qquad \overline{\text{X}}\text{X} = \text{---} \quad \text{(R7)} $$

$$ \text{---}\text{---}\text{---}\text{---} = \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{(R8)} \qquad \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} = \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{(R9)} $$

$$ \overline{\omega_8}^{\otimes 8} = \text{[]}(R10) \qquad \overline{\text{X}}\text{\texttt{[}}\text{\texttt{X}}\text{\texttt{[}}\text{\texttt{X}}\text{\texttt{]} = \overline{\omega_8} \text{---}\texttt{T}^7 \quad \text{(R11)} \qquad \text{---}\text{---}\text{---}\text{---}\text{---} = \text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{(R12)} $$

$$ \text{---}\text{---}\text{---}\text{---} = \text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---}\text{---} \quad \text{(R13)} $$

<caption>■ **Figure 17** Set of relations CNOTdihe₂<sup>source</sup> [1].</caption>