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

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.