Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture

Abstract

We prove Sabidussi's compatibility conjecture. Let $G$ be a finite connected multigraph in which every vertex has even degree and the minimum degree is at least four, and let $T$ be a closed trail that traverses every edge exactly once. The edges of $G$ can be partitioned into circuits (connected 2-regular subgraphs) so that no circuit contains the two edges used consecutively anywhere in $T$. In fact, the edges can be four-coloured so that every such pair receives two different colours and the subgraph formed by the edges of each colour has even degree at every vertex. Formalization in Lean 4 is also available in the author's github.

Disclosure

“ed in section 3. The proof has also been formalized in Lean. The formalization is available in the author’s GitHub repository: https://github.com/gexahedron/sabidussi-lean. Statement of AI use. The proof in this paper is entirely due to GPT 5.6 Pro, and the writeup was prepared with help from GPT 5.6 Sol. Acknowledgements. The author thanks Tom de Groot for valuable suggestions on the exposition of the proof. 2 Reduction to a cyclic word Fix G and T as in theorem 1.1. Temporar”

PDF page 2

Classification

Substantial proof generation

Multiplier

10

Verified

2026-08-23T18:53:13.757403Z

Structural counts