# Techniques: With a Few Square Roots, Quantum Computing is as Easy as Pi

## What the paper contributes (one paragraph)
The paper (arXiv:2310.14056) gives a categorical, axiomatic account of unitary quantum computing. It extends rig groupoids, the semantic model of the classical reversible language Pi, with just two maps (an 8th root of the identity scalar and a square root of boolean negation) and three equations, and proves the result is computationally universal. The construction is realised as a combinator language, Sqrt-Pi, with an equational theory that is sound and complete for arbitrary Clifford circuits, Clifford+T circuits of at most two qubits, and arbitrary Gaussian Clifford+T circuits. This yields, to the authors' knowledge, the first sound and complete equational theory for a computationally universal unitary quantum programming language: circuit equivalences become purely equational rewrites over rig-category coherences rather than complex linear-algebra computations. Many results are mechanised in an extension of the agda-categories library supplied as supplementary material.

## Techniques offered
- **Sound and complete equational theory for unitary quantum circuits** - an equational rewriting system over an extended rig groupoid that decides circuit equivalence by syntactic rewriting, supplying an axiomatic equivalence-checking calculus for Clifford, two-qubit Clifford+T, and Gaussian Clifford+T circuits.
  - guarantee: static proof; soundness and completeness of the equational theory with respect to the Clifford, two-qubit Clifford+T, and Gaussian Clifford+T gate sets.
  - quote: "The semantic construction is turned into an extension of \PiLang, called \SPiLang, that is a computationally universal quantum programming language equipped with an equational theory that is sound and complete with respect to the Clifford gate set, the standard gate set of Clifford+T restricted to $\le 2$ qubits, and the computationally universal Gaussian Clifford+T gate set."
- **Machine-checked formal verification (Agda formalisation)** - a mechanised proof library extending agda-categories that formalises the model and derived circuit equivalences (for example the Sleator-Weinfurter decomposition of the Toffoli gate), supplying machine-checkable correctness proofs for quantum circuit identities.
  - guarantee: static proof; results are formalised and type-checked in Agda, so the supplied circuit-equivalence proofs are machine-verified.
  - quote: "As a supplement to this paper, we have developed an Agda library and used it to formalise some of our results."

## Where it could apply
- Target primitive(s): none directly; applies to circuit equivalence and compilation/rewriting of fixed unitary circuits rather than to a running algorithm such as VQE, QAOA, or QPE.
- Target application group(s): platforms_tooling; error_correction (Clifford and Clifford+T circuit reasoning underpinning stabiliser and fault-tolerant constructions).
- Code family / hardware assumptions: none; the formalism is hardware-agnostic and gate-set-agnostic, instantiated here for qubit Clifford, Clifford+T, and Gaussian Clifford+T gate sets (with qudit gate sets proposed as future work).

## Caveats
This is a theoretical programming-languages and quantum-foundations paper; its primary output is a calculus and equational theory, not a runnable accreditation, decoding, mitigation, or estimation routine. What is suppliable to an external result is the equivalence-checking calculus and its mechanised Agda proofs, useful for verifying compiler rewrites and circuit identities. Completeness is restricted to the named gate sets (full Clifford, Clifford+T limited to at most two qubits, and arbitrary Gaussian Clifford+T); it does not cover arbitrary multi-qubit Clifford+T, and it deliberately excludes state preparation and measurement. The exponential-speedup discussion is informal and flagged as future work.