# Polycontrolled PROPs for Qudit Circuits: A Uniform Complete Equational Theory For Arbitrary Finite Dimension

Colin Blake

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

## To cite this version:

Colin Blake. Polycontrolled PROPs for Qudit Circuits: A Uniform Complete Equational Theory For Arbitrary Finite Dimension. 2026. [https://hal.science/hal-05503323v1](https://hal.science/hal-05503323v1)

HAL Id: hal-05503323

[https://hal.science/hal-05503323v1](https://hal.science/hal-05503323v1)

Preprint submitted on 10 Feb 2026

**HAL** is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Polycontrolled PROPs for Qudit Circuits: A Uniform Complete Equational Theory For Arbitrary Finite Dimension

Colin Blake

Université de Lorraine, CNRS, INRIA, LORIA

Nancy, France

colin.blake@inria.fr

## Abstract

We present a finite schematic axiomatisation of quantum circuits over $d$-level systems (qudits), uniform in every finite dimension $d \ge 2$. For each $d$ we define a PROP $CQC_d$ equipped with a family of control functors, treating control as a primitive categorical constructor. Using a translation between qudit circuits and the LOPP calculus for linear optics based on $d$-ary Gray codes, we obtain for each $d$ a finite set of local axiom schemata $QC_d$ that is sound and complete for unitary $d$-level circuits: two circuits denote the same unitary if and only if they are inter-derivable using axioms involving at most three wires. The generators are compatible with standard universal qudit gate families, yielding a sound equational basis for circuit rewriting and optimisation-by-rewriting. Conceptually, this extends the qubit circuit completeness results of Clément et al. to arbitrary finite dimension, and instantiates the control-as- constructor approach of Delorme and Perdrix in this setting, while keeping the axiom shapes uniform in $d$.

## Keywords

Qudit circuits, Polycontrolled PROPs, controlled quantum circuits, equational theories, categorical quantum mechanics

## 1 Introduction

Quantum circuits provide a standard low-level syntax for finite- dimensional quantum computation: wires carry $d$-level quantum data, boxes represent unitary gates, and a circuit denotes a unitary operator on the tensor power $(\mathbb{C}^d)^{\otimes n}$ [15, 24]. Accordingly, they serve as the basic representation both for algorithm design and for hardware-aware compilation and verification; in this setting, optimisation is typically justified via equational circuit rewriting. Moreover, correctness arguments in verification and compilation are routinely phrased as local diagrammatic rewrites, closed under both sequential and parallel composition. Consequently, from a logical perspective, this raises a foundational completeness ques- tion: can equality of unitary circuits be axiomatised by a *finite*, syntax-directed equational theory in the circuit PROP?

In the PROP formalism (a strict symmetric monoidal category whose objects are wire counts) such a theory is given by a finite set of local rewrite schemata between circuit diagrams, closed under both sequential and parallel composition. For qubits ($d = 2$), complete circuit-level axiomatisations are already known [6, 8, 9]. A key lesson from this line of work is the central role of control. If control is not treated as primitive, then completeness forces axiom schemata that quantify over arbitrarily many control wires. By contrast, treating control functorially in a controlled PROP yields finite, bounded-arity axiom sets [14, 17].

Meanwhile, graphical calculi such as ZX/ZH/ZW admit complete equational theories for broad classes of qubit processes [1, 4, 5, 11, 19, 28]. However, these languages describe general linear maps rather than circuit-level unitaries; moreover, extracting circuits can be non-local—and, indeed, hard in general [12]. This motivates circuit-specific rewrite systems.

For $d > 2$, many platforms support native $d$-level systems (qudits); consequently, qudit-native design and compilation can reduce resource counts or exploit non-binary structure in gate libraries and higher-dimensional circuit design [20, 25, 27, 31]. From an equational perspective, several diagrammatic and circuit formalisms for qudits have been proposed. Qudit and “qufinite” variants of the ZX- and ZH-calculi provide universal graphical languages parameterised by the dimension; moreover, they admit completeness results in some settings [30, 33]. More recently, qufinite ZXW-calculi, together with finite-dimensional ZX and ZW calculi, have yielded complete equational theories for the whole of finite-dimensional Hilbert spaces, uniformly in $d$ [13, 26, 34]. These results are foundationally powerful; nevertheless, they operate at the level of arbitrary linear maps and therefore do not directly yield bounded-arity PROP presentations of a circuit language for unitary gates with a native control constructor. At the circuit level, by contrast, completeness results are largely fragmentary. There are complete rewrite systems for specific subtheories, notably for qutrit stabiliser quantum mechanics in ZX and, more recently, for multi-qutrit Clifford circuits [20]. Beyond ZX-style diagrammatics, further work has developed graphical calculi for multi-qudit computations based on generalised Clifford algebras and related algebraic structures [21, 22]. However, these approaches either target broad classes of linear maps (rather than a circuit syntax for unitary gates), focus on particular fragments, or treat only fixed small dimensions. Consequently, they do not provide a finite, uniform-in-$d$ PROP presentation of the circuit category whose objects are wire arities and whose morphisms are unitary $d$-level circuits over a fixed universal gate signature, with axioms given by local schemata of bounded wire arity.

There is no dimension-uniform finitary presentation of unitary qudit circuits satisfying the following combination of requirements. Namely, for each $d \ge 2$, one seeks a sound and complete finite set of circuit-specific axiom schemata for the PROP of unitary $d$-level circuits over a fixed universal gate signature, with axioms given by local schemata of bounded wire arity and schematic form independent of $d$. This contrasts with the qubit case [6, 8, 9, 14] and, as a result, leaves qudit equational reasoning without a uniform completeness theory. Moreover, beyond foundational interest, the absence of such a fixed rewrite system makes it harder to justify rewriting-based optimisation and verification of native qudit circuits without resorting to ad hoc matrix calculations.
At a high level, we treat control as a primitive operation in a polycontrolled PROP. Control is fundamental in circuit design and compilation: given a subcircuit $f: n \to n$, one forms a controlled version by adjoining a new wire and applying $f$ conditionally; importantly, this construction must be coherent with sequential composition and wire permutations. Rather than treating each controlled-$U$ gate as an ad hoc derived primitive, we build control directly into the categorical structure itself [14, 17]. Concretely, we equip the circuit language with a family of control functors $(C_k)_{k=0}^{d-1}$. Each $C_k$ sends an endomorphism $f: n \to n$ to an endomorphism $C_k(f): 1+n \to 1+n$, which applies $f$ exactly when the added control qudit is in computational basis state $|k\rangle$ (and otherwise acts as the identity on the targets). Multi-controlled operations are obtained systematically by iterating these functors. Treating control as a first-class constructor is what makes bounded-arity axioms possible: local schemata can refer to $C_k(-)$ itself, rather than quantifying over arbitrarily many explicit control wires.

**Main result.** For each finite $d \ge 2$, we define a polycontrolled circuit PROP $CQC_d$. Moreover, we introduce a finite equational theory $QC_d$ generated by local axiom schemata whose schematic form is uniform in $d$ and whose instance involve at most three wires. Theorem 4.19 states that $QC_d$ is sound and complete for the standard unitary semantics $[[\cdot]]: CQC_d \to Qudit_d$: for any $n$-qudit circuits $C_1, C_2: n \to n$,

$$[[C_1]] = [[C_2]] \iff QC_d \vdash C_1 = C_2$$

Here, “uniformity” has three aspects: (i) bounded wire arity; (ii) a fixed, finite list of axiom schema families whose diagrammatic shape does not depend on $d$; and (iii) only indices (in $[d]$) vary with $d$.

Our completeness proof proceeds by reduction to the linear-optical calculus **LOPP**. In particular, following Clément et al. [8], we transfer completeness from **LOPP** [7, 18]. Using a reflected $d$-ary Gray code, we encode an $n$-qudit circuit as a $d^n$-mode single-photon linear-optical circuit. This encoding preserves the intended unitary semantics, up to conjugation by a fixed Gray-code basis permutation. A key technical point is that $CQC_d$ and **LOPP** interpret $\otimes$ differently (tensor product versus direct sum under single-photon semantics). Consequently, the translation cannot be strictly monoidal; instead, we fix a deterministic serialisation of $\otimes$ and prove an encoding/decoding retraction. We then transport completeness of **LOPP** back to $CQC_d$ via decoding and a “mimicking” argument. When $d=2$, the reflected $d$-ary Gray code specialises to the binary reflected Gray code; correspondingly, our reduction to **LOPP** recovers the qubit-level completeness-transfer pattern of [8].

For each finite $d \ge 2$ we obtain:

(1) A polycontrolled circuit PROP. We define the endomorphism PROP $CQC_d$ of $d$-level unitary circuits, equipped with control functors $(C_k)_{k=0}^{d-1}$ whose iteration yields multi-controlled operations.

(2) A finite bounded-arity axiom system. We present a finite set of local axiom schemata $QC_d$ (each instance uses at most three wires) of schematic form uniform in $d$, and show that it is sound and complete for unitary $d$-level circuit equality. This yields a fixed, syntax-directed rewrite system suitable as a foundation for rewriting-based optimisation and verification of native qudit circuits.

(3) A completeness transfer via Gray-code embedding. Using a $d$-ary Gray code, we encode $n$-qudit circuits as $d^n$-mode **LOPP** circuits and decode **LOPP** derivations back into $CQC_d$, yielding a modular completeness proof via [7, 18].

(4) Expressing standard qudit gate families. Our generators and axioms express adjacent two-level gates and basis-controlled phases. Consequently, one can assemble common universal qudit gate families (as recalled in §2.4). This keeps the presentation circuit-level and dimension-uniform, whilst remaining compatible with standard synthesis practice.

Throughout, we work with exact unitary equality: global phases are not quotiented away and therefore appear as scalar $(0 \to 0)$ morphisms. Our goal is a circuit-specific presentation of the PROP of unitary circuits over a fixed signature; unlike the uniform-in-$d$ completeness results for finite-dimensional ZX-/ZW-/ZXW-calculi [13, 26, 34], we do not aim to axiomatise arbitrary linear maps.

The paper is organised as follows. Section 2 defines $CQC_d$ and its unitary semantics; Section 3 presents the axiom schemata generating $QC_d$; and Section 4 give the Gray-code translation to **LOPP** and the completeness transfer culminating in Theorem 4.19.

## 2 Qudit circuits as a polycontrolled PROP

In this section we set up the circuit language used throughout this work. Fix a dimension $d \ge 2$. Our goal is to work in a circuit-level setting: objects are wire counts, morphisms are unitary $d$-level circuits, and circuit equality will ultimately be captured by a finite, local axiom system. The key design choice is that control is primitive. Rather than treating each controlled gate as a separate derived gadget, we build control into the categorical structure: for every computational basis value $k \in [d]$ we have a constructor $C_k(-)$ that turns a circuit $f: n \to n$ into its $k$-controlled version $C_k(f): 1+n \to 1+n$. Multi-controlled operations are then obtained simply by iterating $C_k$.

### 2.1 PROPs and (poly)controlled PROPs

We work in a strict symmetric monoidal setting, so wire counts form the objects, parallel composition is strictly associative, and diagrams are taken modulo the strict coherence laws.

**Definition 2.1** ([23]). A PROP $P$ is a strict symmetric monoidal category whose objects are the natural numbers, generated by a distinguished object 1 with tensor $m \otimes n = m + n$ and unit object 0.

We write $P(m, n)$ for the hom-set $m \to n$. Composition is written $\circ$, tensor (parallel composition) as $\otimes$, and $\sigma_{m,n}: m+n \to n+m$ denotes the symmetry (wire swap).

Since our circuits are unitary, we only consider endomorphisms. For a PROP $P$, write $P_{\text{endo}}$ for its wide endomorphism subcategory: $P_{\text{endo}}(n, n) = P(n, n)$ and $P_{\text{endo}}(m, n) = \emptyset$ for $m \ne n$.

A permutation is any morphism $\pi: n \to n$ obtained from identities and symmetries $\sigma_{m,n}$ using only $\circ$ and $\otimes$. Such morphisms are canonically invertible; we write $\pi^{-1}$ for the inverse permutation.

Informally, “adding a control” is an operation that, given an endomorphism $f: n \to n$, produces an endomorphism on one additional wire that applies $f$ conditionally. Categorically, we package this
The raw syntax carries more parentheses and wiring bookkeeping than we want to treat as meaningful. We therefore quotient by the least congruence that forces: (i) the strict PROP laws; and (ii) the axioms saying that each $C_k$ really is a control functor.

**Definition 2.6.** Let $\equiv$ be the least congruence on $\mathbf{CQC}_d^{\text{raw}}$—that is, an equivalence relation on each $\mathbf{CQC}_d^{\text{raw}}(n, n)$, closed under all contexts built from $\circ$, $\otimes$, and each $C_k$, that contains all well-typed instances of:

* the strict PROP equations [23] (associativity/unit for $\circ$ and $\otimes$, interchange, symmetry naturality and involutivity); and

* for each $k \in [d]$, the functoriality and coherence equations for $C_k$ from Definition 2.2: $C_k(\text{id}_n) \equiv \text{id}_{1+n}$, $C_k(D \circ C) \equiv C_k(D) \circ C_k(C)$, and the coherence schemata (1)-(3) (with $\pi$ ranging over permutation terms).

Thus $C \equiv C'$ means that $C$ and $C'$ differ only by the PROP coherence and by the coherence laws that make each $C_k$ a well-behaved control constructor. No gate-specific equations are imposed here; those enter later via the equational theory $\mathbf{QC}_d$.

**Definition 2.7.** Define the endomorphism PROP $\mathbf{CQC}_d$ by

$$ \mathbf{CQC}_d(n, n) := \mathbf{CQC}_d^{\text{raw}}(n, n) / \equiv, \quad \mathbf{CQC}_d(m, n) := \emptyset \text{ if } m \neq n, $$

with $\circ$ and $\otimes$ induced by the term constructors on representatives, and with symmetry $\sigma_{m,n}$ induced by the corresponding raw permutation terms.

Write $[-] := \mathbf{CQC}_d^{\text{raw}}(n, n) \to \mathbf{CQC}_d(n, n)$ for the quotient map. By construction, each $C_k$ respects $\equiv$ and therefore descends to an endofunctor on $(\mathbf{CQC}_d)_{\text{endo}}$ satisfying Definition 2.2. We call $(\mathbf{CQC}_d, (C_k)_{k=0}^{d-1})$ the polycontrolled PROP of d-level quantum circuits.

## 2.3 Qudit semantics

We now fix the intended semantics: circuits denote unitaries on $(\mathbb{C}^d)^{\otimes n}$. Fix $d \ge 2$ and recall $[d] := \{0, 1, \dots, d-1\}$. Let $\mathbb{C}^d$ be the d-dimensional Hilbert space with computational basis $\{|0\rangle, \dots, |d-1\rangle\}$. For $n \ge 0$, set $\mathcal{H}_n := (\mathbb{C}^d)^{\otimes n} \cong \mathbb{C}^{d^n}$, with basis $\{|x\rangle \mid x \in [d]^n\}$, and write $I_{\mathcal{H}_n}$ for the identity on $\mathcal{H}_n$.

Recall that $U : \mathcal{H}_n \to \mathcal{H}_n$ is unitary if $U^\dagger U = UU^\dagger = I_{\mathcal{H}_n}$, equivalently $U^{-1} = U^\dagger$. We write $U(N) := \{U \in \mathbb{C}^{N \times N} \mid U^\dagger U = UU^\dagger = I_N\}$.

**Definition 2.8.** Let $\mathbf{Qudit}_d$ be the endomorphism PROP defined by the hom-sets

$$ \mathbf{Qudit}_d(n, n) := U(d^n), \quad \mathbf{Qudit}_d(m, n) := \emptyset \text{ if } m \neq n, $$

where we identify $\mathcal{H}_n \cong \mathbb{C}^{d^n}$ via the computational basis. Composition is ordinary composition of linear maps (matrix multiplication), tensor on morphisms is the tensor product of operators, and the symmetry $\sigma_{m,n}: m+n \to n+m$ is the swap unitary determined by

$$ \sigma_{m,n}(|x\rangle \otimes |y\rangle) := |y\rangle \otimes |x\rangle \quad (x \in [d]^m, y \in [d]^n). $$

In particular, $\mathbf{Qudit}_d(0, 0) \cong U(1) = \{z \in \mathbb{C} \mid |z| = 1\}$ consists of global phases.

Given any unitary $U \in \mathbf{Qudit}_d(n, n)$ and a basis value $k \in [d]$, define its $k$-controlled extension $C_k(U) \in \mathbf{Qudit}_d(n+1, n+1)$ by

$$ C_k(U) := |k\rangle \langle k| \otimes U + \sum_{t \in [d], t \neq k} |t\rangle \langle t| \otimes I_{\mathcal{H}_n}. \quad (4) $$

Semantically, $C_k(U)$ applies $U$ to the target register iff the added control qudit is in state $|k\rangle$, and otherwise acts as the identity.

**Definition 2.9.** Define, by structural induction, a family of maps

$$ [[\cdot]] : \mathbf{CQC}_d^{\text{raw}}(n, n) \to \mathbf{Qudit}_d(n, n) \quad (n \in \mathbb{N}) $$

as follows.

* **Generators.** On the generators of $\Sigma_{\mathbf{QC}_d}$ set:

$$ - [[\cdot]] := 1, \quad [[\emptyset]] := e^{i\theta}, \quad [[\cdot]] := \sum_{k \in [d]} |k\rangle \langle k|, $$

$$ - [[\times]] := \sum_{i,j \in [d]} |j,i\rangle \langle i,j|, $$

$$ - [[H^{(r,r+1)}]] := \sum_{k \in [d] \setminus \{r,r+1\}} |k\rangle \langle k| + \frac{1}{\sqrt{2}} (|r\rangle + |r+1\rangle) \langle r| + \frac{1}{\sqrt{2}} (|r\rangle - |r+1\rangle) \langle r+1| $$

* **Sequential and parallel composition.** For raw circuits $C, D$, set

$$ [[D \circ C]] := [[D]] \circ [[C]], \quad [[C \otimes D]] := [[C]] \otimes [[D]]. $$

* **Control.** For $C \in \mathbf{CQC}_d^{\text{raw}}(n, n)$ and $k \in [d]$, set

$$ [[C_k(C)]] := C_k([C]) \in \mathbf{Qudit}_d(1+n, 1+n). \quad (5) $$

**Proposition 2.10.** The interpretation $[[\cdot]] : \mathbf{CQC}_d^{\text{raw}}(n, n) \to \mathbf{Qudit}_d(n, n)$ respects the structural congruence $\equiv$ of Definition 2.6. Hence it factors uniquely through the quotient to a well-defined strict symmetric monoidal functor

$$ [[\cdot]] : \mathbf{CQC}_d \to \mathbf{Qudit}_d, $$

satisfying $[[C] \equiv] = [[C]]$ for every raw circuit $C$.

*PROOF.* The strict PROP equations are respected because $\circ$ is interpreted as composition of linear maps, $\otimes$ as tensor product, and the swap generator as the swap unitary. For control, the functionality of $C_k(-)$ together with (4) yields $[[C_k(\text{id}_n)]] = I_{\mathcal{H}_{n+1}}$ and $[[C_k(D \circ C)]] = [[C_k(D)]] \circ [[C_k(C)]]$. The coherence axioms (1)-(3) hold because $C_k(-)$ acts only on the additional control tensor factor and is therefore insensitive to unused wires and to permutations of the target wires. $\square$

## 2.4 Universality

Fix $d \ge 2$. We now record that our gate signature $\Sigma_{\mathbf{QC}_d}$ is universal for d-level unitary computation: every unitary $U \in U(d^n)$ is denoted by some circuit in $\mathbf{CQC}_d(n, n)$.

We rely on two standard synthesis facts. First, every $2 \times 2$ unitary admits an Euler decomposition in terms of a Hadamard and computational-basis phases [2, 24]: for all $U \in U(2)$ there exist $\theta, \alpha, \beta, \gamma \in \mathbb{R}$ such that

$$ U = e^{i\theta} Z(\alpha) HZ(\beta) HZ(\gamma), $$

where $H \in U(2)$ is the Hadamard and $Z(\phi) = \text{diag}(1, e^{i\phi})$.

Second, $U(d)$ is generated by adjacent two-level unitaries [10, 16, 24, 29]: every $V \in U(d)$ is a product of unitaries, each supported on $\text{span}\{|r\rangle, |r+1\rangle\}$ for some $r \in [d-1]$.

For convenience, define

$$ Z_d^{(j)}(\theta) := [[C_j(\emptyset)]] , \quad H_d^{(r,r+1)} := [[-H^{(r,r+1)}]]. $$

**Lemma 2.11.** Fix $r \in [d-1]$. Let $W \in U(d)$ act as the identity on the orthogonal complement of $\text{span}\{|r\rangle, |r+1\rangle\}$. Then there exists a 1-qudit circuit $C_W \in \mathbf{CQC}_d(1, 1)$ such that $[[C_W]] = W$.
**PROOF.** Restrict $W$ to $\text{span}\{|r\rangle, |r+1\rangle\} \cong \mathbb{C}^2$. By the Euler decomposition, this restriction factors (up to a global phase) as a product of $2 \times 2$ Hadamards and computational-basis phases. Embedding back into $\mathbb{C}^d$, each factor becomes either an adjacent Hadamard $H_d^{(r,r+1)}$, a level-phase $Z_d^{(j)}(\cdot)$, or a global phase. Each is realised by a circuit in $\mathbf{CQC}_d$, and composing them yields $C_W$. $\square$

Define the two-qudit unitary $CZ_d := I_{H_2} - 2|0, 0\rangle\langle 0, 0| \in U(d^2)$. Equivalently, $CZ_d$ sends $|0, 0\rangle \mapsto -|0, 0\rangle$ and fixes all other computational basis states. In $\mathbf{CQC}_d$, $[C_0(C_0(\pi))] = CZ_d$.

We use the standard universality fact that for all $n \ge 0$, arbitrary single-qudit unitaries together with $CZ_d$ generate $U(d^n)$ [3].

**Proposition 2.12.** For every $n \ge 0$, the interpretation map $[\cdot] : \mathbf{CQC}_d(n, n) \to \mathbf{Qudit}_d(n, n) = U(d^n)$ is surjective.

**PROOF.** Let $U \in U(d^n)$.

If $n=0$, then $U \in U(1)$ is a scalar phase $e^{i\theta}$, denoted by $\theta$.

Assume $n \ge 1$. By adjacent two-level generation of $U(d)$, every single-qudit unitary can be written as a product of unitaries supported on $\text{span}\{|r\rangle, |r+1\rangle\}$. By Lemma 2.11, each such factor is realised in $\mathbf{CQC}_d(1, 1)$, hence arbitrary single-qudit unitaries are realised.

Together with $CZ_d$, these single-qudit unitaries generate $U(d^n)$. The gate $CZ_d$ is realised in $\mathbf{CQC}_d$, and the PROP structure (tensoring with identities and permutations) allows placing these realised 1- and 2-qudit circuits on any desired wire(s). Composing the resulting circuits yields some $C \in \mathbf{CQC}_d(n, n)$ with $[C] = U$. $\square$

## 2.5 Equational theories on $\mathbf{CQC}_d$

The PROP $\mathbf{CQC}_d$ quotients raw circuits only by structural bookkeeping: PROP coherence plus the coherence laws of control functions. To reason about genuine circuit identities (e.g. moving phases, rewriting controlled patterns, decomposing swaps), we will work with an additional equational theory $\Gamma$ on $\mathbf{CQC}_d$.

It is useful to keep two notions of equality separate:

* structural equality $C \equiv C'$ on raw syntax (Definition 2.6); and

* content equality generated by extra circuit equations in a chosen equational theory $\Gamma$ on $\mathbf{CQC}_d$.

**Definition 2.13.** An equational theory $\Gamma$ on $\mathbf{CQC}_d$ is a collection of well-typed equations $f = g$ between morphisms of $\mathbf{CQC}_d$.

For such a $\Gamma$, let $(\approx_\Gamma)_n$ be the least family of relations on the hom-sets $\mathbf{CQC}_d(n, n)$ such that:

(1) every axiom $f = g$ in $\Gamma$ satisfies $f \approx_\Gamma g$;

(2) each $\approx_\Gamma$ is an equivalence relation;

(3) $f_1 \approx_\Gamma g_1$ and $f_2 \approx_\Gamma g_2$ imply $f_2 \circ f_1 \approx_\Gamma g_2 \circ g_1$;

(4) $f \approx_\Gamma g$ and $h \approx_\Gamma k$ imply $f \otimes h \approx_\Gamma g \otimes k$;

(5) $f \approx_\Gamma g$ implies $C_k(f) \approx_\Gamma C_k(g)$ for every $k \in [d]$.

We write $\Gamma \vdash f = g$ to mean $f \approx_\Gamma g$. When $C, C'$ are raw terms, the judgement $\Gamma \vdash C = C'$ is shorthand for $\Gamma \vdash [C] = [C']$ in $\mathbf{CQC}_d$. Intuitively, $\Gamma \vdash f = g$ is the congruence closure of $\Gamma$ under sequential composition, parallel composition, and adding controls.

**Definition 2.14.** For each $d \ge 2$, let $\mathbf{QC}_d$ be the equational theory on $\mathbf{CQC}_d$ generated by the axiom schemata displayed in Figures 1 and 2.

We will show in Theorem 4.19 that $\mathbf{QC}_d$ is sound and complete for the unitary semantics $[\cdot] : \mathbf{CQC}_d \to \mathbf{Qudit}_d$. Some schemata in Figures 1–2 use derived-gate abbreviations, defined next in §3.1. Having fixed $\mathbf{CQC}_d$ and its intended semantics, we can now state the finite set of local schemata that axiomatise equality in $\mathbf{CQC}_d$.

# 3 A Finite Axiom System for Qudit Circuits

Fix $d \ge 2$. This section presents the finite set of local axiom schemata that generates our equational theory $\mathbf{QC}_d$ on the circuit PROP $\mathbf{CQC}_d$ (Definition 2.7). These schemata are the non-structural rewrite principles used later in the completeness transfer of Section 4. Throughout, all equations are taken in $\mathbf{CQC}_d$, i.e. modulo the PROP laws and the control-coherence equations already built into $\mathbf{CQC}_d$.

## 3.1 Derived gates used in the axiom schemata

The generators of $\mathbf{CQC}_d$ are the structural PROP circuits, the adjacent two-level Hadamards $[H^{(r,r+1)}] (r \in [d-1])$, the scalar phases $\theta(\theta \in \mathbb{R})$, and the control constructors $C_k(-)$. The axiom schemata in Figures 1–2 are written using a small family of derived one-qudit gates (and derived two-level Hadamards), matching the decoding notation of §4.4. These are purely abbreviations for composite circuits in $\mathbf{CQC}_d$: they introduce no new generators; instead, they package common subcircuits so that the schemata remain readable.

For readability, we present these derived gates in algebraic form in this subsection only. Crucially, symbols such as $H^{(i,j)}$, $X^{(i,j)}$, and $R_x^{(i,j)}(\theta)$ denote morphisms in $\mathbf{CQC}_d$ (i.e. circuit diagrams modulo the structural congruence), not matrices. Only after applying the interpretation functor $[\cdot] : \mathbf{CQC}_d \to \mathbf{Qudit}_d$ do they correspond to the intended unitary operators. We write $H^{(r,r+1)}$ for the adjacent Hadamard generator $[H^{(r,r+1)}]$.

We will use three families of derived one-qudit morphisms (all abbreviations in $\mathbf{CQC}_d$):

(1) $X^{(i,j)}$ for $i, j \in [d]$;

(2) $H^{(i,j)}$ for distinct $i, j \in [d]$;

(3) $R_x^{(i,j)}(\theta)$ for distinct $i, j \in [d]$ and $\theta \in \mathbb{R}$.

For each adjacent pair $(r, r + 1)$ we define the adjacent swap $X^{(r,r+1)}$ by

$$X^{(r,r+1)} := H^{(r,r+1)} \circ C_{r+1}(\pi) \circ H^{(r,r+1)} \quad (6)$$

For notational uniformity, we set $X^{(i,i)} := \text{id}_1$. For distinct $i, j \in [d]$, we define the two-level swap $X^{(i,j)}$ as a composite of adjacent swaps. Assuming $i < j$, set $S_{i,j} := \prod_{k=0}^{j-i-1} X^{(i+k, i+k+1)}$ where $\prod_{k=0}^{m} f_k := f_m \circ \cdots \circ f_0$, then

$$X^{(i,j)} := S_{i+1,j}^{-1} \circ X^{(i,i+1)} \circ S_{i+1,j}, \quad (7)$$

and for $i > j$ set $X^{(i,j)} := X^{(j,i)}$.

We define the two-level Hadamard $H^{(i,j)}$ on levels $(i, j)$ by conjugating an adjacent Hadamard by the corresponding swap that “slides” the relevant level into position. For $i = j$, set $H^{(i,i)} := \text{id}_1$. If $i < j$, set

$$H^{(i,j)} := X^{(j,i+1)} \circ H^{(i,i+1)} \circ X^{(j,i+1)}, \quad (8)$$

and for $i > j$ define the ordered version by swapping the two levels:

$$H^{(i,j)} := X^{(j,i)} \circ H^{(j,i)} \circ X^{(j,i)} \quad (9)$$
Finally, for distinct $i, j \in [d]$ and $\theta \in \mathbb{R}$, we define the two-level beam-splitter rotation $R_x^{(i,j)}(\theta)$ by

$$R_x^{(i,j)}(\theta) := H^{(i,j)} \circ C_i(\underbrace{\theta}_{\theta}) \circ C_j(\overbrace{-\theta}^{\theta}) \circ H^{(i,j)} \quad (10)$$

Under $\llbracket - \rrbracket$, these families act as follows:

* $\llbracket X^{(i,j)} \rrbracket$ swaps $|i\rangle$ and $|j\rangle$ and fixes all other computational basis states.

* $\llbracket H^{(i,j)} \rrbracket$ acts as the usual $2 \times 2$ Hadamard on $\text{span}\{|i\rangle, |j\rangle\}$ (in the ordered basis $(|i\rangle, |j\rangle)$) and as the identity on the orthogonal complement.

* $\llbracket R_x^{(i,j)}(\theta) \rrbracket$ acts on $\text{span}\{|i\rangle, |j\rangle\}$ as $\begin{pmatrix} \cos(\theta) & i \sin(\theta) \\ i \sin(\theta) & \cos(\theta) \end{pmatrix}$ (in the ordered basis $(|i\rangle, |j\rangle)$) and as the identity elsewhere.

To state several families of axioms systematically in $d$, we use a compact meta-notation in circuit diagrams. An indexed box is a dash-dotted rectangle surrounding a subdiagram. It is not part of the raw syntax of Definition 2.5; it abbreviates a finite iterated composite of the enclosed circuit.

An indexed box is annotated by an index variable $k$ together with an optional unary predicate $\varphi(k)$, where $k$ is the only free variable. The intended reading is that $k$ ranges over integers with $0 \le k < d$ that satisfy $\varphi(k)$ (for instance $\varphi(k)$ may be $a \le k < b$, or $k \ne 0$). The box denotes the sequential composite of the enclosed subcircuit, taken in increasing order of $k$:

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

If the predicate is omitted (we write just “$k$”), this abbreviates the default predicate $0 \le k < d$.

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

Note that indexed boxes expand only by sequential composition along the same wires, so they do not increase wire arity (all schemata still involve at most three wires).

## 3.2 The axiom schemata and how to read them

This subsection fixes the axiom schemata generating $QC_d$, and explains the intended roles among them. The rules are presented as local equalities between circuit diagrams; later, we use them to derive the global control-algebra principles (compatibility, commutativity, and exhaustivity) needed for the encoding/decoding arguments.

We define $QC_d$ as the congruence generated by the schematic equations in Figures 1–2 and closed under $\circ$, $\otimes$, and all $C_k$ (Definition 2.13). As always, these are equations in $CQC_d$; they are stated modulo the PROP law and the control functoriality/coherence already built into $CQC_d$.

A useful reading is that Figure 1 collects the one- and two-qudit identities that form the main “gate algebra” of the theory, while Figure 2 supplies the finite gate-level ingredients from which the global control principles of Definition 2.4 become derivable.

We split the non-structural axioms into two groups according to their role in the development.

* Core axioms (Figure 1) form the main algebraic interface of the circuit theory: phase arithmetic, basic two-level identities, the

swap decomposition, and the local decomposition/rotation principles.

* Control-algebra support axioms (Figure 2) are included so that the global control-algebra principles—namely compatibility, commutativity, and exhaustivity from Definition 2.4—are derivable inside $QC_d$, rather than assumed as part of the underlying structure. Concretely, one could strengthen the definition of $CQC_d$ by quotienting the raw syntax additionally by compatibility, commutativity and exhaustivity of control (or by taking these as global rewrite schemata). We deliberately do not do this: these principles are semantically sound for the intended projector-based control interpretation, but they are not consequences of control functoriality alone. Keeping them out of the structural congruence makes the ambient PROP $CQC_d$ conservative, and ensure that the completeness theorem is genuinely a statement about what follows from the finite axiom set $QC_d$.

## 3.3 Derived control-algebra laws

The three control-algebra equations of Definition 2.4 are derivable in the circuit PROP $CQC_d$ from the axiom system $QC_d$. The proofs are purely syntactic and are deferred to Appendices C, D and E. The present subsection records the results and the common reduction step used throughout.

**Lemma 3.1.** Every morphism of $CQC_d$ is provably equal in $QC_d$ to a circuit generated (using only sequential and parallel composition) by

$$ \mathcal{G} = \{\text{id}_n \mid n \in \mathbb{N}\} \cup \{\underbrace{(\theta)}_{\theta} \mid \theta \in \mathbb{R}\} \cup \{-\underbrace{H^{(i,j)}}_{H^{(i,j)}} \mid 0 \le i < j < d\} \\ \cup \{C_k(\underbrace{(\theta)}_{\theta}) \mid k \in [d], \theta \in \mathbb{R}\} \cup \{C_k(C_l(\underbrace{\pi})) \mid k, l \in [d]\}. $$

Lemma 3.1 is obtained by a normalisation procedure that pushes controls down to a bounded set of controlled “layers” (Appendix C.1). Once circuits have been reduced to this form, each control-algebra statement can be proved by tracking how the outer controls interact with layers from $\mathcal{G}$. Compatibility reduces to exchanging the (unique) layers that simultaneously involve both outer control wires (Appendix C); commutativity reduces to commuting pairs of differently-controlled layers from $\mathcal{G}$ (Appendix D); and exhaustivity is then proved by induction, using the totalisation axioms together with the derived compatibility and commutativity steps (Appendix E).

**Theorem 3.2.** For any $n \ge 0$, any $C: n \to n$ in $CQC_d$, and any $a, b \in [d]$,

$$ QC_d \vdash C_a(C_b(C)) \circ (\underbrace{\otimes}_{\otimes} \otimes \text{id}_n) = (\underbrace{\otimes}_{\otimes} \otimes \text{id}_n) \circ C_b(C_a(C)). $$

**Theorem 3.3.** For any $n \ge 0$, any $C_1, C_2: n \to n$ in $CQC_d$, and any distinct $k, l \in [d]$,

$$ QC_d \vdash C_k(C_1) \circ C_l(C_2) = C_l(C_2) \circ C_k(C_1). $$

**Theorem 3.4.** For every $C: n \to n$ in $CQC_d$,

$$ QC_d \vdash \prod_{k=0}^{d-1} C_k(C) = \otimes C. $$
<figure><img src="image_5.png" /><figcaption>Figure 1: Core axiom schemata for QC<sub>d</sub>. In (EH), (3Rx) and (3CRx) the right-hand-side angles are determined by the explicit relations recorded in Appendix A. Rules (XH), (HPd), and (HCd) apply when the indices i, j, k are pairwise distinct. In (HHd) the indices i, j, k, ℓ are pairwise distinct.</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Figure 2: Auxiliary axiom schemata for QC<sub>d</sub>. (1) “Totalisation” rules (TP) and (TH), used to recover exhaustivity of control by a structural induction on circuits. If one takes exhaustivity as an admissible rule schema, then (TP) and (TH) are immediate instances and can be omitted. (2) Local commutation/conjugation schemata for differently-controlled operations: (PPc), (Pπc), (ππc), (ππdc), (HPc), (HCc), (HHc) require $k \neq \ell$. These patterns are redundant once one is allowed to use distinct-control commutativity as a derived rule. (3) The mixed-control swap schemata (CompP) and (Compπ). If compatibility were assumed as an ambient (structural) principle of CQC<sub>d</sub>, then (CompP) and (Compπ) would be derivable and could be omitted.</figcaption></figure>

## 4 Embedding Qudit Circuits into LOPP Circuits

Our completeness proof for QC<sub>d</sub> proceeds by reduction to linear optics. We translate qudit circuits in the PROP CQC<sub>d</sub> into circuits
in the linear-optical PROP **LOPP**, appeal to the sound and complete equational theory LOPP for **LOPP** [7, 18], and then transport derivations back to **CQC**<sub>d</sub>. The bridge is a fixed reflected d-ary Gray ordering of the computational basis (§4.2): it identifies the d<sup>n</sup> optical modes with the n-qudit basis states in such a way that consecutive modes differ in exactly one digit by ±1. As a result, each local **LOPP** generator (acting on one mode or two consecutive modes) decodes to either a basis-controlled phase or a (multi-)controlled adjacent two-level qudit gate.

A key technical point (already present for qubits [8]) is that, although both **CQC**<sub>d</sub> and **LOPP** are PROPs, their monoidal products have different semantics: ⊗ in **CQC**<sub>d</sub> is interpreted by tensor product on Hilbert spaces, whereas ⊗ in **LOPP** is interpreted by direct sum under the single-photon model (Remark 1). Consequently, our translations preserve sequential composition ◦ but cannot be strict monoidal PROP morphisms. We therefore work on raw syntax and fix a deterministic serialisation of ⊗.

Concretely, we define two context-sensitive translations:

* a contextual encoding $E_b^a$ (Definition 4.8) sending a raw n-qudit circuit to a raw **LOPP** circuit on $d^{a+n+b}$ modes, intended to represent the circuit acting on the middle n qudits of an $(a+n+b)$-qudit register; and

* a contextual decoding $D_n^t$ (Definition 4.11) sending a raw **LOPP** circuit supported on consecutive modes $t, t+1, \dots, t+\ell-1 \subseteq \{0, \dots, d^n-1\}$ to a raw n-qudit circuit, by interpreting each local optical generator as a suitably (multi-)controlled two-level qudit gate in Gray order.

The completeness transfer uses three ingredients:

(1) **ENC** (Lemma 4.10): E is semantics-preserving for the Gray-ordered LOPP semantics $[[\cdot]]_{LOPP}$ (Definition 4.7);

(2) **RETR** (Theorem 4.17): decoding the encoding recovers the original circuit (padded by identities), provably in QC<sub>d</sub>; and

(3) **MIMIC** (Theorem 4.16): any LOPP derivation decodes to a QC<sub>d</sub> derivation.

Together with completeness of LOPP, this yields completeness of QC<sub>d</sub>.

## 4.1 The LOPP calculus as a semantic model

This subsection recalls the linear-optical circuit PROP **LOPP** and its standard single-photon unitary semantics. These are the only facts about **LOPP** we use in the proof transfer: the raw syntax and quotient PROP, the interpretation $[[\cdot]]_{sp}$, and the existence of a fixed finite sound and complete equational theory.

Let $\Sigma^{LOPP}$ be the (typed) set of generators

$$[[\cdot]] : 0 \to 0, \quad \cdot : 1 \to 1, \quad \mathcal{X} : 2 \to 2,$$

together with the optical generators (each indexed by $\theta \in \mathbb{R}$)

$$-\theta : 1 \to 1, \quad \mathcal{X}^\theta : 2 \to 2.$$

Intuitively, these are the empty diagram, the identity wire, a swap of two adjacent modes, and the two basic optical components: a phase shifter and a beam splitter.

**Definition 4.1.** Let **LOPP**<sup>raw</sup> be the free endomorphism PROP on $\Sigma^{LOPP}$ (so **LOPP**<sup>raw</sup>($m, n$) = $\emptyset$ for $m \neq n$). Let $\equiv$ be the least congruence on **LOPP**<sup>raw</sup> containing all instances of the strict PROP

equations (identities, associativity/unit for ◦ and ⊗, interchange, symmetry naturality and involutivity), as in Definition 2.6.

Define the endomorphism PROP **LOPP** by

$$\mathbf{LOPP}(m, m) := \mathbf{LOPP}^{\text{raw}}(m, m) / \equiv, \quad \mathbf{LOPP}(m, n) := \emptyset \text{ if } m \neq n, \\ \text{with ◦ and ⊗ induced by the term constructors.}$$

Thus, a morphism in **LOPP**($m, m$) is an m-mode linear-optical circuit modulo strict symmetric-monoidal bookkeeping.

For $m \ge 0$, let $M_m := \mathbb{C}^m$ with its standard mode basis $\{|0\rangle, \dots, |m-1\rangle\}$. We identify unitaries $U \in U(M_m)$ with their $m \times m$ matrices in this basis, i.e. with elements of $U(m)$. For disjoint mode blocks of sizes $m$ and $n$, parallel composition corresponds to the block-diagonal direct sum: for $U \in U(m)$ and $V \in U(n)$,

$$U \oplus V := \begin{pmatrix} U & 0 \\ 0 & V \end{pmatrix} \in U(m+n),$$

using the canonical identification $M_{m+n} \cong M_m \oplus M_n$.

**Definition 4.2.** Working in the standard mode bases of $M_m = \mathbb{C}^m$, we interpret every raw **LOPP** term on m modes as an $m \times m$ unitary matrix.

The single-photon interpretation of **LOPP** is the family of maps

$$[[\cdot]]_{\text{sp}} : \mathbf{LOPP}^{\text{raw}}(m, m) \to U(m) \quad (m \in \mathbb{N})$$

defined by structural induction on raw terms:

* **Generators.**

$$[[\cdot]]_{\text{sp}} := 1, \quad [[\cdot]]_{\text{sp}} := (1), \quad [[-\theta]]_{\text{sp}} := (e^{i\theta}), \\ [[\mathcal{X}]]_{\text{sp}} := \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix}, \quad [[\mathcal{X}^\theta]]_{\text{sp}} := \begin{pmatrix} \cos(\theta) & i \sin(\theta) \\ i \sin(\theta) & \cos(\theta) \end{pmatrix}.$$

* **Sequential composition.** For $C_1, C_2 \in \mathbf{LOPP}^{\text{raw}}(m, m)$,

$$[[C_2 \circ C_1]]_{\text{sp}} := [[C_2]]_{\text{sp}} \circ [[C_1]]_{\text{sp}}.$$

* **Parallel composition.** For $C_1 \in \mathbf{LOPP}^{\text{raw}}(m, m)$ and $C_2 \in \mathbf{LOPP}^{\text{raw}}(n, n)$, $[[C_1 \otimes C_2]]_{\text{sp}} := [[C_1]]_{\text{sp}} \oplus [[C_2]]_{\text{sp}}$.

The interpretation $[[\cdot]]_{\text{sp}}$ respects the structural congruence $\equiv$ of Definition 4.1, hence factors through the quotient to a well-defined family of maps $[[\cdot]]_{\text{sp}} : \mathbf{LOPP}(m, m) \to U(M_m)$, which we again denote by $[[\cdot]]_{\text{sp}}$.

**Remark 1.** Under the single-photon interpretation, the monoidal product of **LOPP** is block-diagonal sum:

$$[[C_1 \otimes C_2]]_{\text{sp}} = [[C_1]]_{\text{sp}} \oplus [[C_2]]_{\text{sp}}.$$

In contrast, the monoidal product of **CQC**<sub>d</sub> is interpreted by the Kronecker tensor product:

$$[[C_1 \otimes C_2]] = [[C_1]] \otimes [[C_2]].$$

Because $U \oplus V$ and $U \otimes V$ are fundamentally different operations, our translations preserve sequential composition but must serialise ⊗; they therefore cannot be strict monoidal PROP morphisms.

The LOPP signature contains no primitive notion of (poly)control; in our reduction, control arises only from the Gray-coded identification between optical modes and computational basis states.
**Theorem 4.3** ([7, 18]). Let LOPP denote the equational theory consisting of the structural PROP equations together with the non-structural axiom schemata of Figure 9 (listed explicitly in Appendix I). Then LOPP is sound and complete for the single-photon semantics: for any circuits $C_1, C_2 : m \to m$,

$$[[C_1]]_{\text{sp}} = [[C_2]]_{\text{sp}} \quad \Rightarrow \quad \text{LOPP} \vdash C_1 = C_2.$$

Fix $d \ge 2$. Since an n-qudit system has Hilbert space dimension $d^n$, our encoding and decoding only use LOPP circuits on $d^n$ modes. We write $\text{LOPP}_d$ for the full subcategory of LOPP on objects $\{d^n \mid n \ge 0\}$. As noted in Remark 1, $\text{LOPP}_d$ is not closed under the monoidal product on objects, but Theorem 4.3 applies *arity-wise* to each fixed object $d^n$.

## 4.2 Gray codes for mode ordering

LOPP generators are local in the mode index: they act on one mode, or on two consecutive modes. To decode such local optical steps as local qudit operations, we fix a Gray ordering of the $d^n$ computational basis states. In this ordering, consecutive mode labels correspond to basis words that differ in exactly one digit, by $\pm 1$. We will use this neighbour property in §4.4 to interpret two-mode LOPP generators as (multi-)controlled adjacent two-level qudit gates.

Fix $d \ge 2$ and write $[d] = \{0, 1, \dots, d-1\}$. An n-qudit register has Hilbert space $\mathcal{H}_n = (\mathbb{C}^d)^{\otimes n}$ with computational basis $\{|x\rangle \mid x \in [d]^n\}$. In the single-photon optical model, a $d^n$-mode interferometer acts on $\mathcal{M}_{d^n}$ with basis $\{|t\rangle \mid 0 \le t < d^n\}$, where $|t\rangle$ means “one photon in mode $t$”. We now choose an explicit identification between these bases that interacts well with consecutive mode indices.

We use the standard reflected d-ary Gray code, which specialises to the usual binary reflected Gray code when $d = 2$.

**Definition 4.4.** Let $[d] = \{0, 1, \dots, d-1\}$. For each $n \ge 0$ define a map

$$G_n^d : \{0, 1, \dots, d^n - 1\} \to [d]^n$$

recursively by:

* $G_0^d(0) = \epsilon$;

* for $n \ge 1$, write $0 \le k < d^n$ uniquely as $k = q \cdot d^{n-1} + r$ with $0 \le q < d$ and $0 \le r < d^{n-1}$, and set

$$G_n^d(k) := \begin{cases} q \cdot G_{n-1}^d(r) & \text{if } q \text{ is even,} \\ q \cdot G_{n-1}^d(d^{n-1} - 1 - r) & \text{if } q \text{ is odd.} \end{cases}$$

Here $\epsilon$ is the empty word, and $q \cdot w$ denotes prefixing the word $w$ by the digit $q$. The next lemma records the operational fact we need: in Gray order, incrementing the mode index changes exactly one computational digit, and only by an adjacent step.

For $d = 3$ and $n = 2$ the reflected Gray order is

$00, 01, 02, 12, 11, 10, 20, 21, 22,$

so successive words differ in exactly one digit, and that digit changes by $\pm 1$.

**Lemma 4.5.** For all $n \ge 1$, we have $G_n^d(0) = (0, \dots, 0)$. Moreover, for each $0 \le k < d^n - 1$ the words $G_n^d(k)$ and $G_n^d(k + 1)$ differ in exactly one position, and in that position the digit changes by one: if

$$G_n^d(k) = (a_1, \dots, a_n) \quad \text{and} \quad G_n^d(k + 1) = (b_1, \dots, b_n),$$

then their is a unique $t \in \{1, \dots, n\}$ such that $a_t \ne b_t$ and $|a_t - b_t| = 1$, while $a_j = b_j$ for all $j \ne t$.

We package the resulting basis reordering as a permutation unitary on $\mathcal{H}_n$.

**Definition 4.6.** For each $n \ge 0$, define the unitary $\mathfrak{G}_{n,d} : \mathcal{M}_{d^n} \to \mathcal{H}_n$ as the permutation matrix implementing the Gray reordering:

$$\mathfrak{G}_{n,d} := \sum_{t=0}^{d^n-1} |G_n^d(t)\rangle\langle t|,$$

equivalently $\mathfrak{G}_{n,d}(|t\rangle) = |G_n^d(t)\rangle$ for $0 \le t < d^n$. In particular, $\mathfrak{G}_{n,d}^{-1} = \mathfrak{G}_{n,d}^{\dagger}$.

Operationally, $\mathfrak{G}_{n,d}$ is the fixed change-of-basis map identifying the mode basis with the computational basis in Gray order.

**Definition 4.7.** For each $n \ge 0$ define a map on raw terms

$$[\cdot]_{\text{LOPP}} : \text{LOPP}^{\text{raw}}(d^n, d^n) \to \text{Qudit}_d(n, n)$$

by conjugating the single-photon matrix semantics with the Gray permutation matrix:

$$[[C]]_{\text{LOPP}} := \mathfrak{G}_{n,d} \circ [[C]]_{\text{sp}} \circ \mathfrak{G}_{n,d}^{\dagger},$$

where $[[\cdot]]_{\text{sp}}$ is the single-photon interpretation of Definition 4.2.

Thus $[[\cdot]]_{\text{LOPP}}$ is the single-photon semantics transported to the qudit computational basis using the fixed Gray identification. For each $n \ge 0$, the map $[[\cdot]]_{\text{LOPP}}$ respects the structural congruence $\equiv$ on $\text{LOPP}^{\text{raw}}(d^n, d^n)$, and hence factors through the quotient to a well-defined function

$$[[\cdot]]_{\text{LOPP}} : \text{LOPP}(d^n, d^n) \to \text{Qudit}_d(n, n).$$

Moreover, the family $([[[\cdot]]_{\text{LOPP}}]_{n \ge 0})$ is compatible with identities and sequential composition, i.e. for all $C_1, C_2 : d^n \to d^n$ in LOPP,

$$[\text{id}_{d^n}]_{\text{LOPP}} = I_{q \cdot t_n}, \quad [[C_2 \circ C_1]]_{\text{LOPP}} = [[C_2]]_{\text{LOPP}} \circ [[C_1]]_{\text{LOPP}}.$$

Equivalently, $[[\cdot]]_{\text{LOPP}}$ is a well-defined functor $\text{LOPP}_d \to \text{Qudit}_d$ (with object map $d^n \mapsto n$).

Consequently, for $n \ge 0$ and $C_1, C_2 : d^n \to d^n$ in LOPP, if $[[C_1]]_{\text{LOPP}} = [[C_2]]_{\text{LOPP}}$ in $\text{Qudit}_d(n, n)$, then LOPP $\vdash C_1 = C_2$.

## 4.3 Contextual encoding of quantum circuits

Fix $d \ge 2$. This subsection defines the contextual encoding $E_b^a : \text{CQC}_d^{\text{raw}}(n, n) \to \text{LOPP}^{\text{raw}}(d^{a+n+b}, d^{a+n+b})$, which translates an n-qudit circuit into a single-photon linear-optical circuit on $d^{a+n+b}$ modes. The parameters $(a, b)$ describe surrounding context: $E_b^a(C)$ is intended to represent $C$ acting on the middle $n$ qudits of an $(a + n + b)$-qudit register.

We work on raw syntax, and we interpret LOPP circuits on $d^n$ modes via the Gray-ordered semantics $[[\cdot]]_{\text{LOPP}}$ of Definition 4.7. As noted in Remark 1, the translation preserves sequential composition $\circ$ but must serialise $\otimes$.

The encoding uses three kinds of operations on raw LOPP syntax: reordering Gray-ordered mode blocks to place an encoded subcircuit in context; lifting a local $d^n$-mode circuit across surrounding Gray branches; and lifting only along a designated branch to model control. Because reflected Gray order reverses the traversal of blocks with odd leading digit, the lifting gadgets sometimes mirror a local subcircuit; this is built into the constructions below.
We therefore fix the following raw **LOPP** constructions (defined explicitly in Appendix G and Section J):

* For all $a, n, b \ge 0$, a raw permutation circuit

$$ \sigma_{a,n,b}^d \in \text{LOPP}^{\text{raw}}(d^{a+n+b}, d^{a+n+b}), $$

intended to implement, at the level of Gray-ordered mode labels, the block symmetry that swaps the middle n-qudit block with the lower b-qudit block.

* For all $p, n \ge 0$, an operator

$$ \text{GrayLift}_d^p(-) : \text{LOPP}^{\text{raw}}(d^n, d^n) \to \text{LOPP}^{\text{raw}}(d^{n+p}, d^{n+p}), $$

which lifts a $d^n$-mode circuit uniformly across the $d^p$ Gray blocks determined by $p$ surrounding qudits.

* For all $p, n \ge 0$ and $j \in [d]$, an operator

$$ j\text{GrayLift}_d^p(-) : \text{LOPP}^{\text{raw}}(d^n, d^n) \to \text{LOPP}^{\text{raw}}(d^{n+1+p}, d^{n+1+p}), $$

which performs the same lift, but only on the branch where a designated control digit equals $j$ (and acts as the identity on the other branches).

In the main text we use only how these gadgets interact with decoding, stated in Lemmas 4.14 and 4.15.

**Remark 2.** Under the single-photon semantics, $\text{GrayLift}_d^p(C)$ is (up to Gray-induced permutations of the mode basis) a block-diagonal direct sum of $d^p$ copies of $[C]_{\text{sp}}$, one for each fixed choice of the surrounding $p$ Gray digits. The reflected Gray traversal reverses some suffix blocks (precisely when the prefix digit is odd); the GrayLift implementation accounts for this by conjugating the affected blocks by a mode-reversal permutation.

**Definition 4.8.** Fix $d \ge 2$. For each $n, a, b \ge 0$ define a function

$$ E_b^a : \text{CQC}_d^{\text{raw}}(n, n) \to \text{LOPP}^{\text{raw}}(d^{a+n+b}, d^{a+n+b}) $$

by structural induction on raw circuits.

(1) **Sequential composition.** For $C_1, C_2 \in \text{CQC}_d^{\text{raw}}(n, n)$,

$$ E_b^a(C_2 \circ C_1) := E_b^a(C_2) \circ E_b^a(C_1). $$

(2) **Parallel composition.** Let $C_1 \in \text{CQC}_d^{\text{raw}}(n_1, n_1)$ and $C_2 \in \text{CQC}_d^{\text{raw}}(n_2, n_2)$, and view $C_1 \otimes C_2$ as acting on $n_1 + n_2$ qudits with $C_1$ on the upper block and $C_2$ on the lower block. Set

$$ E_b^a(C_1 \otimes C_2) := E_b^{a+n_1}(C_2) \circ E_{b+n_2}^a(C_1). $$

This fixes our serialisation convention: we encode the lower block first and then the upper block, matching the decoding convention of Definition 4.11.

(3) **Identities.** For the canonical identity $id_n \in \text{CQC}_d^{\text{raw}}(n, n)$, set

$$ E_b^a(id_n) := id_{d^{a+n+b}}. $$

(4) **Swap.** For the swap generator, set

$$ E_b^a(\Box) := \sigma_{a,b,2}^d \circ \sigma_{a+b,1,1}^d \circ \sigma_{a,2,b}^d. $$

(5) **Global phases.** For the scalar phase generator with parameter $\theta$, set

$$ E_b^a(\emptyset) := (-[\emptyset] -)^{\otimes d^{a+b}}. $$

(Under the single-photon semantics, applying the same phase shifter on every mode yields a global phase.)

(6) **Two-level Hadamards.** For each $0 \le i < d - 1$, fix a $d$-mode **LOPP** circuit $B_d^{(i,i+1)} : 1^{\otimes d} \to 1^{\otimes d}$ whose single-photon semantics is $H_d^{(i,i+1)}$. (Existence follows from standard linear-optical decompositions; a concrete choice is given in Appendix G.) Define

$$ E_b^a(-[H^{(r,r+1)}]) := \sigma_{a,1,b}^d \circ \text{GrayLift}_d^{a+b}(B_d^{(i,i+1)}) \circ \sigma_{a,b,1}^d. $$

(7) **Control.** For $C \in \text{CQC}_d^{\text{raw}}(n, n)$ and $j \in [d]$, define

$$ E_b^a(C_j(C)) := \sigma_{a,n+1,b}^d \circ j\text{GrayLift}_d^{a+b}(E_0^0(C)) \circ \sigma_{a,b,n+1}^d. $$

Finally, for $C \in \text{CQC}_d^{\text{raw}}(n, n)$ we abbreviate $E(C) := E_0^0(C) \in \text{LOPP}^{\text{raw}}(d^n, d^n)$.

We record two basic properties of the encoding. First, it respects the structural congruence on raw qudit circuits and therefore descends to the quotient PROP.

**Lemma 4.9.** Fix $d \ge 2$. For all $n, a, b \ge 0$ and all raw circuits $C, C' \in \text{CQC}_d^{\text{raw}}(n, n)$, if $C \equiv C'$ in the structural congruence of Definition 2.6, then

$$ E_b^a(C) \equiv E_b^a(C') $$

in the strict-PROP congruence on raw **LOPP** circuits of Definition 4.1. Hence $E_b^a$ induces a well-defined function

$$ E_b^a : \text{CQC}_d(n, n) \to \text{LOPP}(d^{a+n+b}, d^{a+n+b}). $$

Second, the encoding preserves the intended unitary semantics, where **LOPP** circuits are interpreted through the Gray identification.

**Lemma 4.10.** For every $n \ge 0$ and every circuit $C : n \to n$ in $\text{CQC}_d$,

$$ [E(C)]_{\text{LOPP}} = [C]. \qquad (\text{ENC}) $$

## 4.4 Contextual decoding of LOPP circuits

This subsection defines a syntax-directed decoding map from raw **LOPP** circuits back to raw qudit circuits. The key point is locality: $-[\emptyset] -$ acts on one mode, while $\times$ and $\supseteq$ act on two consecutive modes. Under the reflected Gray ordering (Definition 4.4), two consecutive modes correspond to computational basis words that differ in exactly one digit by $\pm 1$ (Lemma 4.5). Decoding therefore produces either a basis-state phase, or an adjacent two-level single-qudit gate controlled on the surrounding digits.

We reuse the derived one-qudit gate families $-[X^{(i,j)}]$ (two-level swaps) and $-[R_X^{(i,j)}(\emptyset)]$ (two-level beam-splitter rotations) from §3.1. Recall also that for a word $u \in [d]^*$ and a circuit $f$ we write $C_u(f)$ for iterated control by $u$.

Given $n \ge 1$ and words $u, w \in [d]^*$ with $|u| + 1 + |w| = n$, we define for any one-qudit gate $g : 1 \to 1$ the $n$-qudit circuit

$$ \Lambda_w^u(g) := \sigma_{|u|,|w|,1} \circ C_{uw}(g) \circ \sigma_{|u|,1,|w|}, $$

where $uw$ is concatenation and $\sigma_{a,b,c} := id_a \otimes \sigma_{b,c}$. Semantically, $\Lambda_w^u(g)$ applies $g$ to qudit $|u|+1$ if and only if the surrounding qudits are in basis state $|u\rangle \otimes |w\rangle$, and acts as the identity otherwise.

**Definition 4.11.** Fix $d \ge 2$ and $n \ge 0$. For integers $t, \ell$ with $0 \le t$ and $t + \ell \le d^n$, define a map

$$ D_n^t : \text{LOPP}^{\text{raw}}(t, \ell) \to \text{CQC}_d^{\text{raw}}(n, n) $$
by structural induction on the raw **LOPP** term, viewing it as occupying the consecutive global modes $t, \dots, t + \ell - 1$:

(1) Sequential composition. If $C_1, C_2 \in \text{LOPP}^{\text{raw}}(\ell, \ell)$, then

$$D_n^t(C_2 \circ C_1) := D_n^t(C_2) \circ D_n^t(C_1).$$

(2) Parallel composition (serialised). If $C_1 \in \text{LOPP}^{\text{raw}}(\ell_1, \ell_1)$ and $C_2 \in \text{LOPP}^{\text{raw}}(\ell_2, \ell_2)$, placed side by side so that $C_1$ occupies modes $t, \dots, t + \ell_1 - 1$ and $C_2$ occupies modes $t + \ell_1, \dots, t + \ell_1 + \ell_2 - 1$, then

$$D_n^t(C_1 \otimes C_2) := D_n^{t+\ell_1}(C_2) \circ D_n^t(C_1).$$

(3) Structural generators. For the empty diagram and the identity wire,

$$D_n^t(\begin{smallmatrix} r & -\ell \\ -\ell & -\ell \end{smallmatrix}) := \text{id}_n, \quad D_n^t(\begin{smallmatrix} -\ell & -\ell \\ -\ell & -\ell \end{smallmatrix}) := \text{id}_n.$$

(4) Phase shifters. Let $\begin{smallmatrix} -\theta \\ \theta \end{smallmatrix}$ act on the (global) mode $t$, and write $G_n^d(t) = u \in [d]^n$. Define

$$D_n^t(\begin{smallmatrix} -\theta \\ \theta \end{smallmatrix}) := C_u(\begin{smallmatrix} \theta \end{smallmatrix}).$$

(5) Two-mode generators on consecutive modes. Assume $n \ge 1$ and consider a generator acting on consecutive global modes $t$ and $t+1$ (so $t+1 < d^n$). By Lemma 4.5 there are unique words $u, w \in [d]^*$, a unique digit $v \in [d]$, and a unique sign $\varepsilon \in \{-1, 1\}$ (with $v + \varepsilon \in [d]$) such that

$$G_n^d(t) = uvw, \quad G_n^d(t+1) = u(v+\varepsilon)w, \quad |u|+1+|w|=n.$$

* Swap of modes. For the **LOPP** swap generator, set

$$D_n^t(\begin{smallmatrix} \times \\ \times \end{smallmatrix}) := \Lambda_w^u(\begin{smallmatrix} -\chi^{(v,v+\varepsilon)} \\ \chi^{(v,v+\varepsilon)} \end{smallmatrix}).$$

* Beam splitter. For the **LOPP** beam splitter generator, set

$$D_n^t(\begin{smallmatrix} \theta \\ \theta \end{smallmatrix}) := \Lambda_w^u(\begin{smallmatrix} -\chi^{(v,v+\varepsilon)}(\theta) \\ \chi^{(v,v+\varepsilon)}(\theta) \end{smallmatrix}).$$

Finally, for a raw **LOPP** circuit $C$ on $d^n$ modes we abbreviate $D(C) := D_n^0(C) \in \text{CQC}_d^{\text{raw}}(n, n)$.

**Lemma 4.12.** Each decoded generator acts non-trivially on at most one two-dimensional computational subspace (determined by one or two consecutive Gray indices) and as the identity on the orthogonal complement:

* $D_n^t(\begin{smallmatrix} -\theta \\ \theta \end{smallmatrix})$ applies a phase only on the basis vector $|G_n^d(t)\rangle$;

* $D_n^t(\begin{smallmatrix} \times \\ \times \end{smallmatrix})$ and $D_n^t(\begin{smallmatrix} \theta \\ \theta \end{smallmatrix})$ act only on $\text{span}\{|G_n^d(t)\rangle, |G_n^d(t+1)\rangle\}$.

**Lemma 4.13.** Let $C_1, C_2$ be raw **LOPP** circuits on $d^n$ modes. If $C_1 \equiv C_2$ in the structural congruence generated by the strict PROP equations (as in Definition 4.1), then

$$QC_d \vdash D(C_1) = D(C_2).$$

*Proof.* See Appendix I. The proof is by induction on strict-PROP contexts. The only non-trivial case is the mixed-product axiom; it is handled because decoding of subcircuits on disjoint mode blocks yields (multi-)controlled gates that commute in $QC_d$ (using derived distinct-control commutativity). □

We now record the two interface facts about the **LOPP** gadgets used in the encoding (introduced in §4.3) that we will need for the encoding/decoding retraction argument.

**Lemma 4.14.** Let $D_n^t$ be the contextual decoding map of Definition 4.11. For every $n, p \ge 0$ and every raw **LOPP** circuit $C \in \text{LOPP}^{\text{raw}}(d^n, d^n)$ we have

$$QC_d \vdash D_{n+p}^0 (\text{GrayLift}_d^p(C)) = \text{id}_p \otimes D_n^0(C).$$

Moreover, for each $j \in [d]$,

$$QC_d \vdash D_{n+1+p}^0 (j\text{GrayLift}_d^p(C)) = \text{id}_p \otimes C_j (D_n^0(C)).$$

*Proof.* See Appendix H, in particular Lemmas H.4 and H.5. □

*Remark 3.* Intuitively, decoding a GrayLift produces a product over all control branches. Regrouping branches uses derived commutativity of distinct control (Appendix D), and collapsing the total product uses derived exhaustivity (Appendix E).

**Lemma 4.15.** For all $a, n, b \ge 0$,

$$QC_d \vdash D_{a+n+b}^0 (\sigma_{a,n,b}^d) = \sigma_{a,n,b},$$

where $\sigma_{a,n,b} : a + n + b \to a + b + n$ denotes the corresponding qudit-wire symmetry $\sigma_{a,n,b} := \text{id}_a \otimes \sigma_{n,b}$.

*Proof.* See Appendix J. □

**Theorem 4.16.** Let $n \ge 0$ and let $C_1, C_2 : d^n \to d^n$ be circuits in **LOPP**. If $\text{LOPP} \vdash C_1 = C_2$, then $QC_d \vdash D(C_1) = D(C_2)$.

*Proof.* This follows by induction on **LOPP**-derivations, using that decoding is compatible with the strict PROP congruence (Lemma 4.13) and by checking axiom-by-axiom, that each non-structural **LOPP** axiom decodes to a derivable equation in $QC_d$. Full details are given in Appendix I. □

Thus every rewrite used in an **LOPP** derivation can be replayed, after decoding, inside $QC_d$. We will combine this mimicking step with the encoding/decoding retraction in the next subsection to transfer completeness from **LOPP** to $QC_d$.

## 4.5 Completeness via the linear-optical reduction

This subsection assembles the translation results into a single completeness argument for $QC_d$. The main point is that encoding into **LOPP** and then decoding back is a retraction provable in $QC_d$; combined with mimicking (Theorem 4.16) and completeness of **LOPP**, this transfers semantic equality to derivability in $QC_d$.

**Theorem 4.17.** For all $n, a, b \ge 0$ and all circuits $C : n \to n$ in $\text{CQC}_d$,

$$QC_d \vdash D_{a+n+b}^0 (E_b^a(C)) = \text{id}_a \otimes C \otimes \text{id}_b.$$

*Proof.* Pick a raw representative of $C$ and argue by structural induction. The cases for $\circ$ and the (serialised) $\otimes$ follow immediately from Definitions 4.8 and 4.11. All generator cases are handled uniformly by eliminating the block-permutation wrapper via Lemma 4.15, and discharging the remaining GrayLift steps via Lemma 4.14; the full bookkeeping is given in Appendix H.

We only expand the key control step. Let $C = C_j(C')$ with $C' : m \to m$. By Definition 4.8 we have

$$E_b^a(C) = \sigma_{a,m+1,b}^d \circ j\text{GrayLift}_d^{a+b}(E_0^0(C')) \circ \sigma_{a,b,m+1}^d.$$
Applying $D_{a+m+1+b}^0$ and using Lemma 4.15 (on the outer permutations) together with the controlled GrayLift interface in Lemma 4.14 yields, in QC$_d$,

$$
\begin{align*}
D_{a+m+1+b}^{0}(E_{b}^{a}(C_{j}(C'))) &= \sigma_{a,m+1,b} \circ (\mathrm{id}_{a+b} \otimes C_{j}(D_{m}^{0}(E_{0}^{0}(C')))) \\
&\quad \circ \sigma_{a,b,m+1} \\
&= \mathrm{id}_{a} \otimes C_{j}(D_{m}^{0}(E_{0}^{0}(C')) \otimes \mathrm{id}_{b} \\
&= \mathrm{id}_{a} \otimes C_{j}(C') \otimes \mathrm{id}_{b},
\end{align*}
$$

where the middle equality is strict PROP coherence and the last
equality uses the induction hypothesis for $C'$ at context (0, 0). □

**Corollary 4.18.** For every $n \ge 0$ and every circuit $C : n \to n$ in $CQC_d$, $QC_d \vdash D(E(C)) = C$.

PROOF. Set $a = b = 0$ in Theorem 4.17. □

**Theorem 4.19.** For every $d \ge 2$ the equational theory QC$_d$ of $CQC_d$ is sound and complete for $d$-dimensional unitary circuit. That is, for any $n$-qudit circuits $C_1, C_2 : n \to n$ we have

$$
\llbracket C_1 \rrbracket = \llbracket C_2 \rrbracket \iff QC_d \vdash C_1 = C_2.
$$

PROOF. Soundness is immediate: each axiom schema is valid under $[[–]]$, and $[[–]]$ is a strict symmetric monoidal functor (Proposition 2.10).

For completeness, if $[[C_1]] = [[C_2]]$ then by Lemma 4.10 we have
$[[E(C_1)]]_{LOPP} = [[E(C_2)]]_{LOPP}$, hence completeness of LOPP gives
LOPP $\vdash E(C_1) = E(C_2)$. Decode and mimic (Theorem 4.16) to obtain
$QC_d \vdash D(E(C_1)) = D(E(C_2))$, and conclude by Corollary 4.18. $\square$

**5 Conclusion**

We presented a dimension-uniform, circuit-level equational theory for unitary qudit circuits. Our starting point is the polycontrolled circuit PROP CQC<sub>d</sub>, where control is primitive: for each *k* ∈ [*d*], the constructor C<sub>*k*</sub>(*−*) functionally adjoins a distinguished control wire and applies a circuit exactly when that wire is in basis state |*k*⟩. Over a fixed universal gate signature (adjacent two-level Hadamards, basis-controlled phases, and the structural PROP generator), we defined QC<sub>d</sub>: a *finite* family of local axiom schemata whose instances involve at most three wires and whose diagrammatic shape is independent of *d*. Our main theorem establishes soundness and completeness for the standard semantics [[−]]: CQC<sub>d</sub> → Qudit<sub>d</sub>: QC<sub>d</sub> derives exactly the valid equalities of exact unitary semantics, including global phases as 0 → 0 scalars. A notable consequence is that the expected global control algebra (compatibility, distinct-control commutativity, and exhaustivity) is derivable within QC<sub>d</sub>, rather than being imposed as part of the ambient structural congruence.

Completeness is obtained by a modular proof transfer to linear
optics. Using the reflected *d*-ary Gray code, we encode *n*-qudit cir-
cuits as *d*<sup>*n*</sup>-mode single-photon **LOPP** circuits (up to conjugation
by a fixed Gray-basis permutation), and we handle the tensor/direct-
sum mismatch by a deterministic serialisation of ⊗. We then prove
an encoding/decoding retraction inside QC<sub>*d*</sub> and a mimicking theo-
rem showing that every LOPP rewrite step decodes to a derivation
in QC<sub>*d*</sub>. In this way, completeness of LOPP yields completeness of
QC<sub>*d*</sub>.

Several directions remain open. First, it is natural to extend beyond unitary endomorphisms to circuits with ancilla initialisation, discard, and measurement, aiming for finitary, bounded-arity axiomatisations of qudit channels. Second, on the algorithmic side, it would be valuable to extract practical rewriting methods from QC<sub>d</sub> (normal forms, decision procedures, or terminating/confluent fragments) and to connect them to certified optimisation and verification pipelines for native qudit hardware. Finally, exploring alternative embeddings or gate signatures that better align monoidal structure, may simplify both the metatheory and its compiler-facing interfaces.

**Acknowledgments**

I thank my PhD advisors, Simon Perdrix and Miriam Backens, for
their helpful feedback and for reviewing earlier versions of this
article. 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.
References

[1] Miriam Backens and Aleks Kissinger. 2019. ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non-linearity. *Electronic Proceedings in Theoretical Computer Science* 287 (2019), 23–42. doi:10.4204/EPTCS.287.2 Preprint: arXiv:1805.02175.

[2] Adriano Barenco, Charles H. Bennett, Richard Cleve, David P. DiVincenzo, Norman Margolus, Peter Shor, Tycho Sleator, John Smolin, and Harald Weinfurter. 1995. Elementary gates for quantum computation. *Physical Review A* 52, 5 (1995), 3457–3467. doi:10.1103/PhysRevA.52.3457

[3] Jean-Luc Brylinski and Ranee Brylinski. 2002. Universal Quantum Gates. In *Mathematics of Quantum Computation*. Chapman & Hall/CRC, Boca Raton, FL, USA, 101–116. doi:10.1201/9781420035377-5

[4] Kostia Chardonnet, Marc de Visme, Benoît Valiron, and Renaud Vilmart. 2025. The Many-Worlds Calculus. *Logical Methods in Computer Science* 21, 2 (2025), 13:1–13:44. doi:10.46298/lmcs-21(2:13)2025 Preprint: arXiv:2206.10234.

[5] Giulio Chiribella, Giacomo Mauro D’Ariano, Paolo Perinotti, and Benoît Valiron. 2013. Quantum computations without definite causal structure. *Physical Review A* 88, 2 (2013), 022318. doi:10.1103/PhysRevA.88.022318

[6] Alexandre Clément, Noé Delorme, and Simon Perdrix. 2024. Minimal Equational Theories for Quantum Circuits. In *Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2024)*. IEEE Computer Society Press, Tallinn, Estonia, 27:1–27:14. doi:10.1145/3661814.3662088 See also arXiv:2311.07476.

[7] Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Benoît Valiron. 2022. LOv-Calculus: A Graphical Language for Linear Optical Quantum Circuits. In *47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 241)*. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 35:1–35:16. doi:10.4230/LIPIcs.MFCS.2022.35 Full version: arXiv:2204.11787.

[8] Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Benoît Valiron. 2023. A Complete Equational Theory for Quantum Circuits. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), Boston, MA, USA, June 26–29, 2023*. IEEE, Boston, MA, USA, 1–13. doi:10.1109/LICS6636. 2023.10175801 Full version: arXiv:2206.10577.

[9] Alexandre Clément, Simon Perdrix, Noé Delorme, and Renaud Vilmart. 2024. Quantum Circuit Completeness: Extensions and Simplifications. In *Computer Science Logic (CSL 2024) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 288)*. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 20:1–20:23. doi:10.4230/LIPIcs.CSL.2024.20

[10] William R. Clements, Peter C. Humphreys, Benjamin J. Metcalf, W. Steven Kolthammer, and Ian A. Walmsley. 2016. Optimal design for universal multiprotocol interferometers. *Optica* 3, 12 (2016), 1460–1465. doi:10.1364/OPTICA.3.001460

[11] Bob Coecke and Ross Duncan. 2011. Interacting quantum observables: categorical algebra and diagrammatics. *New Journal of Physics* 13 (2011), 043016. doi:10.1088/1367-2630/13/4/043016

[12] Niel de Beaudrap, Aleks Kissinger, and John van de Wetering. 2022. Circuit Extraction for ZX-Diagrams Can Be #P-Hard. In *49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 229)*. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 119:1–119:19. doi:10.4230/LIPIcs.ICALP.2022.119

[13] Marc de Visme and Renaud Vilmart. 2025. Minimality in Finite-Dimensional ZW-Calculi. In *Computer Science Logic (CSL 2025) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 326)*. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 49:1–49:22. doi:10.4230/LIPIcs.CSL.2025.49 Full version: arXiv:2401.16225.

[14] Noé Delorme and Simon Perdrix. 2026. Diagrammatic Reasoning with Control as a Constructor: Applications to Quantum Circuits. In *Proceedings of the International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2026) (Lecture Notes in Computer Science)*. Springer. arXiv:2508.21756 [quant-ph] Accepted for publication.

[15] David Deutsch. 1989. Quantum computational networks. *Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences* 425, 1868 (Sept. 1989), 73–90. doi:10.1098/rspa.1989.0099

[16] Yao-Min Di and Hai-Rui Wei. 2013. Synthesis of Multivalued Quantum Logic Circuits by Elementary Gates. *Physical Review A* 87, 1 (2013), 012325. doi:10.1103/PhysRevA.87.012325

[17] Chris Heunen, Robin Kaarsgaard, and Louis Lemonnier. 2025. One rig to control them all. arXiv:2510.05032 [cs.LO] https://arxiv.org/abs/2510.05032

[18] Nicolas Heurtel. 2025. A Complete Graphical Language for Linear Optical Circuits with Finite-Photon-Number Sources and Detectors. In *Computer Science Logic (CSL 2025) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 326)*. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 38:1–38:23. doi:10.4230/LIPIcs.CSL.2025.38 Full version: arXiv:2402.17693.

[19] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. 2020. Completeness of the ZX-Calculus. *Logical Methods in Computer Science* 16, 2 (June 2020), 11:1–11:72. doi:10.23638/LMC-16(2:11)2020

[20] Sarah Meng Li, Michele Mosca, Neil J. Ross, John van de Wetering, and Yuming Zhao. 2025. A Complete and Natural Rule Set for Multi-Qutrit Clifford Circuits. *Electronic Proceedings in Theoretical Computer Science* 426 (Aug. 2025), 23–78. doi:10.4204/eptcs.426.2

[21] Robert Lin. 2021. An Algebraic Framework for Multi-Qudit Computations with Generalized Clifford Algebras. arXiv:2103.15324 [quant-ph] doi:10.48550/arXiv.2103.15324

[22] Robert Lin. 2025. A Graphical Calculus for Quantum Computing with Multiple Qudits using Generalized Clifford Algebras. *Quantum* 9 (Nov. 2025), 1913. doi:10.22331/q-2025-11-17-1913

[23] Saunders Mac Lane. 1965. Categorical Algebra. *Bull. Amer. Math. Soc.* 71, 1 (1965), 40–106. doi:10.1090/S0002-9904-1965-11234-4

[24] Michael A. Nielsen and Isaac L. Chuang. 2010. *Quantum Computation and Quantum Information* (10th anniversary ed.). Cambridge University Press, Cambridge. See pp. 189–192.

[25] Filipa C. R. Peres. 2023. Pauli-based model of quantum computation with higher-dimensional systems. *Physical Review A* 108, 3 (2023), 032606. doi:10.1103/PhysRevA.108.032606

[26] Boldizsár Poór, Razin A. Shaikh, and Quanlong Wang. 2025. ZX-calculus is Complete for Finite-Dimensional Hilbert Spaces. *Electronic Proceedings in Theoretical Computer Science* 426 (Aug. 2025), 127–158. doi:10.4204/eptcs.426.5

[27] Carlos Efrain Quintero Narvaez. 2021. Universality for Sets of Three-Valued Qubit Gates. arXiv:2109.07282 [quant-ph] https://arxiv.org/abs/2109.07282

[28] André Ranchin and Bob Coecke. 2014. Complete set of circuit equations for stabilizer quantum mechanics. *Physical Review A* 90, 1 (2014), 012109. doi:10.1103/PhysRevA.90.012109

[29] D. J. Rowe, B. C. Sanders, and H. de Guise. 1999. Representations of the Weyl group and Wigner functions for SU(3). *J. Math. Phys.* 40, 7 (1999), 3604–3615. doi:10.1063/1.532911

[30] Patrick Roy, John van de Wetering, and Lia Yeh. 2023. The Qudit ZH-Calculus: Generalised Toffoli+Hadamard and Universality. *Electronic Proceedings in Theoretical Computer Science* 384 (2023), 142–170. doi:10.4204/EPTCS.384.9 Preprint: arXiv:2307.10095.

[31] John van de Wetering and Lia Yeh. 2023. Building Qutrit Diagonal Gates from Phase Gadgets. *Electronic Proceedings in Theoretical Computer Science* 394 (2023), 46–65. doi:10.4204/EPTCS.394.4 Preprint: arXiv:2204.13681.

[32] Renaud Vilmart. 2019. A near-minimal axiomatisation of ZX-calculus for pure qubit quantum mechanics. In *Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019)*. IEEE Computer Society Press, Vancouver, BC, Canada, 768–777. doi:10.1109/LICS.2019.8785765

[33] Quanlong Wang. 2021. Qufinite ZX-calculus: A Unified Framework of Qudit ZX-Calculi. arXiv:2104.06429 [quant-ph] https://arxiv.org/abs/2104.06429

[34] Quanlong Wang, Boldizsár Poór, and Razin A. Shaikh. 2023. Completeness of qufinite ZXW calculus, a graphical language for finite-dimensional quantum theory. arXiv:2309.13014 [quant-ph] https://arxiv.org/abs/2309.13014
## A Angle relations for rotation axioms

This appendix fixes the *meta-level parameter functions* used in the rotation axioms (EH), (3Rx) and (3CRx). Each of these axioms is a schematic equation in which the *left-hand side* contains freely chosen real parameters, while the *right-hand side* parameters are *deterministic functions* of the left-hand side. The purpose of recording these functions is purely bookkeeping: it makes each axiom schema fully explicit, and (when needed) supports a uniqueness convention for rewriting.

In Delorme's one-qubit Euler parametrisations, the decomposition of a two-level unitary naturally comes with an overall scalar factor (global phase in $U(2)$). In the present paper we apply such decompositions inside a fixed two-dimensional subspace span{|$i$⟩, |$j$⟩} of a d-level system. A phase factor that is “global” for the 2 × 2 block is not a scalar on the full d-dimensional space: rather, it is the operation that multiplies both |$i$⟩ and |$j$⟩ by the same phase while leaving the other basis levels unchanged. In our syntax this is realised by applying the same level-phase on both levels, i.e. by $C_i(α) \circ C_j(α)$. Crucially, on the (i, j)-subspace this acts as $e^{iα}I_2$, hence it commutes with every gate supported on (i, j) (in particular with $H^{(i,j)}$ and with all level phases). As a result, whenever the qubit formulas isolate a scalar phase, we are free to slide the corresponding two-level phase and absorb it into neighbouring level phases. This is the only reason our explicit angle formulas do not coincide syntactically with the qubit case; semantically they implement the same underlying $U(2)$ parametrisation on span{|$i$⟩, |$j$⟩}.

Throughout, equalities between angles are understood modulo $2π$. We write $arg(z)$ for the principal argument of a non-zero complex number $z \in \mathbb{C}$, taking values in $(-π, π]$. When we restrict an angle to a range (e.g. $β \in [0, 2π)$), we always mean its canonical representative in that interval. We also use the standard two-argument arctangent $atan2(y, x)$ with values in $(-π, π]$.

## Euler-type relation (EH)

The axiom (EH) is a two-level Euler-type identity (applied in the paper on a subspace span{|$i$⟩, |$j$⟩} of a qudit). Syntactically, the left-hand side is parameterised by two real angles $α_0, α_2$, while the right-hand side uses four angles $β_0, β_1, β_2, β_3$. The intended meaning is:

for every choice of ($α_0, α_2$), there is a unique choice of ($β_0, β_1, β_2, β_3$) in the prescribed ranges that makes (EH) sound (on the relevant two-dimensional subspace), and hence sound as a qudit equation by acting as the identity outside that subspace.

We follow Delorme's explicit Euler parametrisation (stated for qubits) and use the same extraction function, with the “two-level global phase” convention explained above.

Given $α_0, α_2 \in \mathbb{R}$, define

$$z = -\sin\left(\frac{\alpha_0 + \alpha_2}{2}\right) + i \cos\left(\frac{\alpha_0 - \alpha_2}{2}\right), \quad z' = \cos\left(\frac{\alpha_0 + \alpha_2}{2}\right) - i \sin\left(\frac{\alpha_0 - \alpha_2}{2}\right).$$

We then define $β_0, β_1, β_2, β_3 \in [0, 2π)$ by cases. The degenerate cases $z = 0$ or $z' = 0$ are treated separately to avoid dividing by 0; the generic case uses the ratio $z/z'$.

* If $z' = 0$, set

$$β_0 = 2 \arg(z), \quad β_1 = \frac{\pi + α_0 + α_2}{2} - \arg(z), \quad β_2 = \frac{\pi + α_0 + α_2}{2} - \arg(z), \quad β_3 = 0.$$

* If $z = 0$, set

$$β_0 = 2 \arg(z'), \quad β_1 = \frac{α_0 + α_2}{2} - \arg(z'), \quad β_2 = π + \frac{α_0 + α_2}{2} - \arg(z'), \quad β_3 = 0.$$

* Otherwise (when $z \neq 0$ and $z' \neq 0$), set

$$β_0 = \arg(z) + \arg(z'), \quad β_1 = -\arg\left(i + \left|\frac{z}{z'}\right|\right) + \frac{\pi + α_0 + α_2}{2} - \arg(z),$$

$$β_2 = \arg\left(i + \left|\frac{z}{z'}\right|\right) + \frac{\pi + α_0 + α_2}{2} - \arg(z), \quad β_3 = \arg(z) - \arg(z').$$

With this choice, Equation (EH) holds on the relevant two-dimensional subspace. Since every occurrence of (EH) in the main development is applied to a two-level gate supported on span{|$i$⟩, |$j$⟩} and acts as the identity on the other computational levels, these formulas can be used systematically for all $d \ge 2$.

## Three-rotation identities (3Rx and 3CRx)

The axioms (3Rx) and (3CRx) express the standard fact that the same real 3 × 3 rotation (hence an element of SO(3)) admits both a ZXZ and an XZX Euler decomposition. They are the qudit/circuit-side reflections of the “(E3)” principle used in the linear-optical setting: (3Rx) is the uncontrolled identity, and (3CRx) is its controlled analogue. The parameter relations are identical in both cases.

Concretely, let $R_x(θ)$ and $R_z(θ)$ be the standard real rotation matrices about the x- and z-axes, and write

$$R_{E3} = \begin{pmatrix} r_{1,1} & r_{1,2} & r_{1,3} \\ r_{2,1} & r_{2,2} & r_{2,3} \\ r_{3,1} & r_{3,2} & r_{3,3} \end{pmatrix} \in \text{SO}(3).$$

The angles $γ_1, γ_2, γ_3$ (left-hand side of (3Rx)) and $δ_1, δ_2, δ_3$ (right-hand side) are chosen so that

$$R_{E3} = R_z(γ_1) R_x(γ_2) R_z(γ_3) = R_x(δ_1) R_z(δ_2) R_x(δ_3). \quad (11)$$
Thus $(\gamma_1, \gamma_2, \gamma_3)$ are the ZX Euler angles of $R_{E3}$ and $(\delta_1, \delta_2, \delta_3)$ are the corresponding XZX Euler angles.

The extraction formulas below are exactly those used in the linear-optical literature; they are stated with explicit “generic” and “gimbal-lock” cases, since Euler angle are not unique in degenerate configurations.

Assume first that we are not in a gimbal-lock configuration for XZX, i.e. $-1 < r_{1,1} < 1$. Then

$$ \delta_2 = \arccos(r_{1,1}), \quad \delta_1 = \operatorname{atan2}(r_{3,1}, r_{2,1}), \quad \delta_3 = \operatorname{atan2}(r_{1,3}, -r_{1,2}). \qquad (12) $$

The remaining cases correspond to gimbal lock for XZX, i.e. $\delta_2 \in \{0, \pi\}$, where only a constraint on $\delta_1 \pm \delta_3$ is determined:

* If $r_{1,1} = 1$, then necessarily $\delta_2 = 0$, and all solutions satisfy

$$ \delta_2 = 0, \quad \delta_1 + \delta_3 = \operatorname{atan2}(r_{3,2}, r_{3,3}). \qquad (13) $$

* If $r_{1,1} = -1$, then necessarily $\delta_2 = \pi$, and all solutions satisfy

$$ \delta_2 = \pi, \quad \delta_1 - \delta_3 = \operatorname{atan2}(r_{3,2}, r_{3,3}). \qquad (14) $$

In gimbal-lock cases there remains one degree of freedom in $(\delta_1, \delta_3)$; any choice satisfying (13) or (14) yields the same rotation matrix. For definiteness one may choose canonical representatives by setting the last X-rotation to 0.

Dually, if $-1 < r_{3,3} < 1$, then

$$ \gamma_2 = \arccos(r_{3,3}), \quad \gamma_3 = \operatorname{atan2}(r_{1,3}, -r_{2,3}), \quad \gamma_1 = \operatorname{atan2}(r_{3,1}, r_{3,2}). \qquad (15) $$

The degenerate ZXZ cases are:

* If $r_{3,3} = 1$, then $\gamma_2 = 0$ and all solutions satisfy

$$ \gamma_2 = 0, \quad \gamma_1 + \gamma_3 = \operatorname{atan2}(-r_{1,2}, r_{1,1}). \qquad (16) $$

* If $r_{3,3} = -1$, then $\gamma_2 = \pi$ and all solutions satisfy

$$ \gamma_2 = \pi, \quad \gamma_1 - \gamma_3 = \operatorname{atan2}(-r_{1,2}, r_{1,1}). \qquad (17) $$

Again one may choose canonical representatives (e.g. by setting the last Z-rotation to 0), but any satisfying pair give the same rotation.

## B Auxiliary diagrammatic derivations

Throughout this appendix we work in the equational theory $QC_d$, and write $QC_d \vdash C_1 = C_2$ when the circuit identity $C_1 = C_2$ is derivable from the axioms of Figures 1-2

### B.1 Catalogue of derived rules

<figure><img src="image_7.png" /><figcaption>Figure 3: Derived rules in $QC_d$ (batch 1).</figcaption></figure>
<figure><img src="image_8.png" /><figcaption>Figure 4: Derived rules in QC<sub>d</sub> (batch 2).</figcaption></figure>

## B.2 Proofs of the derived rules

PROOF OF (0PHASE).

$$ \begin{array}{l} \textcircled{0} \stackrel{(2\pi)}{=} \textcircled{0} \quad \textcircled{2\pi} \stackrel{\text{(Sum)}}{=} \textcircled{2\pi} \stackrel{(2\pi)}{=} \textcircled{2\pi} \end{array} $$
If $i < j$

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

If $i > j$, by definition $X^{i,j} = X^{j,i}$ so this is covered by the previous case. $\square$

**PROOF OF (HINV).** If $i = j$, this is trivial.

If $i < j$

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

If $i > j$,

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

**PROOF OF (HDEC).**

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

**PROOF OF (HTOT).**

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

**PROOF OF (RXTOT).**

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

<figure><img src="image_15.png" /></figure>
PROOF OF (XCTRL).

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

☐

PROOF OF (XX1).

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

☐

PROOF OF (XX2).

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

☐

PROOF OF (XCTRLSYM).

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

☐

PROOF OF (RXSYM).

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

☐
PROOF OF (HCH).

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

□

PROOF OF (CHC).

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

□

PROOF OF (PHP).

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

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

PROOF OF (HPH).

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

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

PROOF OF (CXC).

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

<figure><img src="image_29.png" /></figure>
PROOF OF (CHDEC).

<figure><img src="image_30.png" /></figure>
PROOF OF (EP).

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

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

PROOF OF (CCPDEC).

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

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

PROOF OF (CCCPDEC).

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

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

PROOF OF (CCP-CP).

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

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

PROOF OF (CCN-CP).

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

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

PROOF OF (CH-CP).

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

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

PROOF OF (CCP-CCP<sub>‡</sub>).

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

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

PROOF OF (CCP-CNOT).

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

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

PROOF OF (CCP-CCP).

<figure><img src="image_51.png" /></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" /></figure>

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

PROOF OF (CCP-CH$_{∞}$).

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

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

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

☐

PROOF OF (CCN-CP<sub>‡</sub>).

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

☐

PROOF OF (CCN-CH<sub>‡</sub>).

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

☐
PROOF OF (CH-CH$_{∞}$).

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

□

PROOF OF (CNOT-CH$_{∞}$).

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

□
PROOF OF (CCN-CH₂π).

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

☐

PROOF OF (CCN-CCN₄).

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

☐

PROOF OF (CCN-CCN₃).

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

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

PROOF OF (CCP-CCN).

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

<figure><img src="image_71.png" /></figure>
PROOF OF (CCN-CCN).

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

For any $i$ we have

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

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

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

<figure><img src="image_76.png" /></figure>
$$ (\text{CCP-CCN}) = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7, every node/.style={scale=0.7}] \tikzset{set/.style={circle, draw, fill, minimum size=1.2pt, inner sep=0pt}} \node[set, fill=blue!20] (A) at (0,0) {};
\node[set, fill=blue!20] (B) at (1,0) {};
\node[set, fill=blue!20] (C) at (2,0) {};
\node[set, fill=blue!20] (D) at (3,0) {};
\node[set, fill=blue!20] (E) at (4,0) {};
\node[set, fill=blue!20] (F) at (5,0) {};
\node[set, fill=blue!20] (G) at (6,0) {};
\node[set, fill=blue!20] (H) at (7,0) {};
\node[set, fill=blue!20] (I) at (8,0) {};
\node[set, fill=blue!20] (J) at (9,0) {};
\node[set, fill=blue!20] (K) at (10,0) {};
\node[set, fill=blue!20] (L) at (11,0) {};
\node[set, fill=blue!20] (M) at (12,0) {};
\node[set, fill=blue!20] (N) at (13,0) {};
\node[set, fill=blue!20] (O) at (14,0) {};
\node[set, fill=blue!20] (P) at (15,0) {};
\node[set, fill=blue!20] (Q) at (16,0) {};
\node[set, fill=blue!20] (R) at (17,0) {};
\node[set, fill=blue!20] (S) at (18,0) {};
\node[set, fill=blue!20] (T) at (19,0) {};
\node[set, fill=blue!20] (U) at (20,0) {};
\node[set, fill=blue!20] (V) at (21,0) {};
\node[set, fill=blue!20] (W) at (22,0) {};
\node[set, fill=blue!20] (X) at (23,0) {};
\node[set, fill=blue!20] (Y) at (24,0) {};
\node[set, fill=blue!20] (Z) at (25,0) {};
\node[set, fill=blue!20] (A') at (0,1) {};
\node[set, fill=blue!20] (B') at (1,1) {};
\node[set, fill=blue!20] (C') at (2,1) {};
\node[set, fill=blue!20] (D') at (3,1) {};
\node[set, fill=blue!20] (E') at (4,1) {};
\node[set, fill=blue!20] (F') at (5,1) {};
\node[set, fill=blue!20] (G') at (6,1) {};
\node[set, fill=blue!20] (H') at (7,1) {};
\node[set, fill=blue!20] (I') at (8,1) {};
\node[set, fill=blue!20] (J') at (9,1) {};
\node[set, fill=blue!20] (K') at (10,1) {};
\node[set, fill=blue!20] (L') at (11,1) {};
\node[set, fill=blue!20] (M') at (12,1) {};
\node[set, fill=blue!20] (N') at (13,1) {};
\node[set, fill=blue!20] (O') at (14,1) {};
\node[set, fill=blue!20] (P') at (15,1) {};
\node[set, fill=blue!20] (Q') at (16,1) {};
\node[set, fill=blue!20] (R') at (17,1) {};
\node[set, fill=blue!20] (S') at (18,1) {};
\node[set, fill=blue!20] (T') at (19,1) {};
\node[set, fill=blue!20] (U') at (20,1) {};
\node[set, fill=blue!20] (V') at (21,1) {};
\node[set, fill=blue!20] (W') at (22,1) {};
\node[set, fill=blue!20] (X') at (23,1) {};
\node[set, fill=blue!20] (Y') at (24,1) {};
\node[set, fill=blue!20] (Z') at (25,1) {};
\node[set, fill=blue!20] (A'') at (0,2) {};
\node[set, fill=blue!20] (B'') at (1,2) {};
\node[set, fill=blue!20] (C'') at (2,2) {};
\node[set, fill=blue!20] (D'') at (3,2) {};
\node[set, fill=blue!20] (E'') at (4,2) {};
\node[set, fill=blue!20] (F'') at (5,2) {};
\node[set, fill=blue!20] (G'') at (6,2) {};
\node[set, fill=blue!20] (H'') at (7,2) {};
\node[set, fill=blue!20] (I'') at (8,2) {};
\node[set, fill=blue!20] (J'') at (9,2) {};
\node[set, fill=blue!20] (K'') at (10,2) {};
\node[set, fill=blue!20] (L'') at (11,2) {};
\node[set, fill=blue!20] (M'') at (12,2) {};
\node[set, fill=blue!20] (N'') at (13,2) {};
\node[set, fill=blue!20] (O'') at (14,2) {};
\node[set, fill=blue!20] (P'') at (15,2) {};
\node[set, fill=blue!20] (Q'') at (16,2) {};
\node[set, fill=blue!20] (R'') at (17,2) {};
\node[set, fill=blue!20] (S'') at (18,2) {};
\node[set, fill=blue!20] (T'') at (19,2) {};
\node[set, fill=blue!20] (U'') at (20,2) {};
\node[set, fill=blue!20] (V'') at (21,2) {};
\node[set, fill=blue!20] (W'') at (22,2) {};
\node[set, fill=blue!20] (X'') at (23,2) {};
\node[set, fill=blue!20] (Y'') at (24,2) {};
\node[set, fill=blue!20] (Z'') at (25,2) {};
\end{tikzpicture} \qquad (22) $$

$$ (\text{CCP-CCN})(\text{CCN-CH}_{2\pi}) = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7, every node/.style={scale=0.7}] \tikzset{set/.style={circle, draw, fill, minimum size=1.2pt, inner sep=0pt}} \node[set, fill=blue!20] (A) at (0,0) {};
\node[set, fill=blue!20] (B) at (1,0) {};
\node[set, fill=blue!20] (C) at (2,0) {};
\node[set, fill=blue!20] (D) at (3,0) {};
\node[set, fill=blue!20] (E) at (4,0) {};
\node[set, fill=blue!20] (F) at (5,0) {};
\node[set, fill=blue!20] (G) at (6,0) {};
\node[set, fill=blue!20] (H) at (7,0) {};
\node[set, fill=blue!20] (I) at (8,0) {};
\node[set, fill=blue!20] (J) at (9,0) {};
\node[set, fill=blue!20] (K) at (10,0) {};
\node[set, fill=blue!20] (L) at (11,0) {};
\node[set, fill=blue!20] (M) at (12,0) {};
\node[set, fill=blue!20] (N) at (13,0) {};
\node[set, fill=blue!20] (O) at (14,0) {};
\node[set, fill=blue!20] (P) at (15,0) {};
\node[set, fill=blue!20] (Q) at (16,0) {};
\node[set, fill=blue!20] (R) at (17,0) {};
\node[set, fill=blue!20] (S) at (18,0) {};
\node[set, fill=blue!20] (T) at (19,0) {};
\node[set, fill=blue!20] (U) at (20,0) {};
\node[set, fill=blue!20] (V) at (21,0) {};
\node[set, fill=blue!20] (W) at (22,0) {};
\node[set, fill=blue!20] (X) at (23,0) {};
\node[set, fill=blue!20] (Y) at (24,0) {};
\node[set, fill=blue!20] (Z) at (25,0) {};
\node[set, fill=blue!20] (A') at (0,1) {};
\node[set, fill=blue!20] (B') at (1,1) {};
\node[set, fill=blue!20] (C') at (2,1) {};
\node[set, fill=blue!20] (D') at (3,1) {};
\node[set, fill=blue!20] (E') at (4,1) {};
\node[set, fill=blue!20] (F') at (5,1) {};
\node[set, fill=blue!20] (G') at (6,1) {};
\node[set, fill=blue!20] (H') at (7,1) {};
\node[set, fill=blue!20] (I') at (8,1) {};
\node[set, fill=blue!20] (J') at (9,1) {};
\node[set, fill=blue!20] (K') at (10,1) {};
\node[set, fill=blue!20] (L') at (11,1) {};
\node[set, fill=blue!20] (M') at (12,1) {};
\node[set, fill=blue!20] (N') at (13,1) {};
\node[set, fill=blue!20] (O') at (14,1) {};
\node[set, fill=blue!20] (P') at (15,1) {};
\node[set, fill=blue!20] (Q') at (16,1) {};
\node[set, fill=blue!20] (R') at (17,1) {};
\node[set, fill=blue!20] (S') at (18,1) {};
\node[set, fill=blue!20] (T') at (19,1) {};
\node[set, fill=blue!20] (U') at (20,1) {};
\node[set, fill=blue!20] (V') at (21,1) {};
\node[set, fill=blue!20] (W') at (22,1) {};
\node[set, fill=blue!20] (X') at (23,1) {};
\node[set, fill=blue!20] (Y') at (24,1) {};
\node[set, fill=blue!20] (Z') at (25,1) {};
\node[set, fill=blue!20] (A'') at (0,2) {};
\node[set, fill=blue!20] (B'') at (1,2) {};
\node[set, fill=blue!20] (C'') at (2,2) {};
\node[set, fill=blue!20] (D'') at (3,2) {};
\node[set, fill=blue!20] (E'') at (4,2) {};
\node[set, fill=blue!20] (F'') at (5,2) {};
\node[set, fill=blue!20] (G'') at (6,2) {};
\node[set, fill=blue!20] (H'') at (7,2) {};
\node[set, fill=blue!20] (I'') at (8,2) {};
\node[set, fill=blue!20] (J'') at (9,2) {};
\node[set, fill=blue!20] (K'') at (10,2) {};
\node[set, fill=blue!20] (L'') at (11,2) {};
\node[set, fill=blue!20] (M'') at (12,2) {};
\node[set, fill=blue!20] (N'') at (13,2) {};
\node[set, fill=blue!20] (O'') at (14,2) {};
\node[set, fill=blue!20] (P'') at (15,2) {};
\node[set, fill=blue!20] (Q'') at (16,2) {};
\node[set, fill=blue!20] (R'') at (17,2) {};
\node[set, fill=blue!20] (S'') at (18,2) {};
\node[set, fill=blue!20] (T'') at (19,2) {};
\node[set, fill=blue!20] (U'') at (20,2) {};
\node[set, fill=blue!20] (V'') at (21,2) {};
\node[set, fill=blue!20] (W'') at (22,2) {};
\node[set, fill=blue!20] (X'') at (23,2) {};
\node[set, fill=blue!20] (Y'') at (24,2) {};
\node[set, fill=blue!20] (Z'') at (25,2) {};
\end{tikzpicture} \qquad (23) $$

and hence, applying this for all $i$,

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

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

## C Compatibility

Fix $d \ge 2$ and the polycontrolled dagger PROP $CQC_d$ of §2, equipped with control functor $C_k$ for each $k \in \{0, \dots, d-1\}$. In this appendix we prove Theorem 3.2 (§3.3), i.e. the mixed-control compatibility principle (COMPAT in Definition 2.4), inside the equational theory QC$_d$.

Our proof is purely syntactic and uses a normalisation step that will also be reused in Appendix D (commutativity of distinct controls). Throughout we work modulo:

* the strict symmetric monoidal coherence in $CQC_d$ (associativity, unit, symmetry, interchange), so wire permutations can be freely inserted and removed; and

* the coherence laws for each control functor $C_k$ (functoriality, strength, and naturality), so controls can be pushed through structural contexts.
**Algorithm 1** SEPARATE: push parallelism out, isolate single-gate layers with explicit controls

1: **function** SEPARATE(f)

2:     **let** f' := f where we removed swaps using SMC coherence and (S)

3:     **match** f' with

4:         **case** f₁ ⊗ f₂:

5:             **return** (SEPARATE(f₁) ⊗ id<sub>|f₂|</sub>) ◦ (id<sub>|f₁|</sub> ⊗ SEPARATE(f₂))

6:         **case** f₁ ⊗ f₂:

7:             **return** SEPARATE(f₁) ◦ SEPARATE(f₂)

8:         **case** C<sub>m</sub>(f₁):

9:             **match** f₁ with

10:         **case** g ◦ h: **return** SEPARATE(C<sub>m</sub>(g)) ◦ SEPARATE(C<sub>m</sub>(h))

11:     **case** g ⊗ h:

12:         **return** (SEPARATE(C<sub>m</sub>(g)) ⊗ id<sub>|h|</sub>) ◦ (id<sub>1</sub> ⊗ σ<sub>|g|,|h|</sub>) ◦

13:         (SEPARATE(C<sub>m</sub>(h)) ⊗ id<sub>|g|</sub>) ◦ (id<sub>1</sub> ⊗ σ<sub>|h|,|g|</sub>)

14:     **case** $\boxed{H^{(i,j)}}$: **return** SEPARATE(Apply CHDec to rewrite f')

15:         **case** (α): **return** f'

16:     **case** id<sub>n</sub>: **return** id<sub>n+1</sub>

17:     **case** C<sub>n</sub>(g):

18:         **match** g with

19:             **case** (π): **return** f'

20:         **case** (β): **return** SEPARATE(Apply CCPDec to rewrite f')

21:     **case** C<sub>k</sub>((α)): **return** SEPARATE(Apply CCCPDec to rewrite f')

22:     **otherwise return** SEPARATE(C<sub>m</sub>(SEPARATE(f₁)))

23:     **otherwise:** **return** f'

## C.1 Normalisation into controlled layers

The point of this subsection is to isolate a small family of “one-gate layers”, each equipped with an explicit control word. Concretely, we show that every circuit can be rewritten (provably in QC<sub>d</sub>) into a sequential composition of such layers, with all wire permutations made explicit. This normal form is what allows the compatibility argument to reduce to the single axiom (CπS), and the commutativity argument to reduce to a finite table of generator commutations.

**Definition C.1.** An atomic layer is a morphism of the form

$$L := (id_p \otimes G \otimes id_q) : n \to n, \quad G \in \{id_n \mid n \in \mathbb{N}\} \cup \{\theta \mid \theta \in \mathbb{R}\} \cup \{-\boxed{H^{(i,j)}} \mid 0 \le i < j < d\} \cup \{C_k(\theta) \mid k, \theta \in \{C_k(C_l(\pi)) \mid k, l\}\}$$

A controlled layer is any circuit of the form C<sub>u</sub>(L) for a control word u.

If a circuit C is written as a sequential composition of controlled layers

$$C = L_m \circ \dots \circ L_1, \quad L_t = C_{u_t}(id_{p_t} \otimes G_t \otimes id_{q_t}),$$

its control-depth multiset is $cd(C) := \{|u_t| \mid t = 1, \dots, m\}$. We order such multisets by the usual multiset extension of the natural order on $\mathbb{N}$.

We now give an explicit normalisation procedure. Informally, it: (i) eliminates implicit swaps using strict monoidal coherence and the swap decomposition axiom, (ii) pushes ⊗ outward by serialising it into a composition of “upper then lower” actions, and (iii) pushes controls down to generators, expanding controlled composites using the bounded-arity axioms of QC<sub>d</sub>.

**Lemma C.2.** SEPARATE terminates on all inputs *f* and returns a sequential composition

$$SEPARATE(f) = L_m \circ \dots \circ L_1,$$

where each $L_t$ is an atomic layer and all permutations appear only as explicit wire-swaps between such layers.

**PROOF.** Define a well-founded measure on circuits by

$$\mu(f) := (\text{\#of non-identity gates in } f, \sum_{g \text{ gate in } f} \text{control-depth}(g)),$$

ordered lexicographically. Each recursive clause of the definition of SEPARATE either:

* eliminates a tensor node in favour of sequential composition of smaller circuits (strictly reducing the number of non-identity gates in the first component), or
* pushes a control one step closer to a generator and immediately expands a controlled generator using Lemmas CHDEC, CCPDEC and CCCPDEC, which strictly reduces the total nesting depth of non-generator gates.

Functoriality, strength and swap laws are used only to rearrange the diagram and do not increase $\mu$. Hence $\mu$ decreases along every recursive branch, so SEPARATE terminates. By construction, the output is a composition of controlled layers with generator drawn from the stated finite set and with all permutations explicit. □

**Corollary C.3.** Every morphism of $CQC_d$ is provably equal in $QC_d$ to a circuit generated (using only sequential and parallel composition) by

$$ \mathcal{G} = \{ \mathrm{id}_n \mid n \in \mathbb{N} \} \cup \{ (\theta) \mid \theta \in \mathbb{R} \} \cup \{ -[\mathrm{H}^{(i,j)}] - \mid 0 \le i < j < d \} \cup \{ \mathrm{C}_k(\theta) \mid k, \theta \} \cup \{ \mathrm{C}_k(\mathrm{C}_l(\pi)) \mid k, l \} $$

## C.2 Compatibility of mixed controls

We now derive mixed-control compatibility (COMPAT in Definition 2.4) from the finite axiom system $QC_d$, using the normalisation machinery above.

**PROOF OF THEOREM 3.2.** Write $S := \sigma_{1,1} \otimes \mathrm{id}_n : 2 + n \to 2 + n$. Consider the two $(2 + n)$-wire circuits

$$ F_{ab} := \mathrm{C}_a(\mathrm{C}_b(f)), \quad F_{ba} := \mathrm{C}_b(\mathrm{C}_a(f)). $$

Apply the normalisation procedure SEPARATE (Algorithm 1) to $F_{ab}$ and $F_{ba}$. By construction, each rewrite step performed by SEPARATE is justified either by strict PROP coherence, by control-functoriality/strength/naturality, or by one of the bounded-arity axiom schemata of Figures 1-2. Hence $QC_d \vdash F_{ab} = \mathrm{SEPARATE}(F_{ab})$ and $QC_d \vdash F_{ba} = \mathrm{SEPARATE}(F_{ba})$.

Inspecting the clauses of SEPARATE, the only situation in which two nested controls are left *undecomposed* is the branch

$$ \textbf{case } \mathrm{C}_m(\mathrm{C}_n(g)) \textbf{ with } g = (\pi) : \textbf{return} f', $$

i.e. nested control on the scalar $\pi$-phase. All other nested-control cases are immediately expanded using Lemmas CCPDEC and CCCPDEC (and the controlled-Hadamard decompositions), so that in $\mathrm{SEPARATE}(F_{ab})$ and $\mathrm{SEPARATE}(F_{ba})$ the only atomic layers that can simultaneously involve the two outer control wires are instances of the doubly-controlled $\pi$-phase $\mathrm{C}_a(\mathrm{C}_b(\pi))$ (possibly tensored with identity on untouched wires).

We now push the swap $S$ through the sequential decomposition $\mathrm{SEPARATE}(F_{ab})$ from right to left. For any layer that acts on at most one of the two outer control wires, this is pure strict symmetric-monoidal coherence (naturality of $\sigma$). For a layer equal to $\mathrm{C}_a(\mathrm{C}_b(\pi))$ on the two outer control wires, the required step is exactly the axiom schema $(C\pi S)$, i.e. (CompP). Thus we can rewrite

$$ \mathrm{SEPARATE}(F_{ab}) \circ S = S \circ \mathrm{SEPARATE}(F_{ba}) $$

in $QC_d$. Finally, replacing $\mathrm{SEPARATE}(F_{ab})$ by $F_{ab}$ and $\mathrm{SEPARATE}(F_{ba})$ by $F_{ba}$ using the equalities above yields $F_{ab} \circ S = S \circ F_{ba}$, as required. □

## D Commutativity

Fix $d \ge 2$ and the polycontrolled dagger PROP $CQC_d$ of §2. In this appendix we prove Theorem 3.3 (§3.3), i.e. that circuits controlled on *distinct* computational-basis values commute.

As in Appendix C, we work modulo strict symmetric monoidal coherences and the coherence laws of each control functor. We will use the finite generating family $\mathcal{G}$ obtained by the normalisation procedure SEPARATE (Corollary C.3) to reduce the commutativity statement to a finite list of generator-level commutations.

**PROOF OF THEOREM 3.3.** By Corollary C.3 and SMC coherence we may assume that

$$ f = \mathrm{id}_p \otimes f' \otimes \mathrm{id}_{n-n_f-p}, \quad g = \mathrm{id}_q \otimes g' \otimes \mathrm{id}_{n-n_g-q}, $$

with $f' : n_f \to n_f$ and $g' : n_g \to n_g$ belonging to $\mathcal{G}$, and where $0 \le p \le q$. If $q - p > n_f$, we can insert a symmetry $\mathrm{id}_p \otimes \sigma_{n_f, q-p-n_f} \otimes \mathrm{id}_{n-q}$ on both sides of the desired equation to reduce to the case $q - p \le n_f$. Thus we only need to consider the relative offset $i := q - p \in \{0, \dots, n_f\}$. If $g' = \mathrm{id}_{n_g}$ then $\mathrm{C}_l(g)$ is the identity and the statement is trivial, so we exclude this case in the table below.

The remaining possibilities are summarised in the following table, where each non-trivial entry cites the derived commutation lemma used to swap the two layers in question (all equations are proved in Appendix B).
<table><thead><tr><th></th><th>f' = id<sub>n</sub></th><th>f' = (θ)</th><th>f' = C<sub>i</sub>((θ))</th><th>f' = C<sub>i</sub>(C<sub>j</sub>((π)))</th><th>f' = —[H<sup>(i,j)</sup>—]</th></tr></thead><tbody><tr><td>g' = id<sub>m</sub></td><td>trivial</td><td>trivial</td><td>trivial</td><td>trivial</td><td>trivial</td></tr><tr><td>g' = (Y)</td><td></td><td>i = 0: (PPc)</td><td>i = 0: (CCP-CP)</td><td>i = 0: (CCN-CP)</td><td>i = 0: (CH-CP)</td></tr><tr><td rowspan="2">g' = C<sub>k</sub>((Y))</td><td></td><td></td><td>i = 0: (CCP-CCP)</td><td>i = 0: (CCP-CCN)</td><td>i = 0: (HPc)</td></tr><tr><td></td><td></td><td>i = 1: (CCP-CCP<sub>‡</sub>)</td><td>i = 1: (CCN-CP<sub>‡</sub>)</td><td>i = 1: (CCP-CH<sub>‡</sub>)</td></tr><tr><td rowspan="3">g' = C<sub>k</sub>(C<sub>ℓ</sub>((π)))</td><td></td><td></td><td></td><td>i = 0: (CCN-CCN)</td><td>i = 0: (HCc)</td></tr><tr><td></td><td></td><td></td><td>i = 1: (CCN-CCN<sub>3</sub>)</td><td>i = 1: (CCN-CH<sub>2π</sub>)</td></tr><tr><td></td><td></td><td></td><td>i = 2: (CCN-CCN<sub>4</sub>)</td><td>i = 2: (CCN-CH<sub>‡</sub>)</td></tr><tr><td>g' = —[H<sup>(k,l)</sup>—]</td><td></td><td></td><td></td><td></td><td>i = 0: (HHc)</td></tr><tr><td></td><td></td><td></td><td></td><td></td><td>i = 1: (CH-CH<sub>‡</sub>)</td></tr></tbody></table>

Each cited lemma states precisely that the corresponding pair of controlled generators commutes for the indicated value of the offset i. Tensoring with identities on the untouched wires and inserting coherence isomorphisms as needed yields

$$C_k(f) \circ C_l(g) = C_l(g) \circ C_k(f)$$

for each of the finitely many generator pair. Since arbitrary circuits are built from these generators by sequential and parallel composition, and $C_k$ is a strict monoidal functor, the general case follows. □

## E Exhaustivity

In this appendix we prove Theorem 3.4 (§3.3), i.e. that the family of control functors $(C_k)_{k=0}^{d-1}$ is exhaustive.

**PROOF OF THEOREM 3.4.** Using the swap decomposition axiom (S) together with strict symmetric-monoidal coherence, we may assume $f$ is presented without explicit swap generators. We then prove the claim by structural induction on $f$.

Let $E(f)$ denote the equation

$$\prod_{k=0}^{d-1} C_k(f) = — \otimes f.$$

We prove $E(f)$ for all circuits $f$ by structural induction on $f$ using the generators and operations of $\mathbf{CQC}_d$.

**Base cases.** For the monoidal unit and a single wire we have

$$\prod_{k=0}^{d-1} C_k(\underbrace{\phantom{\Gamma}}_{\Gamma}) = — = — \otimes \underbrace{\phantom{\Gamma}}_{\Gamma},$$

$$\prod_{k=0}^{d-1} C_k(—) = \mathrm{id}_2 = — \otimes —,$$

so $E(\underbrace{\phantom{\Gamma}}_{\Gamma})$ and $E(—)$ hold. Since $\mathrm{id}_n \cong —^{\otimes n}$, the general identity case follows from the tensor step below.

For a scalar phase $(\theta)$, the total phase axiom (TP) gives

$$\prod_{k=0}^{d-1} C_k(\underbrace{\theta}_{\theta}) \stackrel{(\mathrm{TP})}{=} — \otimes \underbrace{\theta}_{\theta},$$

so $E(\underbrace{\theta}_{\theta})$ holds.

For a two-level Hadamard $—[H^{(i,j)}—]$ the total Hadamard equation (TH) yields

$$\prod_{k=0}^{d-1} C_k(—[H^{(i,j)}—]) \stackrel{(\mathrm{TH})}{=} — \otimes —[H^{(i,j)}—],$$

so $E(—[H^{(i,j)}—])$ holds.

**Sequential composition.** Assume $E(g)$ and $E(h)$. By functoriality of each $C_k$ we have $C_k(g \circ h) = C_k(g) \circ C_k(h)$, hence

$$\prod_{k=0}^{d-1} C_k(g \circ h) = \prod_{k=0}^{d-1} (C_k(g) \circ C_k(h)).$$

Using commuting controls (Theorem 3.3), we can reorder the factors so that all $C_k(g)$ appear to the left of all $C_k(h)$:

$$\prod_{k=0}^{d-1} (C_k(g) \circ C_k(h)) \stackrel{\text{Theorem 3.3}}{=} \prod_{k=0}^{d-1} C_k(g) \circ \prod_{k=0}^{d-1} C_k(h).$$
By the induction hypothesis,

$$ \prod_{k=0}^{d-1} C_k(g) = - \otimes g, $$

$$ \prod_{k=0}^{d-1} C_k(h) = - \otimes h, $$

and therefore

$$ \prod_{k=0}^{d-1} C_k(g \circ h) = (- \otimes g) \circ (- \otimes h) = - \otimes (g \circ h), $$

so $E(g \circ h)$ holds.

**Parallel composition.** Assume $E(g)$ and $E(h)$. Using the definition of $C_k$ as a strict monoidal endofunctor together with the strength/coherence laws, a controlled tensor can be written (up to symmetry) as

$$ C_k(g \otimes h) = (C_k(g) \otimes \mathrm{id}_{|g|}) \circ (- \otimes \sigma_{|g|,|h|}) \circ (C_k(h) \otimes \mathrm{id}_{|g|}) \circ (- \otimes \sigma_{|h|,|g|}). $$

Hence

$$ \prod_{k=0}^{d-1} C_k(g \otimes h) = \prod_{k=0}^{d-1} \left( (C_k(g) \otimes \mathrm{id}_{|h|}) \circ (- \otimes \sigma_{|g|,|h|}) \circ (C_k(h) \otimes \mathrm{id}_{|g|}) \circ (- \otimes \sigma_{|h|,|g|}) \right) $$

$$ \stackrel{\text{Theorem 3.3}}{=} \prod_{k=0}^{d-1} (C_k(g) \otimes \mathrm{id}_{|h|}) \circ (- \otimes \sigma_{|g|,|h|}) \circ \prod_{k=0}^{d-1} (C_k(h) \otimes \mathrm{id}_{|g|}) \circ (- \otimes \sigma_{|h|,|g|}). $$

Applying the induction hypothesis pointwise and using monoidality of $- \otimes -$,

$$ \prod_{k=0}^{d-1} C_k(g \otimes h) = (- \otimes g \otimes \mathrm{id}_{|h|}) \circ (- \otimes \sigma_{|g|,|h|}) \circ (- \otimes h \otimes \mathrm{id}_{|g|}) \circ (- \otimes \sigma_{|h|,|g|}) = - \otimes (g \otimes h), $$

so $E(g \otimes h)$ holds.

**Nested control.** Finally, suppose $E(g)$ holds and consider $C_m(g)$. Using compatibility of mixed controls (Theorem 3.2), nested controls may be exchanged at the cost of a swap:

$$ C_k(C_m(g)) = (\sigma_{1,1} \otimes \mathrm{id}_{|g|}) \circ C_m(C_k(g)) \circ (\sigma_{1,1} \otimes \mathrm{id}_{|g|}). $$

Hence

$$ \prod_{k=0}^{d-1} C_k(C_m(g)) = (\sigma_{1,1} \otimes \mathrm{id}_{|g|}) \circ \prod_{k=0}^{d-1} C_m(C_k(g)) \circ (\sigma_{1,1} \otimes \mathrm{id}_{|g|}) $$

$$ = (\sigma_{1,1} \otimes \mathrm{id}_{|g|}) \circ C_m \left( \prod_{k=0}^{d-1} C_k(g) \right) \circ (\sigma_{1,1} \otimes \mathrm{id}_{|g|}) $$

$$ \stackrel{\mathrm{E}(g)}{=} (\sigma_{1,1} \otimes \mathrm{id}_{|g|}) \circ C_m(- \otimes g) \circ (\sigma_{1,1} \otimes \mathrm{id}_{|g|}). $$

By functoriality and coherence of $C_m$, the right-hand side is precisely $- \otimes C_m(g)$, so $E(C_m(g))$ holds.

**Corollary E.1.** Since we can write the swap gate using the generators above (Equation (S)), $E(\sigma_{m,n})$ also holds, and the previous lemma extends to all circuits in $CQC_d$.

Since every circuit in $CQC_d$ is built from the above generators by sequential composition, tensor product, and (nested) control, the property $E(f)$ holds for all $f$, completing the proof. □

The exhaustivity property says that the collection of projectors $(|k\rangle \langle k|)^{d-1}_{k=0}$ on the control wire forms a partition of the identity, which is reflected syntactically by the equation of Theorem 3.4. As a useful consequence, controlled operations are stable under conjugation on the target system.

# F Further derived identities

Throughout this appendix we work in the equational theory $QC_d$, and write $QC_d \vdash C_1 = C_2$ when the circuit identity $C_1 = C_2$ is derivable from the axioms of Figures 1–2
<figure><img src="image_79.png" /><figcaption>Figure 6: Derived rules in QC<sub>d</sub> (batch 4).</figcaption></figure>

<figure><img src="image_80.png" /><figcaption>Figure 7: Derived rules in QC<sub>d</sub> (batch 5).</figcaption></figure>

## F.1 Catalogue of derived rules

## F.2 Proofs of the derived rules

PROOF OF (H-CCP).

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

PROOF OF (CH-HC). We treat the case $i, j, k$ pairwise distinct; the case with $ℓ, m, n$ is analogous.

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

☐

PROOF OF (CX-HC). Again consider $i, j, k$ pairwise distinct; the case with $ℓ, m, n$ is analogous.

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

□

**F.2.1** A π-normalisation lemma (choosing the split parameter x). In the proof of (EULERB) we introduce an auxiliary real parameter x (by splitting a middle rotation/phase into two pieces x and α₂ − x). This produces a family of circuit identities indexed by x, in which the angles βᵢ(x) and γᵢ(x) produced by the Euler-extraction depend on x (while the input angles α₁, α₂, α₃ are fixed).

To continue the purely diagrammatic part of the derivation, we need one additional property: we can choose a value x₀ such that the bridge phase β₃(x₀) + γ₀(x₀) is a multiple of π. Since angles are always understood modulo 2π, this means that β₃(x₀) + γ₀(x₀) is either 0 or π modulo 2π, which is exactly what justifies the two cases treated in the proof of (EULERB).

**Lemma F.1** (Existence of a π-normalised split [32]). Fix α₁, α₂, α₃ ∈ ℝ and consider the continuous function N : [-π/2, π/2] → ℝ defined by

$$N(x) := \sin(\alpha_1) \cos(x) \cos(\alpha_3) + \cos(\alpha_1) \sin(\alpha_3) \cos(\alpha_2 - x).$$

Then their exists x₀ ∈ [-π/2, π/2] such that N(x₀) = 0.

Moreover, in the Euler-extraction step used in the proof of (EULERB), the corresponding bridge phase satisfies

$$\beta_3(x_0) + \gamma_0(x_0) \in \pi\mathbb{Z},$$

hence (modulo 2π) we necessarily have β₃(x₀) + γ₀(x₀) ≡ 0 or ≡ π.

**PROOF.** First note that

$$N(-\frac{\pi}{2}) = \cos(\alpha_1) \sin(\alpha_3) \cos(\alpha_2 + \frac{\pi}{2}) = -\cos(\alpha_1) \sin(\alpha_3) \sin(\alpha_2),$$

while

$$N(\frac{\pi}{2}) = \cos(\alpha_1) \sin(\alpha_3) \cos(\alpha_2 - \frac{\pi}{2}) = \cos(\alpha_1) \sin(\alpha_3) \sin(\alpha_2).$$

Hence N(-π/2) = -N(π/2), so N(-π/2) · N(π/2) ≤ 0. By continuity of N, the intermediate value theorem yields x₀ ∈ [-π/2, π/2] with N(x₀) = 0.

For the second part, recall how the angles β₃(x) and γ₀(x) are obtained: they arise from solving the trigonometric matching conditions that identify the two sides of the Euler-extraction step (equivalently: matching the corresponding 2 × 2 blocks on the relevant two-dimensional subspace). A standard calculation shows that the tangent of the bridge sum β₃(x) + γ₀(x) can be written as a ratio

$$\tan(\beta_3(x) + \gamma_0(x)) = \frac{N(x)}{D(x)}$$

for some real-valued continuous denominator D(x) (the explicit shape of D is irrelevant here; it is the usual t-addition denominator and is continuous wherever the extraction is defined). At x = x₀ we have N(x₀) = 0, hence tan(β₃(x₀) + γ₀(x₀)) = 0, which implies β₃(x₀) + γ₀(x₀) ∈ πℝ. Reducing modulo 2π gives the claimed dichotomy ≡ 0 or ≡ π. □

**Remark 4.** The lemma only provides existence (not uniqueness) of a suitable x₀, and any such choice is valid for the subsequent diagrammatic derivation. Operationally, this is the only point in the proof where we appeal to a small analytic argument; once x₀ is fixed, the remainder proceeds purely by the equational rules of QC₃.
PROOF OF (EULERB).

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

Choose $x_0$ as in Lemma F.1, so that $\beta_3(x_0) + \gamma_0(x_0) \in \pi\mathbb{Z}$. Working modulo $2\pi$, there are two cases: (i) $\beta_3(x_0) + \gamma_0(x_0) \equiv 0$, and (ii) $\beta_3(x_0) + \gamma_0(x_0) \equiv \pi$. We treat these cases separately below.

$$ \text{Case } \beta_3 + \gamma_0 = 0. $$

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

$$ \text{Case } \beta_3 + \gamma_0 = \pi. $$

<figure><img src="image_87.png" /></figure>
$$ = \boxed{\begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}]
    \node[draw, circle, fill=white, inner sep=1.2pt] (center) at (0,0) {};
    \node[draw, circle, fill=white, inner sep=1.2pt] (left) at (-1.5,0) {};
    \node[draw, circle, fill=white, inner sep=1.2pt] (right) at (1.5,0) {};
    \node[draw, circle, fill=white, inner sep=1.2pt] (top) at (0,1.5) {};
    \node[draw, circle, fill=white, inner sep=1.2pt] (bottom) at (0,-1.5) {};
    \node at (center) {$\beta_0$};
    \node at (left) {$\beta_1$};
    \node at (right) {$\beta_2$};
    \node[above=0.2cm of center] {$\beta'$};
    \node[below=0.2cm of center] {$\gamma'$};
    \node[above=0.2cm of right] {$\gamma$};
    \node[below=0.2cm of left] {$\phi$};
    \node[above=0.2cm of top] {$\phi + \gamma_3$};
    \node[below=0.2cm of top] {$\phi + \gamma_1 + \pi$};
\end{tikzpicture}} $$

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

PROOF OF (EULER).

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

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

## G Details of the GrayLift/Gray-Code Encoding

This appendix spells out two concrete raw-LOPP constructions used by the contextual encoding of Section 4.3:

(1) an explicit d-mode LOPP circuit $B_d^{(i,i+1)}$ whose single-photon semantics is the adjacent two-level Hadamard $H_d^{(i,i+1)}$; and

(2) the GrayLift operators $\text{GrayLift}_d^P(-)$ and $j\text{GrayLift}_d^P(-)$, which replicate a local LOPP subcircuit across Gray-coded mode blocks, inserting a mirror operation on blocks where the reflected d-ary Gray order runs the relevant suffix in reverse.

The main text use only the semantic interface properties of these gadgets (such as how they decode); the particular raw implementations here are simply one convenient choice.

### G.1 A single-qudit network for $H_d^{(i,i+1)}$

Fix $d \ge 2$ and $i \in \{0, \dots, d-2\}$. Recall that in the encoding we need a local LOPP circuit on $d$ modes which, under the single-photon semantics, acts like the qudit gate that mixes exactly two adjacent levels and leaves all other levels untouched.

Concretely, let $H := \frac{1}{\sqrt{2}}(\begin{smallmatrix} 1 & 1 \\ 1 & -1 \end{smallmatrix}) \in U(2)$ be the usual $2 \times 2$ Hadamard. We define the adjacent two-level Hadamard $H_d^{(i,i+1)} \in U(d)$ by

$$ H_d^{(i,i+1)} := I_i \oplus H \oplus I_{d-i-2}. $$

Thus $H_d^{(i,i+1)}$ acts non-trivially only on the two-dimensional subspace $\text{span}\{|i\rangle, |i+1\rangle\}$, and is the identity on all other computational basis vectors. In particular:

* when $d=2$ and $i=0$, this is just the ordinary Hadamard $H$;

* when $d=3$ and $i=1$, it mixes modes 1 and 2 while leaving mode 0 unchanged.

Write $P(\phi) : 1 \to 1$ for the LOPP phase-shifter generator of angle $\phi$, and $B(\theta) : 2 \to 2$ for the LOPP beam-splitter generator of angle $\theta$ (as in Theorem 4.2). We consider the following 2-mode interferometer:

$$ H_{BS} := (\text{id}_1 \otimes P(-\pi/2)) \circ B(\pi/4) \circ (\text{id}_1 \otimes P(-\pi/2)) : 2 \to 2. $$

Intuitively, $B(\pi/4)$ is the standard 50/50 beam splitter (in our phase convention), and the surrounding phase shifters correct the relative phases so that the overall transformation is exactly the real Hadamard matrix in the mode basis. This is the simplest way to implement a real $2 \times 2$ Hadamard using the complex-valued beam-splitter convention of Theorem 4.2.

We then place $H_{BS}$ on modes $i, i+1$ inside a d-mode circuit:

$$ B_d^{(i,i+1)} := \text{id}_i \otimes H_{BS} \otimes \text{id}_{d-i-2} : d \to d. $$

Operationally, if a single photon enters in mode $i$, then $B_d^{(i,i+1)}$ outputs an equal-amplitude superposition over modes $i$ and $i+1$; if it enters in mode $i+1$, the superposition has a relative minus sign; and all other modes are transmitted unchanged.

**Lemma G.1.** For each $d \ge 2$ and $0 \le i \le d-2$, the circuit $B_d^{(i,i+1)}$ is a raw LOPP term built only from phase shifters, beam splitters, and identities, and its single-photon semantics satisfies

$$ \left[ B_d^{(i,i+1)} \right]_{\text{sp}} = H_d^{(i,i+1)} \in U(d). $$

PROOF. Under $\llbracket - \rrbracket_{\text{sp}}$, the phase shifter $P(\phi)$ acts as $[e^{i\phi}]$ on the corresponding mode, so $\llbracket \text{id}_1 \otimes P(\phi) \rrbracket_{\text{sp}} = \text{diag}(1, e^{i\phi})$ on 2 modes. The beam splitter has matrix

$$ \llbracket B(\theta) \rrbracket_{\text{sp}} = \begin{pmatrix} \cos(\theta) & \text{i}\sin(\theta) \\ \text{i}\sin(\theta) & \cos(\theta) \end{pmatrix}. $$
For $\theta = \pi/4$ and $\phi = -\pi/2$ we have $\cos(\pi/4) = \sin(\pi/4) = 1/\sqrt{2}$ and $e^{i\phi} = e^{-i\pi/2} = -i$, so

$$[H_{BS}]_{sp} = \operatorname{diag}(1, -i) \cdot \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & i \\ i & 1 \end{pmatrix} \cdot \operatorname{diag}(1, -i) = \frac{1}{\sqrt{2}} \begin{pmatrix} 1 & 1 \\ 1 & -1 \end{pmatrix} = H.$$

Since parallel composition in **LOPP** is interpreted as block-diagonal direct sum on disjoint mode blocks, we have

$$[\mathrm{id}_i \otimes H_{BS} \otimes \mathrm{id}_{d-i-2}]_{\mathrm{sp}} = I_i \oplus H \oplus I_{d-i-2} = H_d^{(i,i+1)}.$$

□

## G.2 Alternating mirror symmetry on Gray-coded modes

We now define the GrayLift gadgets used in the encoding, namely the operators $\text{GrayLift}_d^p(-)$ and $\text{jGrayLift}_d^p(-)$ introduced informally in Section 4.3. Their role is easiest to understand by thinking in terms of Gray-coded blocks.

Fix $d \ge 2$ and $n \ge 1$. The reflected $d$-ary Gray code $G_n^d$ (Definition 4.4) orders the $d^n$ basis words in $[d]^n$ so that consecutive words differ in one digit by $\pm 1$. This ordering has a crucial structural feature: if we fix a prefix $u \in [d]^{n-1}$ and vary only the last digit, the $d$ words $u_0, u_1, \dots, u(d-1)$ appear consecutively in Gray order, but they appear either in increasing order or in decreasing order depending on how the reflected recursion traverses that prefix. For example:

* for $d = 2, n = 2$, the reflected Gray order is 00, 01, 11, 10: the block with prefix 0 lists last digits as 0, 1, while the block with prefix 1 lists last digits as 1, 0;

* for $d = 3, n = 2$, the reflected Gray order is 00, 01, 02, 12, 11, 10, 20, 21, 22: prefixes 0 and 2 list last digits as 0, 1, 2, while prefix 1 lists them as 2, 1, 0.

In the encoding, we often want to take a local **LOPP** circuit $C$ acting on a block of $d^m$ consecutive modes (representing the Gray traversal of some suffix register) and apply that same logical action uniformly for every fixed configuration of some surrounding digits. Because the Gray traversal flips direction on certain branches, “the same logical action” sometimes corresponds to applying $C$ and sometimes to applying a mirrored copy of $C$, where the order of the modes inside that block is reversed. The GrayLift operators implement exactly this systematic replication-with-optional-mirroring.

**Definition G.2.** For each $r \ge 0$, let $\rho_r : 1^{\otimes d^r} \to 1^{\otimes d^r}$ be the **LOPP** permutation circuit that reverses the order of the $d^r$ modes: on the single-photon basis $\{|0\rangle, \dots, |d^r - 1\rangle\}$ it acts by $\rho_r |k\rangle = |d^r - 1 - k\rangle$.

For any raw **LOPP** circuit $C: 1^{\otimes d^r} \to 1^{\otimes d^r}$, define its mirror by $\text{Rev}(C) := \rho_r \circ C \circ \rho_r^{-1}$.

Since $\rho_r$ is an involutive permutation, $\rho_r^{-1} = \rho_r$. Equivalently, at the matrix level, $\text{Rev}(C)$ conjugates $[C]_{sp}$ by the reversal permutation matrix.

For $q \in [d]$, set

$$\text{Rev}^q(C) := \begin{cases} C & \text{if } q \text{ is even,} \\ \text{Rev}(C) & \text{if } q \text{ is odd.} \end{cases}$$

This parity test matches the reflected recursion in the Gray code: odd leading digits reverse the traversal of the suffix.

**Definition G.3.** Fix $d \ge 2$, let $m \ge 0$, and let $C: 1^{\otimes d^m} \to 1^{\otimes d^m}$ be a raw **LOPP** circuit. For each $p \ge 0$ define a raw **LOPP** circuit

$$\text{GrayLift}_d^p(C) : 1^{\otimes d^{m+p}} \to 1^{\otimes d^{m+p}}$$

recursively by

$$\text{GrayLift}_d^0(C) := C, \quad \text{GrayLift}_d^{p+1}(C) := \bigotimes_{q=0}^{d-1} \text{Rev}^q(\text{GrayLift}_d^p(C)).$$

Fix also $j \in [d]$. Define the controlled GrayLift $j\text{GrayLift}_d^p(C) : 1^{\otimes d^{m+1+p}} \to 1^{\otimes d^{m+1+p}}$ recursively by

$$j\text{GrayLift}_d^0(C) := \bigotimes_{q=0}^{d-1} \text{Rev}^q(C^{(q)}), \quad C^{(q)} := \begin{cases} C & \text{if } q = j, \\ \text{id}_{d^m} & \text{if } q \neq j, \end{cases}$$

and

$$j\text{GrayLift}_d^{p+1}(C) := \bigotimes_{q=0}^{d-1} \text{Rev}^q(j\text{GrayLift}_d^p(C)).$$

The recursion is best read as “one more surrounding digit”. At level $p+1$, we split the $d^{m+p+1}$ mode into $d$ consecutive blocks of size $d^{m+p}$, indexed by the new leading digit $q \in [d]$. On each block, we place a copy of the previous lift $\text{GrayLift}_d^p(C)$, but mirrored when $q$ is odd.

Two small expansions illustrate the pattern. For $p=1$ we have

$$\text{GrayLift}_d^1(C) = \text{Rev}^0(C) \otimes \text{Rev}^1(C) \otimes \dots \otimes \text{Rev}^{d-1}(C),$$

so for $d=2$ this is $C \otimes \text{Rev}(C)$, and for $d=3$ this is $C \otimes \text{Rev}(C) \otimes C$.
For $p = 0$, the controlled lift is already informative:

$$j\text{GrayLift}_d^0(C) = \text{Rev}^0(C^{(0)}) \otimes \text{Rev}^1(C^{(1)}) \otimes \dots \otimes \text{Rev}^{d-1}(C^{(d-1)}),$$

so it places a single (possibly mirrored) copy of $C$ on the $j$-th block and identities elsewhere. For example, for $d = 3$ and $j = 1$ we get $j\text{GrayLift}_3^0(C) = \text{id} \otimes \text{Rev}(C) \otimes \text{id}$, reflecting the fact that the $q = 1$ Gray branch is traversed in reverse order.

The next lemma isolates the combinatorial feature of Gray order that makes GrayLift correct: fixing a prefix produces a contiguous block of indices, and within that block the last digit runs either forward or backward.

**Lemma G.4.** Fix $d \ge 2$ and $n \ge 0$. For each word $u \in [d]^n$, they're exist an index $s(u)$ with $0 \le s(u) \le d^{n+1} - d$ and a sign $\epsilon(u) \in \{+1, -1\}$ such that

$$\{t \in \{0, \dots, d^{n+1} - 1\} \mid G_{n+1}^d(t) \text{ has prefix } u\} = \{s(u), s(u) + 1, \dots, s(u) + d - 1\},$$

and for every $r \in \{0, \dots, d-1\}$ we have

$$G_{n+1}^d(s(u) + r) = \begin{cases} u r & \text{if } \epsilon(u) = +1, \\ u (d-1-r) & \text{if } \epsilon(u) = -1, \end{cases}$$

where $u r$ denotes concatenation of the word $u$ with the digit $r$.

Moreover, one may take $\epsilon$ to be the unique function $\epsilon : [d]^* \to \{\pm 1\}$ defined by $\epsilon(\epsilon) = +1$ and

$$\epsilon(qu) = \begin{cases} \epsilon(u) & \text{if } q \text{ is even,} \\ -\epsilon(u) & \text{if } q \text{ is odd.} \end{cases}$$

In particular, $\epsilon(u)$ flips sign exactly once for each odd digit encountered when reading $u$ from left to right.

**PROOF.** We prove the block statement and the recursion for $\epsilon$ simultaneously by induction on $n$.

Base case $n = 0$: we have $u = \epsilon$ and $G_1^d(t) = (t)$ for $0 \le t < d$, so we may take $s(\epsilon) = 0$ and $\epsilon(\epsilon) = +1$.

Inductive step: let $n \ge 1$ and write $u = qv$ with $q \in [d]$ and $v \in [d]^{n-1}$. Any $t \in \{0, \dots, d^{n+1} - 1\}$ can be written uniquely as $t = q \cdot d^n + r$ with $0 \le r < d^n$.

If $q$ is even, then by Theorem 4.4 we have $G_{n+1}^d(qd^n + r) = q \cdot G_n^d(r)$. Thus $G_{n+1}^d(qd^n + r)$ has prefix $qv$ iff $G_n^d(r)$ has prefix $v$. By the induction hypothesis, the set of such $r$ is an interval of length $d$, hence so is the set of such $t$, with the same last-digit direction. This corresponds to setting $\epsilon(qv) = \epsilon(v)$.

If $q$ is odd, then $G_{n+1}^d(qd^n + r) = q \cdot G_n^d(d^n - 1 - r)$. Put $r' := d^n - 1 - r$. By the induction hypothesis, the set of $r'$ for which $G_n^d(r')$ has prefix $v$ is an interval $[a, a + d - 1]$. Its image under $r = d^n - 1 - r'$ is the interval $[d^n - d - a, d^n - 1 - a]$, again of length $d$. Since the map $r' \mapsto d^n - 1 - r'$ reverse order, the last digit is traversed in the opposite direction on this block; this corresponds to setting $\epsilon(qv) = -\epsilon(v)$. $\square$

The takeaway of Theorem G.4 is that each fixed prefix $u$ determines a single contiguous mode block of length $d$ in which only the last digit varies, and it varies either as $0, 1, \dots, d-1$ or as $d-1, d-2, \dots, 0$. This is exactly the reason the GrayLift recursion toggles mirroring when a leading digit is odd: it ensures that, once we identify modes with basis words in reflected Gray order, every lifted copy of a local subcircuit acts on its intended suffix register with the same logical orientation.

## H Encoding and Decoding

In this appendix we prove Theorem 4.17 (encoding/decoding retraction). Recall that $E_\ell^k$ is the contextual encoding (Definition 4.8), and $D_n^t$ is the contextual decoding (Definition 4.11). The theorem states that for every $C : n \to n$ in $\mathbf{CQC}_d$ and every context size $k, \ell \ge 0$, decoding the encoded circuit recovers $C$ padded by identities:

$$QC_d \vdash D_{k+n+\ell}^0 (E_\ell^k(C)) = \text{id}_k \otimes C \otimes \text{id}_\ell.$$

It is helpful to keep in mind what this statement is saying operationally. The encoding $E_\ell^k$ turns an $n$-qudit circuit into a $d^{k+n+\ell}$-mode single-photon optical circuit by using the reflected $d$-ary Gray ordering of computational basis states. The decoding $D_n^t$ goes the other way: it reads a local optical generator acting on one mode (a phase shifter) or two consecutive modes (a swap or a beam splitter) as a qudit operation supported on one two-dimensional subspace of $\mathcal{H}_n$, controlled on the surrounding Gray digits. Because $\otimes$ means tensor product on qudits but direct sum on optics, both translations are forced to be context-sensitive and to serialise tensor products. The retraction theorem is the formal statement that these design choices are coherent: once the surrounding context is fixed, encoding and decoding cancel each other exactly (up to the expected identity padding on context wires).

The proof proceeds in three steps:

(1) we analyse how $D_n^t$ behaves on a contiguous Gray-code block corresponding to a fixed value of the most significant qudit;

(2) we apply this to the alternating mirror-symmetry networks $\text{GrayLift}_d$ and $j\text{GrayLift}_d$, which are the basic optical “lifting gadgets” used in the encoding;

(3) we conclude by a structural induction on circuits in $\mathbf{CQC}_d$.
## H.1 Decoding a fixed Gray-code block

The key combinatorial fact is that, in reflected *d*-ary Gray order, mode indices are grouped into blocks according to the first Gray digit. Fix $a \ge 0$. The $d^{a+1}$ mode labels split into *d* consecutive blocks of length $d^a$:

$$ \{0, \dots, d^a - 1\}, \{d^a, \dots, 2d^a - 1\}, \dots, \{(d-1)d^a, \dots, d^{a+1} - 1\}, $$

and these blocks correspond to leading Gray digit $j = 0, 1, \dots, d-1$. Inside the block for a fixed $j$, every Gray word has prefix $j$, so one expects every decoded generator to acquire an outer $C_j$. The only subtlety is that the reflected Gray code traverses odd blocks in reverse order. For example, when $d=3$ and $a=1$ (so we are looking at words of length 2), the reflected Gray order is

$$ 00, 01, 02, \ 12, 11, 10, \ 20, 21, 22, $$

so the $j=0$ block is forward, the $j=1$ block is reversed, and the $j=2$ block is forward again. The next two lemmas formalise exactly how decoding behaves in the forward and reversed cases.

**Lemma H.1.** Let $C$ be a **LOPP** circuit acting on $\ell$ consecutive modes, and fix $a \ge 0$ and $s$ with $s + \ell \le d^a$. For every even $j \in \{0, \dots, d-1\}$ we have

$$ D_{a+1}^{d^a j+s}(C) = C_j(D_a^s(C)). $$

*PROOF.* We argue by structural induction on $C$. The intuition is that, for even $j$, the Gray code factors on that block as

$$ G_{a+1}^{d}(d^{a}j + t) = j \cdot G_{a}^{d}(t), $$

so every decoded generator is the usual decoding at the smaller size $a$, wrapped in a $j$-control.

Empty and identity. If $C$ is the empty diagram $\begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}] \draw[thick] (-.5,0) -- (0,0); \draw[thick] (0,0) -- (.5,0); \draw[thick] (0,0) -- (0,.5); \draw[thick] (0,0) -- (0,-.5); \draw[thick] (0,0) -- (0,1); \draw[thick] (0,0) -- (0,-1); \draw[thick] (0,0) -- (0,2); \draw[thick] (0,0) -- (0,-2); \draw[thick] (0,0) -- (0,3); \draw[thick] (0,0) -- (0,-3); \end{tikzpicture}$ or a single wire $\begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}] \draw[thick] (-.5,0) -- (0,0); \draw[thick] (0,0) -- (.5,0); \draw[thick] (0,0) -- (0,.5); \draw[thick] (0,0) -- (0,-.5); \draw[thick] (0,0) -- (0,1); \draw[thick] (0,0) -- (0,-1); \draw[thick] (0,0) -- (0,2); \draw[thick] (0,0) -- (0,-2); \draw[thick] (0,0) -- (0,3); \draw[thick] (0,0) -- (0,-3); \end{tikzpicture}$, then by definition of $D$ we have

$$ D_{a+1}^{d^a j+s}(C) = \mathrm{id}_{a+1} = C_j(\mathrm{id}_a) = C_j(D_a^s(C)). $$

Phase shifter. Suppose $C$ is a phase shifter $\begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}] \draw[thick] (-.5,0) -- (0,0); \draw[thick] (0,0) -- (.5,0); \draw[thick] (0,0) -- (0,.5); \draw[thick] (0,0) -- (0,-.5); \draw[thick] (0,0) -- (0,1); \draw[thick] (0,0) -- (0,-1); \draw[thick] (0,0) -- (0,2); \draw[thick] (0,0) -- (0,-2); \draw[thick] (0,0) -- (0,3); \draw[thick] (0,0) -- (0,-3); \end{tikzpicture}$ on the mode with global index $d^a j + s$. Since $j$ is even, the Gray code traverses the block with leading digit $j$ in increasing order, so

$$ G_{a+1}^{d}(d^{a}j + s) = j \cdot G_{a}^{d}(s). $$

Decoding at offset $d^a j + s$ therefore yields

$$ D_{a+1}^{d^a j+s}(-\boxed{\theta}) = C_j(C_{G_a^d(s)}(\boxed{\theta})) = C_j(D_a^s(-\boxed{\theta})). $$

As a concrete instance, for $d=3$, $a=1$, $j=0$ and $s=1$ we have $G_2^3(1) = 01$ and the decoded phase shifter is $C_0(C_1(\boxed{\theta}))$, i.e. the phase is applied only on the computational basis vector $|01\rangle$.

Beamsplitter. Let $C = \begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}] \draw[thick] (-.5,0) -- (0,0); \draw[thick] (0,0) -- (.5,0); \draw[thick] (0,0) -- (0,.5); \draw[thick] (0,0) -- (0,-.5); \draw[thick] (0,0) -- (0,1); \draw[thick] (0,0) -- (0,-1); \draw[thick] (0,0) -- (0,2); \draw[thick] (0,0) -- (0,-2); \draw[thick] (0,0) -- (0,3); \draw[thick] (0,0) -- (0,-3); \end{tikzpicture}$ act on two consecutive modes $d^a j + s$ and $d^a j + s + 1$. Since $s+1 < d^a$ and $j$ is even, we have

$$ G_{a+1}^{d}(d^{a}j + s) = j \cdot G_{a}^{d}(s), \quad G_{a+1}^{d}(d^{a}j + s + 1) = j \cdot G_{a}^{d}(s + 1). $$

Write $G_a^d(s) = u'vw$ and $G_a^d(s+1) = u'xw$, so that

$$ G_{a+1}^{d}(d^{a}j + s) = ju'vw, \quad G_{a+1}^{d}(d^{a}j + s + 1) = ju'xw. $$

In words, the two consecutive modes differ only in the suffix digit (the unique position where Gray neighbours differ); the leading digit stays equal to $j$. Decoding $\begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}] \draw[thick] (-.5,0) -- (0,0); \draw[thick] (0,0) -- (.5,0); \draw[thick] (0,0) -- (0,.5); \draw[thick] (0,0) -- (0,-.5); \draw[thick] (0,0) -- (0,1); \draw[thick] (0,0) -- (0,-1); \draw[thick] (0,0) -- (0,2); \draw[thick] (0,0) -- (0,-2); \draw[thick] (0,0) -- (0,3); \draw[thick] (0,0) -- (0,-3); \end{tikzpicture}$ at offset $d^a j + s$ therefore produces exactly the same two-level gate as in the $a$-qudit decoding, but additionally controlled on the leading digit $j$:

$$ D_{a+1}^{d^a j+s} (\begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}] \draw[thick] (-.5,0) -- (0,0); \draw[thick] (0,0) -- (.5,0); \draw[thick] (0,0) -- (0,.5); \draw[thick] (0,0) -- (0,-.5); \draw[thick] (0,0) -- (0,1); \draw[thick] (0,0) -- (0,-1); \draw[thick] (0,0) -- (0,2); \draw[thick] (0,0) -- (0,-2); \draw[thick] (0,0) -- (0,3); \draw[thick] (0,0) -- (0,-3); \end{tikzpicture}) = C_j(D_a^s(\begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}] \draw[thick] (-.5,0) -- (0,0); \draw[thick] (0,0) -- (.5,0); \draw[thick] (0,0) -- (0,.5); \draw[thick] (0,0) -- (0,-.5); \draw[thick] (0,0) -- (0,1); \draw[thick] (0,0) -- (0,-1); \draw[thick] (0,0) -- (0,2); \draw[thick] (0,0) -- (0,-2); \draw[thick] (0,0) -- (0,3); \draw[thick] (0,0) -- (0,-3); \end{tikzpicture})). $$

Swap. The argument for the **LOPP** swap $\begin{tikzpicture}[baseline={([yshift=-.5ex]current bounding box.center)}] \draw[thick] (-.5,0) -- (0,0); \draw[thick] (0,0) -- (.5,0); \draw[thick] (0,0) -- (0,.5); \draw[thick] (0,0) -- (0,-.5); \draw[thick] (0,0) -- (0,1); \draw[thick] (0,0) -- (0,-1); \draw[thick] (0,0) -- (0,2); \draw[thick] (0,0) -- (0,-2); \draw[thick] (0,0) -- (0,3); \draw[thick] (0,0) -- (0,-3); \end{tikzpicture}$ is identical to the beamsplitter case, using the decoding clause of Definition 4.11 for swaps instead of beamsplitters.

Sequential composition. If $C = C_1 \circ C_2$ (so the two subcircuits act on the same mode interval), then

$$ D_{a+1}^{d^a j+s}(C) = D_{a+1}^{d^a j+s}(C_1) \circ D_{a+1}^{d^a j+s}(C_2) $$

by definition. By the induction hypothesis,

$$ D_{a+1}^{d^a j+s}(C_t) = C_j(D_a^s(C_t)) \quad (t = 1, 2), $$

so

$$ D_{a+1}^{d^a j+s}(C) = C_j(D_a^s(C_1)) \circ C_j(D_a^s(C_2)) = C_j(D_a^s(C)), $$

using functoriality of $C_j$.

Parallel composition. If $C = C_1 \otimes C_2$ with $C_1$ on $\ell_1$ modes and $C_2$ on $\ell_2$ modes, then $D$ serialises the tensor by decoding the left block first and the right block afterwards. Concretely,

$$ D_{a+1}^{d^a j+s}(C) = D_{a+1}^{d^a j+s+\ell_1}(C_2) \circ D_{a+1}^{d^a j+s}(C_1). $$
By the induction hypothesis applied to $C_1$ at offset $s$ and to $C_2$ at offset $s + \ell_1$,

$$D_{a+1}^{d^{a}j+s}(C) = C_j(D_a^{s+\ell_1}(C_2)) \circ C_j(D_a^s(C_1)) = C_j(D_a^s(C)),$$

again by functoriality of $C_j$.

**Lemma H.2.** Let $C$ be a circuit of LOPP acting on $\ell$ consecutive modes, and fix $a \ge 0$ and $s$ with $s + \ell \le d^a$. For every odd $j \in \{0, \dots, d-1\}$ we have

$$D_{a+1}^{d^a j+s}(C) = C_j(D_a^{d^a-s-\ell}(\mathrm{Rev}(C))),$$

where $\mathrm{Rev}(C)$ denotes the circuit obtained from $C$ by reversing the order of the $d^a$ modes in the relevant block.

*PROOF.* This is the same induction as in Lemma H.1, but with one extra bookkeeping step reflecting the fact that odd Gray blocks are traversed in reverse order. When $j$ is odd, the block with leading digit $j$ is read backwards by the Gray code:

$$G_{a+1}^{d}(d^{a}j + t) = j \cdot G_{a}^{d}(d^{a} - 1 - t).$$

For example, with $d = 3$ and $a = 1$, the $j = 1$ block corresponds to the three consecutive mode indices 3, 4, 5, but their Gray labels are 12, 11, 10 rather than 10, 11, 12. Thus, a subcircuit $C$ acting on modes starting at offset $s$ in that block corresponds to the same pattern as a forward-traversed circuit, but located at the mirrored starting position $d^a - s - \ell$.

The role of $\mathrm{Rev}(C)$ is precisely to compensate for this reversal at the syntactic level: it renames mode $t$ within the block to mode $(d^a - 1 - t)$. Once $\mathrm{Rev}$ is inserted, the decoding of each generator reduces to the even case with the mirrored offset, and then acquires the outer $C_j$ because the leading Gray digit is $j$ throughout the block.

The inductive steps for sequential and parallel composition are identical to those in Lemma H.1, using the respective induction hypotheses and functoriality of $C_j$.

## H.2 Decoding GrayLifts

The operators $\mathrm{GrayLift}_d^m$ and $j\mathrm{GrayLift}_d^m$ are the optical gadgets used in the encoding to “lift” a local $d^n$-mode circuit through $m$ additional Gray digits. Intuitively, $\mathrm{GrayLift}_d^m(C)$ is a block circuit consisting of $d^m$ copies of $C$ spread across the Gray blocks determined by the extra digits, mirroring the copy whenever the reflected Gray traversal reverses the local order. Decoding should therefore produce $m$ untouched qudits (identities), together with the same decoded action as $C$ on the remaining $n$ qudits. Similarly, $j\mathrm{GrayLift}_d^m(C)$ performs the same lift but only on the branch where a designated digit equals $j$; decoding should therefore add a $j$-control, again padded by $m$ identities for the extra context digits.

We first record a simple arity property: each $\mathrm{GrayLift}$ layer multiplies the number of modes by $d$, corresponding to adding one more Gray digit.

**Lemma H.3.** Let $C$ be a LOPP circuit acting on $d^n$ modes. Then for every $k \ge 0$ the circuit $\mathrm{GrayLift}_d^k(C)$ acts on $d^{n+k}$ modes.

*PROOF.* We proceed by induction on $k$. For $k = 0$ we have $\mathrm{GrayLift}_d^0(C) = C$ by definition, so $\mathrm{GrayLift}_d^0(C)$ acts on $d^n$ modes.

Assume the statement holds for some $k \ge 0$, i.e. that $\mathrm{GrayLift}_d^k(C)$ acts on $d^{n+k}$ modes. By definition,

$$\mathrm{GrayLift}_d^{k+1}(C) = \bigotimes_{q=0}^{d-1} \mathrm{Rev}^q(\mathrm{GrayLift}_d^k(C)).$$

The mode-reversal $\mathrm{Rev}^q(\cdot)$ is implemented by a permutation of modes and therefore does not change the number of modes, so each tensor factor acts on $d^{n+k}$ modes. The tensor product of $d$ such factors therefore acts on $d \cdot d^{n+k} = d^{n+k+1}$ modes, completing the induction. $\square$

**Lemma H.4.** Let $C$ be a LOPP circuit acting on $d^n$ modes, and let $m \ge 0$. Then

$$D_{n+m}^{0}(\mathrm{GrayLift}_{d}^{m}(C)) = \mathrm{id}_{m} \otimes D_{n}^{0}(C)$$

as circuits in $CQC_d$.

*PROOF.* We argue by induction on $m$. It may help to first consider the case $m = 1$: $\mathrm{GrayLift}_d^1(C)$ is a tensor of $d$ blocks, one per leading digit $j$, and decoding each block yields a $j$-controlled copy of $D_n^0(C)$. Composing these $d$ controlled copies and using exhaustivity collapses the whole product to $\mathrm{id}_1 \otimes D_n^0(C)$. The general case iterates this argument one Gray digit at a time.

Base case ($m = 0$). By definition $\mathrm{GrayLift}_d^0(C) = C$, so

$$D_n^0(\mathrm{GrayLift}_d^0(C)) = D_n^0(C) = \mathrm{id}_0 \otimes D_n^0(C),$$

since $\mathrm{id}_0$ is the monoidal unit.

Inductive step. Assume the lemma holds for some $m \ge 0$, i.e.

$$D_{n+m}^{0}(\mathrm{GrayLift}_{d}^{m}(C)) = \mathrm{id}_{m} \otimes D_{n}^{0}(C).$$
Set $F := \text{GrayLift}_d^m(C)$, so by Lemma H.3 $F$ acts on $d^{n+m}$ modes. By definition,

$$ \text{GrayLift}_d^{m+1}(C) = \bigotimes_{j=0}^{d-1} \text{Rev}^j(F), $$

a tensor of $d$ blocks, each occupying a contiguous mode block of size $d^{n+m}$.

Decoding in an $(n+m+1)$-qudit context serialises the tensor product:

$$ D_{n+m+1}^{0}(\text{GrayLift}_{d}^{m+1}(C)) = D_{n+m+1}^{d^{n+m}(d-1)}(\text{Rev}^{d-1}(F)) \circ \dots \circ D_{n+m+1}^{d^{n+m}}(\text{Rev}^{1}(F)) \circ D_{n+m+1}^{0}(\text{Rev}^{0}(F)). $$

For each $j$, the block $\text{Rev}^j(F)$ lives inside the Gray-code block with leading digit $j$. Applying Lemma H.1 when $j$ is even and Lemma H.2 when $j$ is odd (always with $s=0$ and $\ell = d^{n+m}$) yields, in either case,

$$ D_{n+m+1}^{d^{n+m}j}(\text{Rev}^j(F)) = C_j(D_{n+m}^0(F)). $$

Substituting back, we obtain

$$ D_{n+m+1}^{0}(\text{GrayLift}_{d}^{m+1}(C)) = \prod_{j=0}^{d-1} C_j(D_{n+m}^{0}(F)), $$

where the product is sequential composition in some fixed order. By commutativity of distinct controls (Theorem 3.3) the order does not matter, and by exhaustivity (Theorem 3.4) the product collapses to

$$ \prod_{j=0}^{d-1} C_j(D_{n+m}^{0}(F)) = \text{id}_1 \otimes D_{n+m}^{0}(F). $$

Using the induction hypothesis $D_{n+m}^0(F) = \text{id}_m \otimes D_n^0(C)$, we conclude

$$ D_{n+m+1}^{0}(\text{GrayLift}_{d}^{m+1}(C)) = \text{id}_1 \otimes (\text{id}_m \otimes D_{n}^{0}(C)) = \text{id}_{m+1} \otimes D_{n}^{0}(C). $$

**Lemma H.5.** Let $C$ be a LOPP circuit acting on $d^n$ modes, and let $m \ge 0$. Then

$$ D_{n+1+m}^{0}(j\text{GrayLift}_{d}^{m}(C)) = \text{id}_m \otimes C_j(D_{n}^{0}(C)) $$

as circuits in $CQC_d$.

*PROOF.* We proceed by induction on $m$. The base case is the branch-selection behaviour: only the block with leading digit $j$ contains $C$, and decoding turns that into $C_j(D_n^0(C))$. The inductive step then adds one more GrayLift layer, which by exhaustivity contributes exactly one more untouched qudit (an extra identity wire).

Base case ($m=0$). By definition, $j\text{GrayLift}_d^0(C)$ is a tensor of $d$ blocks on $d^n$ modes each, where all blocks are identities except the $j$-th block, which contains $C$ (mirrored if needed to match Gray traversal). Decoding serialises this tensor into a product over $q \in \{0, \dots, d-1\}$. For $q \ne j$, the decoded factor is the identity, while for $q = j$ we get, using Lemma H.1 or Lemma H.2 (depending on the parity of $j$),

$$ D_{n+1}^{d^n j}(\text{Rev}^j(C)) = C_j(D_n^0(C)). $$

Hence

$$ D_{n+1}^{0}(j\text{GrayLift}_{d}^{0}(C)) = C_j(D_{n}^{0}(C)) = \text{id}_0 \otimes C_j(D_{n}^{0}(C)). $$

Inductive step. Assume the lemma holds for some $m \ge 0$, i.e.

$$ D_{n+1+m}^{0}(j\text{GrayLift}_{d}^{m}(C)) = \text{id}_m \otimes C_j(D_n^0(C)). $$

Set $F := j\text{GrayLift}_d^m(C)$. By the recursive definition of $j\text{GrayLift}$, we have

$$ j\text{GrayLift}_d^{m+1}(C) = \bigotimes_{q=0}^{d-1} \text{Rev}^q(F), $$

so decoding in an $(n+1+m+1)$-qudit context gives

$$ D_{n+1+m+1}^{0}(j\text{GrayLift}_{d}^{m+1}(C)) = \prod_{q=0}^{d-1} D_{n+1+m+1}^{d^{n+1+m}q}(\text{Rev}^q(F)). $$

Applying Lemma H.1 or Lemma H.2 to each block (with $s=0$ and $\ell = d^{n+1+m}$) yields

$$ D_{n+1+m+1}^{d^{n+1+m}q}(\text{Rev}^q(F)) = C_q(D_{n+1+m}^0(F)). $$
Applying $D$ and functoriality for sequential composition gives

$$D(E_{\ell}^{k}(-[H^{(r,r+1)}])) = D(\sigma_{k,1,\ell}^{d}) \circ D(\text{GrayLift}_{d}^{k+\ell}(B_{d}^{(i,i+1)})) \circ D(\sigma_{k,\ell,1}^{d}).$$

By Lemma J.11,

$$D(\sigma_{k,1,\ell}^{d}) = \text{id}_k \otimes \sigma_{1,\ell}, \quad D(\sigma_{k,\ell,1}^{d}) = \text{id}_k \otimes \sigma_{\ell,1}.$$

By Lemma H.4, instantiated with $C = B_{d}^{(i,i+1)}$ and $m = k + \ell$,

$$D(\text{GrayLift}_{d}^{k+\ell}(B_{d}^{(i,i+1)})) = \text{id}_{k+\ell} \otimes D_{1}^{0}(B_{d}^{(i,i+1)}).$$

Finally, by the choice of $B_{d}^{(i,i+1)}$ (Lemma G.1) and the decoding correctness for this fixed single-qudit network,

$$D_{1}^{0}(B_{d}^{(i,i+1)}) = -[H^{(r,r+1)}].$$

Combining these equalities and simplifying using PROP coherence yields

$$D(E_{\ell}^{k}(-[H^{(r,r+1)}])) = \text{id}_{k} \otimes -[H^{(r,r+1)}] \otimes \text{id}_{\ell}.$$

Sequential composition. If $f = g \circ h$, then by Definition 4.8,

$$E_{\ell}^{k}(g \circ h) = E_{\ell}^{k}(g) \circ E_{\ell}^{k}(h),$$

so

$$D(E_{\ell}^{k}(g \circ h)) = D(E_{\ell}^{k}(g)) \circ D(E_{\ell}^{k}(h)).$$

The induction hypothesis gives $D(E_{\ell}^{k}(g)) = \text{id}_{k} \otimes g \otimes \text{id}_{\ell}$ and $D(E_{\ell}^{k}(h)) = \text{id}_{k} \otimes h \otimes \text{id}_{\ell}$, hence

$$D(E_{\ell}^{k}(g \circ h)) = \text{id}_{k} \otimes (g \circ h) \otimes \text{id}_{\ell}.$$

Parallel composition. If $f = g \otimes h$ with $g : n_g \to n_g$ and $h : n_h \to n_h$, then Definition 4.8 serialises the tensor product:

$$E_{\ell}^{k}(g \otimes h) = E_{\ell}^{k+n_g}(h) \circ E_{\ell+n_h}^{k}(g).$$

Decoding preserves $\circ$, so

$$D(E_{\ell}^{k}(g \otimes h)) = D(E_{\ell}^{k+n_g}(h)) \circ D(E_{\ell+n_h}^{k}(g)).$$

Applying the induction hypotheses to $h$ at context $(k + n_g, \ell)$ and to $g$ at context $(k, \ell + n_h)$ yields

$$D(E_{\ell}^{k}(g \otimes h)) = \text{id}_{k} \otimes (g \otimes h) \otimes \text{id}_{\ell}.$$

Control. Finally, let $f = C_j(g)$ with $g : m \to m$. By Definition 4.8,

$$E_{\ell}^{k}(C_{j}(g)) = \sigma_{k,m+1,\ell}^{d} \circ j\text{GrayLift}_{d}^{k+\ell}(E_{0}^{0}(g)) \circ \sigma_{k,\ell,m+1}^{d}.$$

Decoding and using Lemma J.11 reduces the outer permutations to the corresponding qudit-wire symmetries. For the middle term we use Lemma H.5 to obtain

$$D(j\text{GrayLift}_{d}^{k+\ell}(E_{0}^{0}(g))) = \text{id}_{k+\ell} \otimes C_{j}(D_{m}^{0}(E_{0}^{0}(g))).$$

By the induction hypothesis applied to $g$ with $k = \ell = 0$, $D_{m}^{0}(E_{0}^{0}(g)) = g$, hence the middle factor is $\text{id}_{k+\ell} \otimes C_{j}(g)$, and the surrounding symmetries cancel by PROP coherence. Therefore

$$D(E_{\ell}^{k}(C_{j}(g))) = \text{id}_{k} \otimes C_{j}(g) \otimes \text{id}_{\ell}.$$

This exhausts the constructors of $CQC_d$, hence $QC_d \vdash D_{k+n+\ell}^{0}(E_{\ell}^{k}(f)) = \text{id}_{k} \otimes f \otimes \text{id}_{\ell}$ for all $f$, as required. $\square$

# I Mimicking rules

This appendix proves Theorem 4.16 from Section 4: every equational step in the LOPP calculus can be mimicked inside our qudit theory via decoding. Concretely, for any $n \ge 0$ and any $d^n$-mode LOPP circuits $C_1, C_2$, if LOPP $\vdash C_1 = C_2$ then their decodings satisfy $QC_d \vdash D(C_1) = D(C_2)$.

The proof has two independent checks:

(1) decoding is compatible with the strict-PROP congruence on raw LOPP terms (i.e. the strict symmetric monoidal/PROP equations);

(2) decoding maps each non-structural axiom of the LOPP calculus (Figure 9) to a derivable equation in $QC_d$.

Since both equational theories are congruences closed under arbitrary contexts, these two checks suffice to mimic arbitrary LOPP derivations.

We work with raw circuits, i.e. string diagrams freely generated from the LOPP (or qudit) generators using $\circ$ and $\otimes$, before quotienting by any equations. We use $\equiv$ for the strict-PROP congruence on raw LOPP circuits as in Definition 4.1. For convenience we reproduce the generating equations in Figure 8.
<figure><img src="image_91.png" /><figcaption>Figure 8: Structural axioms generating the congruence $\equiv$ on raw circuits (either raw quantum circuits or raw optical circuits).</figcaption></figure>

## Commutation of decoded circuits on disjoint blocks

We first record a basic commuting property of decoding when two optical subcircuits act on disjoint mode intervals.

**Lemma I.1.** Let $C_1 : \ell_1 \to \ell_1$ and $C_2 : \ell_2 \to \ell_2$ be raw optical circuits. Let $n \ge 0$ and let $t_1, t_2 \in \mathbb{N}$ satisfy $0 \le t_1, 0 \le t_2, t_1 + \ell_1 \le t_2$, and $t_2 + \ell_2 \le d^n$. Then

$$QC_d \vdash D_n^{\ell_2}(C_2) \circ D_n^{\ell_1}(C_1) = D_n^{\ell_1}(C_1) \circ D_n^{\ell_2}(C_2).$$

*PROOF.* We argue by structural induction on the pair $(C_1, C_2)$.

If either circuit is a sequential composite, the statement follows immediately from the induction hypothesis and the defining clause $D_n^t(C_2 \circ C_1) = D_n^t(C_2) \circ D_n^t(C_1)$.

If either circuit is a tensor composite, we use the serialisation clause $D_n^t(C_1 \otimes C_2) = D_n^{t+\ell_1}(C_2) \circ D_n^t(C_1)$ (Definition 4.11) together with associativity of $\circ$ to reduce to commuting decoded subcircuits whose acted-on mode intervals remain disjoint; the required commutations are then provided by the induction hypothesis.

Thus it suffices to treat the case where both $C_1$ and $C_2$ are LOPP generators (phase shifter, beam splitter, or swap). By Lemma 4.12, each decoded generator acts non-trivially on at most one basis vector (phase shifter) or one two-dimensional Gray-neighbour subspace (beam splitter/swap). Since the mode intervals are disjoint, these supports are disjoint in the Gray-ordered computational basis, and the corresponding decoded operations commute in $QC_d$ using the derived distinct-control commutativity principle together with the local commutation schemata of Figure 2. $\square$

## Contexts and compatibility with structural congruence

To phrase compatibility with $\equiv$ it is convenient to work with contexts.

**Definition I.2.** A (one-hole) raw context $\mathbb{C}[\cdot]_i$ is a term over the LOPP signature built from $\circ$ and $\otimes$ with a distinguished placeholder of arity $i$. If the outer arity of $\mathbb{C}[\cdot]_i$ is $N$, we say that $\mathbb{C}[\cdot]_i$ is an $N$-mode context with hole arity $i$.

**Definition I.3.** Given a $N$-mode context $\mathbb{C}[\cdot]_i$ and an $i$-mode raw circuit $C$, we write $\mathbb{C}[C]$ for the $N$-mode circuit obtained by filling the hole in $\mathbb{C}[\cdot]_i$ with $C$.

**Lemma I.4.** Let $C_1, C_2$ be $d^n$-mode raw optical circuits. If $C_1 \equiv C_2$, then

$$QC_d \vdash D(C_1) = D(C_2).$$
**PROOF.** We prove the following offset-and-context strengthening: for any context $C[\cdot]_i$, any $i$-mode circuits $C_1, C_2$, and any $t, n$ with $t + N \le d^n$ (where $N$ is the outer arity of $C[\cdot]_i$),

$$C_1 \equiv C_2 \implies QC_d \vdash D'_n(C[C_1]) = D'_n(C[C_2]).$$

The desired statement is the special case $C[\cdot]_i = [\cdot]_i$ and $t = 0$.

By induction on the context structure it suffices to check preservation of the generating axioms of Figure 8. Identities and tensor units are sent to $id_n$ by Definition 4.11. Associativity of $\circ$ is preserved because $D'_n$ is defined compositionally on $\circ$. Associativity of $\otimes$ is preserved because $D'_n$ serialises $\otimes$ into a fixed sequential composite, and the two bracketings decode to the same composite up to associativity of $\circ$. For the mixed-product/interchange axiom (29), expanding both sides via the serialisation clause yields composites of decoded subcircuits acting on disjoint mode blocks; Lemma I.1 provides the required commutations. Naturality and involutivity of swap follow from the fact that decoding of permutation circuits agrees with the corresponding qudit-wire symmetries (see Appendix J). $\square$

## Mimicking the LOPP equational theory

Recall the non-structural axioms of LOPP (Figure 9).

<figure><img src="image_92.png" /><figcaption>Figure 9: Non-structural axioms of the LOPP calculus [18]: phase addition, $2\pi$-periodicity, swap decomposition, and Euler/three-beamsplitter identities.</figcaption></figure>

**Theorem I.5.** For any $d^n$-mode raw optical circuits $C_1, C_2$, if LOPP $\vdash C_1 = C_2$, then

$$QC_d \vdash D(C_1) = D(C_2).$$

**PROOF.** The LOPP derivability relation is the congruence generated by the strict-PROP axioms (Figure 8) and the non-structural axioms (A)-(3BS). By Lemma I.4, decoding respects the strict-PROP congruence, so it suffices to verify that each non-structural axiom is preserved by decoding at an arbitrary offset $t$ (closure under contexts is handled exactly as in the proof of Lemma I.4).

Let $t, n$ be such that the relevant local LOPP circuit sits inside $d^n$ modes.

* **Phase addition (A).** Decoding a phase shifter on mode $t$ yields $C_{C_d(t)}(\theta)$ (Definition 4.11). The decoded equation is therefore an instance of the $QC_d$ phase arithmetic axiom (Sum), closed under iterated control.

* **$2\pi$-periodicity (2$\pi$).** Similarly, decoding $-2\pi$ yields a multi-controlled $2\pi$-phase, which is equal to $id_n$ by the $QC_d$ axiom ($2\pi$) (again closed under iterated control). The right-hand side decodes to $id_n$.

* **Swap decomposition (SW).** This is a two-mode local identity. Decoding at offset $t$ yields a (multi-)controlled two-level swap on the unique Gray-neighbour subspace determined by modes $t, t + 1$ (Definition 4.11). The right-hand side decodes to the same controlled two-level swap by a direct diagrammatic calculation in $QC_d$, using the axioms (TP) and (TH) together with the core two-level gate identities of Figure 1.

* **Euler identity (E).** Decoding sends each beam splitter on the consecutive modes $t, t + 1$ to a (multi-)controlled two-level rotation $-R_X^{(v,v+e)}(\theta)$ on the corresponding Gray-neighbour computational subspace. The resulting decoded equation is an instance of the $QC_d$ Euler schema (EH) (closed under control and conjugation by the surrounding wire permutations used in $\Lambda_w^u(-)$).

* **Three-beamsplitter identity (3BS).** Decoding of the three-mode local pattern depends only on which Gray digit changes between $t, t + 1, t + 2$ (Lemma 4.5). If all three consecutive modes lie in a single adjacent-level chain for one digit, the decoded equation is an instance of (3Rx). Otherwise, one of the rotation is additionally controlled by a fixed value of another digit, and the decoded equation is an instance of (3CRx).

Thus decoding preserves each generator of the LOPP equational theory and is stable under contexts; hence LOPP $\vdash C_1 = C_2$ implies $QC_d \vdash D(C_1) = D(C_2)$. $\square$
**PROOF.** By definition,

$$D(C_{d,k,f, [q_1,q_2], [p_1,p_2]}^{\star}) = D\left(\prod_{\beta, \alpha} C_{d, \beta \cdot q_1 \cdot q_2 \cdot \alpha, \beta \cdot p_1 \cdot p_2 \cdot \alpha}\right) \\ = \prod_{\beta, \alpha} D(C_{d, \beta \cdot q_1 \cdot q_2 \cdot \alpha, \beta \cdot p_1 \cdot p_2 \cdot \alpha})$$

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

Each factor

acts on the same pair of target levels and differs only by its outer controls; by commutation

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

and exhaustivity of controls (Thms. 3.3 and 3.4) the product simplifies to a single three-CNOT pattern with no remaining controls, tensored with identities on the untouched wires. This yields the claimed form. □

## J.3 Recursive construction of word-swaps

To describe the optical implementation $C_{d,w_1,w_2}$ more concretely, it is convenient to use a parity based notation on words.

**Definition J.5.** For a word $w = h_1 \cdots h_m \in [d]^m$ define its (binary) parity by

$$\text{Parity}(w) = (h_1 \text{ mod } 2) \oplus \cdots \oplus (h_m \text{ mod } 2) \in \{0, 1\},$$

where $\oplus$ is addition modulo 2.

Given a word $u$ and an integer $n \ge 0$, the *parity tail* $\text{ParityTail}_{u,n} \in [d]^n$ is

$$\text{ParityTail}_{u,n} = \begin{cases} 0^n & \text{if } \text{Parity}(u) = 0, \\ (d-1)^n & \text{if } \text{Parity}(u) = 1. \end{cases}$$

The following inductive clauses specify $C_{d,w_1,w_2}$ for arbitrary $w_1, w_2 \in [d]^m$.

(1) **Base case (adjacent Gray neighbours).** Suppose

$$w_1 = \text{pref} \cdot p \cdot \text{suf}, \quad w_2 = \text{pref} \cdot q \cdot \text{suf},$$

with $|q - p| = 1$ and $\text{suf} = \text{ParityTail}_{\text{pref}\cdot\text{max}(p,q), |\text{suf}|}$. Then $w_1$ and $w_2$ are consecutive in Gray order, and we set

$$C_{d,w_1,w_2} = \text{id}_{G_d^{-1}(\text{pref}\cdot\text{min}(p,q)\cdot\text{suf})} \otimes \underbrace{\otimes}_{\text{id}_{d|w_1|-G_d^{-1}(\text{pref}\cdot\text{max}(p,q)\cdot\text{suf})-1}}$$

(2) **Adjusting the suffix.** Suppose again $w_1 = \text{pref} \cdot p \cdot \text{suf}$ and $w_2 = \text{pref} \cdot q \cdot \text{suf}$ with $|q - p| = 1$, but $\text{suf}$ is not already a parity tail. Write $\text{suf} = \alpha_1 \cdot \alpha_i \cdot \alpha_2$ such that $\alpha_2 = \text{ParityTail}_{\text{pref}\cdot\text{max}(p,q)\cdot\alpha_1, |\alpha_2|}$ and $\alpha_i \neq \text{ParityTail}_{\text{pref}\cdot\text{max}(p,q)\cdot\alpha_1, 1}$. Let

$$\alpha'_{i} = \alpha_{i} + (-1)^{\text{Parity}(\text{pref}\cdot\text{min}(p,q))}$$

and define

$$w'_{1} = \text{pref} \cdot p \cdot \alpha_{1} \cdot \alpha'_{i} \cdot \alpha_{2}, \quad w'_{2} = \text{pref} \cdot q \cdot \alpha_{1} \cdot \alpha'_{i} \cdot \alpha_{2}.$$

Then we set

$$C_{d,w_1,w_2} = C_{d,w_1,w'_1} \circ C_{d,w_2,w'_2} \circ C_{d,w'_1,w'_2} \circ C_{d,w_2,w'_2} \circ C_{d,w_1,w'_1}.$$

(3) **Bridging distant levels.** Suppose $w_1 = \text{pref} \cdot p \cdot \text{suf}$ and $w_2 = \text{pref} \cdot q \cdot \text{suf}$ with $|q - p| > 1$. Let

$$w_{\text{max}} = \text{pref} \cdot \text{max}(p, q) \cdot \text{suf}, \quad w_{\text{max}-1} = \text{pref} \cdot (\text{max}(p, q) - 1) \cdot \text{suf}, \quad w_{\text{min}} = \text{pref} \cdot \text{min}(p, q) \cdot \text{suf}.$$

We then define

$$C_{d,w_1,w_2} = C_{d,w_{\text{max}},w_{\text{max}-1}} \circ C_{d,w_{\text{min}},w_{\text{max}-1}} \circ C_{d,w_{\text{max}},w_{\text{max}-1}}.$$

(4) **Words differing in two positions.** Suppose

$$w_1 = \text{pref} \cdot p_1 \cdot \text{mid} \cdot p_2 \cdot \text{suf}, \quad w_2 = \text{pref}' \cdot q_1 \cdot \text{mid} \cdot q_2 \cdot \text{suf}$$

with $p_1 \neq q_1$ and $p_2 \neq q_2$. Let

$$w'_{2} = \text{pref} \cdot q_{1} \cdot \text{mid} \cdot q_{2} \cdot \text{suf}, \quad w' = \text{pref} \cdot p_{1} \cdot \text{mid} \cdot q_{2} \cdot \text{suf}.$$