发表机构
Tsinghua University; University of Amsterdam; QuSoft; Dalhousie University; University of Copenhagen（清华大学; 阿姆斯特丹大学; QuSoft; 达尔豪斯大学; 哥本哈根大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出所有奇素数维度下多量子比特 Clifford 电路的 16 条完备重写规则，通过辛群同构和电路正规形式证明完备性，并在 Agda 中验证。
AI 中文摘要
我们提出了所有奇素数维度下多量子比特 Clifford 电路的 16 条重写规则的完备集。完备性意味着表示同一线性映射的任意两个 Clifford 电路都可以使用这些规则相互重写。每条规则最多涉及三个量子比特，并且具有直观的解释。为了建立完备性，我们首先在辛群层面工作，利用辛群 Sp(2n, Z_d) 与 Clifford 群关于 Pauli 群的商群之间的同构。我们构造了一个电路正规形式，它捕获 Clifford 算子的 stabiliser tableau，并且在 Pauli 修正下是唯一的。利用这个正规形式，我们推导出一组完备的辛关系，然后通过加入 Pauli 修正将其提升为 Clifford 关系。我们还在 Agda 证明助手中形式化验证了在全局相位下的完备性。
英文摘要
We present a complete set of $16$ rewrite rules for multi-qudit Clifford circuits in all odd prime dimensions. Completeness means that any two Clifford circuits representing the same linear map can be rewritten into each other using these rules. Each rule involves at most three qudits and admits an intuitive interpretation. To establish completeness, we first work at the symplectic level, using the isomorphism between the symplectic group $\mathrm{Sp}(2n,\mathbb{Z}_p)$ and the quotient of the Clifford group by the Pauli group. We construct a circuit normal form that captures the stabiliser tableau of a Clifford operator and is unique up to Pauli correction. Using this normal form, we derive a complete set of symplectic relations, which we then lift to Clifford relations by incorporating Pauli corrections. We also formally verify completeness in the Agda proof assistant.
Comments80 pages, plus a separate supplement. This work is accompanied by a full proof of the relation reduction solved without AI assistance and a machine-checked Agda formalisation, both available in public repositories linked in the paper
