Completeness for Fault Equivalence of Clifford ZX Diagrams

Aleks Kissinger; Benjamin Rodatz; Maximilian R\"usch

arxiv: 2510.08477 · v3 · pith:RITJTBCHnew · submitted 2025-10-09 · 🪐 quant-ph

Completeness for Fault Equivalence of Clifford ZX Diagrams

Maximilian R\"usch , Aleks Kissinger , Benjamin Rodatz This is my paper

Pith reviewed 2026-05-21 21:13 UTC · model grok-4.3

classification 🪐 quant-ph

keywords ZX calculusfault equivalenceClifford circuitsquantum error correctiondiagram rewritingfault gadgetsnormal formPauli noise

0 comments

The pith

A sound and complete set of ZX rewrite rules exists for fault equivalence of Clifford diagrams.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that a specific collection of ZX rewrites is both sound and complete when diagrams represent Clifford circuits and faults are arbitrary Pauli errors. Two circuits count as fault equivalent when the noise effects on one are never worse than on the other, so rewrites that preserve this relation keep any fault-tolerant guarantees intact. Fault gadgets are the key device: they split each diagram into an ideal fault-free part and a separate part that lists every possible fault outcome. With these gadgets the authors derive a unique normal form under noise and prove that the rules can rewrite any Clifford ZX diagram into that form.

Core claim

The authors prove that a chosen set of ZX rewrites is sound and complete for fault equivalence of Clifford ZX diagrams. Fault gadgets separate each diagram into a fault-free component that captures the ideal linear map and a noisy component that enumerates all possible Pauli fault effects, including correlations. This separation yields a unique normal form for diagrams under noise, and every diagram can be reduced to this normal form by repeated application of the proposed rules.

What carries the argument

Fault gadgets, diagrammatic constructions that isolate the fault-free behavior from the complete enumeration of Pauli fault effects.

If this is right

Any two fault-equivalent Clifford diagrams can be transformed into each other using only the listed rules.
Circuit optimizations can be performed while provably preserving the original fault-tolerance properties.
A framework for fault-tolerant synthesis and optimisation becomes correct by construction.
The normal form supplies a canonical representative for checking fault equivalence.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same gadget technique might be adapted to test approximate equivalence under small non-Pauli noise.
Automated rewriting tools could use the normal form to verify equivalence of larger stabilizer circuits.
The rules may interact usefully with existing ZX simplifications for measurement-based computation.

Load-bearing premise

The completeness result holds only when the diagrams are Clifford and the faults are arbitrary but Pauli.

What would settle it

Two Clifford ZX diagrams that are fault equivalent yet cannot be rewritten into the same normal form by the given rules, or two diagrams that the rules equate but whose fault behaviors differ.

read the original abstract

Two circuits are considered to be equivalent under noise if the effect of faults on one circuit is no worse than the effect of faults on the other circuit. We call this relationship fault equivalence. Fault equivalence offers a way to transform circuits while provably preserving their fault-tolerant properties, enabling a framework for fault-tolerant circuit synthesis and optimisation that is correct by construction. The ZX calculus offers a diagrammatic way to represent and reason about quantum circuits and is a useful tool for manipulating circuits while preserving fault equivalence. For this, the usual set of ZX rewrites has to be restricted to not only preserve the underlying linear map represented by the diagram, but also fault equivalence. In this work, we provide a set of ZX rewrites that are sound and complete for fault equivalence of Clifford ZX diagrams. This means that any equivalence that can be derived using the proposed rules is certain to be correct, and any correct equivalence can be derived using only these rules. For this, we utilise diagrammatic constructions called fault gadgets to reason about arbitrary, possibly correlated Pauli faults in ZX diagrams. Fault gadgets allow us to separate the diagram into a fault-free part, which captures the noise-free behaviour of a diagram, and a noisy part that enumerates the effects of all possible faults. Using this, we provide a unique normal form for ZX diagrams under noise and show that any diagram can be brought into this normal form using our proposed rule set.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper gives a soundness and completeness result for a restricted ZX rule set that preserves fault equivalence under Pauli faults for Clifford diagrams.

read the letter

This paper establishes that a restricted set of ZX rewrites is sound and complete for fault equivalence of Clifford ZX diagrams. The authors use fault gadgets to separate the ideal linear map from the effects of all possible Pauli faults, including correlated ones, and then show a unique normal form reachable by the rules. The novelty lies in tailoring the ZX rules to preserve not only the standard semantics but also this fault equivalence relation. Prior completeness results for ZX handle the noise-free case, but here the rewrites must keep the fault behavior intact. The fault gadgets provide a diagrammatic way to enumerate the Pauli error effects without losing the graphical structure. The paper does well by giving a clear motivation for fault equivalence in the context of fault-tolerant circuit synthesis. Being able to rewrite diagrams while guaranteeing that the error properties remain the same is a practical step forward. The argument follows the usual strategy for ZX completeness proofs but adapts it to the new semantics, and the stress-test indicates no obvious internal contradictions. A soft spot is the limited applicability. Everything is restricted to Clifford gates and Pauli faults; circuits with non-Clifford elements or different noise models are outside the scope. The proofs are not machine-checked, so while the approach looks consistent, there could be subtle gaps in showing that the normal form is always unique and that all equivalences are captured. The abstract claims completeness, but full details would clarify if the gadget construction handles all correlations properly. This work is for researchers in quantum computing who focus on diagrammatic methods and fault tolerance. Someone building or optimizing error-corrected circuits could use these rules to perform transformations with provable guarantees. I would recommend sending this to peer review. It presents a new completeness theorem that seems well-grounded in the ZX framework and addresses a real need in the field.

Referee Report

2 major / 3 minor

Summary. The manuscript claims to introduce a finite set of ZX-calculus rewrite rules that are sound and complete for fault equivalence on Clifford ZX diagrams. Fault equivalence is defined so that one diagram is no worse than another under arbitrary (possibly correlated) Pauli faults. The authors define fault gadgets that separate the fault-free linear map from an explicit enumeration of all Pauli fault effects, establish a unique normal form reachable by the rules, and argue that any Clifford ZX diagram can be rewritten to this normal form while preserving fault equivalence.

Significance. If the soundness and completeness claims hold, the result would provide a diagrammatic calculus for provably correct-by-construction transformations of fault-tolerant Clifford circuits, enabling synthesis and optimisation that preserve fault-tolerance properties. The fault-gadget construction for enumerating Pauli effects (including correlations) is a concrete technical contribution that extends standard ZX completeness techniques to a noise-aware setting. The restriction to Clifford gates and Pauli noise is clearly stated, so the result is scoped appropriately.

major comments (2)

[§4] §4, Theorem 4.1 (normal-form uniqueness): the argument that every diagram reduces to the claimed normal form under the proposed rules relies on an inductive enumeration of fault gadgets; the induction step for diagrams containing multiple overlapping spiders is only sketched and does not explicitly address the case of correlated faults across non-adjacent wires.
[§3.2] §3.2, Definition 3.4 (fault gadget semantics): the mapping from a fault gadget to the set of all possible Pauli error operators is stated to be exhaustive, but the proof that the gadget construction captures arbitrary correlations (rather than only independent or pairwise faults) is not given in full detail; a small counter-example diagram with three-qubit correlated noise would clarify the claim.

minor comments (3)

[Figure 2] Figure 2: the labels on the fault-gadget wires are difficult to read at the printed size; adding a small legend or increasing font size would improve clarity.
Notation: the symbol for the fault-free part of a diagram is introduced as F(D) in §3 but later appears as F_D without redefinition; consistent notation throughout would help readers.
[§3] The paper would benefit from an explicit statement of the precise ZX rule set (perhaps as a table in §3) so that readers can verify the rules are finite and local.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their positive evaluation and detailed comments on the manuscript. We address each major comment below and indicate the revisions we plan to make.

read point-by-point responses

Referee: [§4] §4, Theorem 4.1 (normal-form uniqueness): the argument that every diagram reduces to the claimed normal form under the proposed rules relies on an inductive enumeration of fault gadgets; the induction step for diagrams containing multiple overlapping spiders is only sketched and does not explicitly address the case of correlated faults across non-adjacent wires.

Authors: We agree that the induction step in the proof of Theorem 4.1 is presented in a somewhat abbreviated form. In the revised manuscript we will expand this step with an explicit case analysis for diagrams containing multiple overlapping spiders. The argument will be extended to show that the enumeration of fault gadgets continues to account for all possible Pauli correlations, including those acting across non-adjacent wires, by considering the composition of the relevant fault operators at each inductive step. revision: yes
Referee: [§3.2] §3.2, Definition 3.4 (fault gadget semantics): the mapping from a fault gadget to the set of all possible Pauli error operators is stated to be exhaustive, but the proof that the gadget construction captures arbitrary correlations (rather than only independent or pairwise faults) is not given in full detail; a small counter-example diagram with three-qubit correlated noise would clarify the claim.

Authors: The fault-gadget construction enumerates every possible combination of Pauli operators on the wires it acts upon, which by definition includes arbitrary multi-qubit correlations. We accept that a fully expanded proof of exhaustiveness would improve clarity. We will therefore insert a short three-qubit example diagram subject to a fully correlated Pauli error (e.g., a single X⊗X⊗X fault together with all other combinations) and explicitly verify that every term appears in the gadget expansion. revision: yes

Circularity Check

0 steps flagged

No significant circularity; completeness proof is self-contained

full rationale

The paper establishes soundness and completeness of a finite set of ZX rewrites for fault equivalence on Clifford diagrams by constructing fault gadgets that explicitly separate the fault-free linear map from an enumeration of all Pauli fault effects (including correlations). It then exhibits a unique normal form reachable via the rules. This follows the standard diagrammatic strategy for ZX completeness proofs and is internally consistent within the stated restrictions to Clifford gates and Pauli noise. No step reduces by construction to a fitted parameter, self-referential definition, or load-bearing self-citation chain; the equivalence relation and normal form are defined independently of the rewrite rules, and the proof does not rely on prior results by the same authors in a way that creates circularity. The derivation is therefore self-contained against external mathematical benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The work rests on the standard completeness of ZX for Clifford circuits and introduces fault gadgets as the key new construction; no numerical parameters are fitted.

axioms (1)

standard math ZX calculus is complete for the linear maps of Clifford circuits
Invoked to justify that the restricted rules still capture the underlying quantum operation when faults are ignored.

invented entities (1)

fault gadget no independent evidence
purpose: To isolate the fault-free map and enumerate all possible Pauli fault effects within a single diagram
New diagrammatic device introduced to reason about correlated faults while preserving the rewrite system.

pith-pipeline@v0.9.0 · 5784 in / 1241 out tokens · 57180 ms · 2026-05-21T21:13:06.344274+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We provide a set of ZX rewrites that are sound and complete for fault equivalence of Clifford ZX diagrams... fault gadgets... unique normal form
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

Proposition 5.9. Every diagram DN ... has a fault normal form... using only the rules from Fig. 3.

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

A framework for low-overhead quantum fault tolerance via spacetime lifting
quant-ph 2026-06 unverdicted novelty 7.0

Spacetime lifting constructs fault complexes with almost-linear fault distance in spacetime cost, outperforming prior constructions and supporting fault-tolerant logical teleportation via cluster-state protocols.