A Khudorozhkov: Classical reversible circuit equivalence is locally provable

Circuit equivalence asks when two circuits implement the same computation. For classical reversible circuits built from local gates (such as Toffoli gates), this question can be phrased algebraically: can one transform one circuit into another using identities between gates? I will present a locality theorem for classical reversible circuit equivalence. We prove that there exists a universal constant k, independent of the number of wires, such that any equivalence between two reversible circuits can be established by a sequence of functionality-preserving rewrites, where each rewrite changes a subcircuit touching at most k wires. In this sense, any true identity between circuits can be proven using bounded-size local moves. I will also explain how this result gives progress toward a complete equational theory of classical reversible circuits, motivated in part by two complementary problems: circuit compilation, which simplifies circuits for efficient implementation, and circuit obfuscation, which scrambles circuits to obscure their structure without altering functionality.