Researchers have developed an equational theory for Detector Error Models (DEMs), which are structured representations of error mechanisms in quantum circuits. These models are fundamental in quantum compilation pipelines, as they enable the capture of fault tolerance at the circuit level. The new framework provides a rigorous way to compare and verify the equivalence of different DEMs, which is crucial for the design and optimization of robust quantum algorithms.

The work introduces a sound, terminating, and confluent rewriting system for DEM terms, formulated as a symmetric monoidal theory over the Giry monad. It has been proven that every DEM term has a unique normal form, which can be computed efficiently in quasilinear time, with a complexity of O(k|E|log|E|), where |E| is the number of instructions and k bounds the size of the target set. This establishes a complete set of invariants, using Tanner graphs, for structural DEM equivalence.

This breakthrough represents the first static decision procedure for DEM equivalence with rigorous correctness guarantees. It is complete for non-adaptive quantum error correction (QEC) pipelines, precisely deciding full decoder-equivalence. Furthermore, the method scales to partially adaptive circuits, such as lattice surgery or distributed QEC, without incurring exponential overhead. The application of this methodology is of great importance for the verification and optimization of quantum compilers, enabling more reliable development of quantum computing.