Skip to content
Preprint

An Exactness Barrier for ZX-Calculus Optimization of Synthesized Clifford+T Circuits

Aug 2026 · 0 citations · 51 references
Physics

TL;DR

It is proved that the local ZX simplification layer (spider fusion and identity removal) computes exactly the free-product normal form of Z_2 * Z_8, giving exact per-instance compression and, under a calibrated ergodicity hypothesis, a depth-independent limit law confirmed on two independently constructed nets.

Abstract

Gate synthesis and circuit optimization are usually studied separately, and evidence on their interaction is contradictory: ZX-calculus rewriting removes a stable fraction of Solovay-Kitaev circuits, yet almost nothing from number-theoretically synthesized circuits. We show both behaviours follow from a single bound. For any optimizer that preserves the implemented element exactly--including all sound ZX rewriting with extraction--the achievable T-count is bounded below by the denominator exponent of the synthesized ring element. This exactness barrier is computable per instance and separates exact post-processing from approximation-aware resynthesis by a certified factor reaching 101x at recursion depth five. The two behaviours are then the barrier operating at different distances from the floor. For Solovay-Kitaev circuits we prove that the local ZX simplification layer (spider fusion and identity removal) computes exactly the free-product normal form of Z_2 * Z_8, giving exact per-instance compression and, under a calibrated ergodicity hypothesis, a depth-independent limit law confirmed on two independently constructed nets. For number-theoretically synthesized circuits the floor is already saturated: on single-qubit words automated ZX simplification attains it exactly, via a closed-form formula for minimal T-count in terms of phase linkage through the Z-axis normalizer. At two qubits and beyond the same valuation yields unconditional rigidity certificates, which on the quantum-Shannon-decomposition plus gridsynth pipeline certify 99.4-99.9% of the synthesized T-count as incompressible, with rigidity strengthening as accuracy tightens. This explains, and predicts the size of, the near-null optimization recently reported for that pipeline.

View source

Similar papers

Preprint Aug 2026

Numerical Evaluation of ZX Calculus Optimization for Solovay Kitaev Quantum Circuit Synthesis

A measurement of what diagrammatic post-processing recovers from structural redundancy in the Solovay-Kitaev algorithm, which optimizes for numerical convergence rather than circuit economy, and its output carries structural redundancy that a gate-level compiler cannot see.

Dulari De Silva, A. Mahasinghe, Chon-Fai Kam et al. · 0 citations
Preprint Sep 2026

Link-middle-cut lower bounds for Clifford circuit synthesis

This work extends the link--middle--cut (LMC) framework for linear reversible circuits to Clifford operators represented by binary symplectic tableaux and derives efficiently computable bounds for synthesis up to a permutation of the output qubits, corresponding to free qubit relabeling.

Søren Fuglede Jørgensen · 0 citations
Preprint Aug 2026

CircLS: Compiling Lattice Surgery to Physical Circuits with Dynamic Allocation

CircLS is a full-stack lattice surgery compiler that allocates data patches dynamically: each patch is allocated at its first use and freed at its last use, and the freed tiles can be reused as ancilla paths.

John Zhang · 1 citation
Preprint Aug 2026

AlchemQ: Proof-Carrying Quantum Circuit Optimization with Per-Result Equivalence Certificates

We present AlchemQ v0.5, a proof-of-concept system that couples an untrusted beam-search optimizer with a machine-checkable per-result certification layer and a versioned certificate protocol (0.2.0), so that every optimized circuit ships with a verifiable artifact rather than a bare claim. The certifier proves equival...

Adam Laabs · 0 citations
Preprint Aug 2026

RENESIS: Energy-Aware Synthesis of Adiabatic Logic from Irreversible Netlists

We describe Renesis, an automated synthesis tool that accepts an ordinary irreversible netlist and produces a verified, technology-mapped energy-recovery (adiabatic) circuit, using energy rather than area or delay as the optimization criterion. Renesis models the netlist with a vector-space formulation that expresses s...

Mitchell A. Thornton · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.