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

Nikolay Ulyanov

math.CO Jul 14, 2026 · v1

Read PDF arXiv abstract Code

TL;DR

A proof of Sabidussi's compatibility conjecture is accompanied by a Lean 4 formalization available on the author's GitHub.

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.

Problem

Sabidussi's compatibility conjecture asks whether an Eulerian multigraph with minimum degree at least four admits a circuit decomposition compatible with the transition system induced by a given Euler tour.

Approach

The graph statement is reduced to a combinatorial 'cyclic-word colouring' theorem asking to colour gaps of a cyclic word with elements of F_2^2 subject to adjacency and parity constraints. Two parity lemmas over F_2 (a four-colour parity criterion and a three-state balancing principle) are proved. Local patterns and pairwise interactions are combined to produce the required colouring, yielding a four-colouring of edges. A Lean 4 formalization of the argument is provided.

Results

Sabidussi's compatibility conjecture is proved, in the stronger form of an edge four-colouring with the stated parity properties, implying the existence of a compatible circuit decomposition; a corollary gives a 5-cycle double cover of cubic graphs with a prescribed dominating circuit.

Papers With

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