Papers With

← All papers
First page of Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture

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

Nikolay Ulyanov

math.CO Jul 14, 2026 · v2
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
The proof of Sabidussi's compatibility conjecture is formalized in Lean 4, with the 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 an Euler tour of $G$. The edges of $G$ can be partitioned into circuits (connected $2$-regular subgraphs) so that no circuit contains two edges used consecutively anywhere in $T$. In fact, the edges can be four-coloured so that every such pair receives different colours and every colour class has even degree at every vertex. We use a counting argument based on the Chevalley-Warning theorem to show that a four-colouring with the required properties exists. Splitting each colour class into circuits then gives the desired compatible decomposition. Formalization in Lean 4 is also available in the author's github.
Problem

Sabidussi's compatibility conjecture asks the following. Take an Eulerian multigraph with minimum degree at least four and fix an Euler tour. Can the edges be partitioned into circuits so that no circuit contains two edges used consecutively in the tour?

Approach

The graph problem is reduced to colouring the gaps of a cyclic word with elements of F_2^2. The colouring must give consecutive gaps different colours, and each colour must occur an even number of times at every letter. Two parity lemmas are used: a four-colour parity criterion via a quadratic form, and a three-state balancing lemma proved by a Chevalley–Warning-style counting argument. These lemmas yield the required colouring. The result is also formalized in Lean 4.

Results

Every such graph has an edge four-colouring in which consecutive tour edges get different colours and every colour class is even. Splitting each colour class into circuits proves the conjecture. As a corollary, a cubic graph with a dominating circuit C has a 5-cycle double cover containing C.