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

Technical Summary: A Proof of Sabidussi's Compatibility Conjecture

Problem Statement
The paper addresses Sabidussi's compatibility conjecture within the context of finite connected multigraphs. Specifically, it considers an Eulerian multigraph $G$ (where every vertex has even degree) with a minimum degree $\delta(G) \geq 4$. Given a closed trail $T$ that traverses every edge exactly once (an Euler tour), the problem asks whether the edges of $G$ can be partitioned into circuits (connected 2-regular subgraphs) such that no circuit contains two edges that appear consecutively in $T$.

In the language of transition systems, an Euler tour induces a pairing of half-edges at each vertex. A circuit decomposition is "compatible" if no circuit pairs half-edges that are prescribed as a transition by the tour. The conjecture asserts that such a compatible decomposition always exists under the given degree constraints.

Methodology
The proof proceeds through a reduction from the graph-theoretic problem to a combinatorial problem involving cyclic words, followed by an algebraic construction using parity arguments over the field $\mathbb{F}_2$.

1. Reduction to Cyclic Words:
   The authors define a cyclic word $w = (v_0, v_1, \dots, v_{m-1})$ representing the sequence of vertices visited by the Euler tour $T$. The edges of the tour correspond to "gaps" between these letters. The problem is reformulated as finding a coloring of these gaps with elements from $\mathbb{F}_2^2$ (a 4-coloring) such that:

   • Adjacent gaps (corresponding to consecutive edges in the tour) receive different colors.
   • For every vertex $v$ in the graph, the colors assigned to the gaps incident to occurrences of $v$ satisfy a parity condition: each color appears an even number of times among the gap incidences.

2. Algebraic Framework:
   The core of the proof relies on two lemmas established in Section 3:

   • Lemma 3.1 (Four-colour parity): A family of elements in $\mathbb{F}_2^2$ contains each element an even number of times if and only if their linear sum is zero and their quadratic sum (defined via a specific bilinear form $q(x) = x_1x_2$) is zero.
   • Lemma 3.2 (Three-state balancing): A global selection principle stating that for a finite set $U$ and a three-element set $\Sigma$, if certain symmetry and zero-sum conditions are met by a function $\beta$, the number of assignments satisfying a system of local constraints is odd (and thus non-zero).

3. Construction of the Coloring:
   The proof constructs the required gap coloring by:

   • Defining "local patterns" $\Delta_{a,t}$ for each letter $a$ in the cyclic word, which assign non-zero values in $\mathbb{F}_2^2$ to the occurrences of $a$ such that their sum is zero.
   • Defining interaction terms $\beta_{ab}$ between distinct letters based on the order of their occurrences in the word.
   • Applying Lemma 3.2 to select a specific state $t_a \in \Omega$ (where $\Omega = \mathbb{F}_2^2 \setminus \{0\}$) for each letter $a$. This selection ensures that the interaction constraints vanish.
   • Using these selections to define a sequence $y_i$ (differences between gap colors) and integrating them to recover the gap colors $x_i$.
   • Verifying that the resulting coloring satisfies the even-degree condition for each color class at every vertex by showing that the sum of colors and the sum of their quadratic forms vanish, invoking Lemma 3.1.

Key Contributions and Results

• Theorem 1.1: The paper proves that for any finite Eulerian multigraph with minimum degree at least 4 and any Euler tour $T$, there exists a coloring $\chi: E(G) \to \mathbb{F}_2^2$ such that consecutive edges in $T$ have different colors, and every vertex has even degree in each color class.
• Corollary 1.2: As a consequence, the graph $G$ admits a circuit decomposition compatible with the transition system induced by $T$.
• Improvement on Cycle Double Covers: The paper notes that in the presence of a dominating circuit, the result implies that a cubic graph $H$ has a 5-cycle double cover containing that circuit. This improves upon the recently proved 8-cycle double cover theorem (attributed to OpenAI in the text) for graphs with a dominating circuit.
• Formalization: The proof has been fully formalized in the Lean theorem prover.

Significance and Claims
The paper claims to provide a complete proof of Sabidussi's compatibility conjecture, a problem that had been studied since the work of Kotzig (1968) and Fleischner (1980). While previous results had established the conjecture for planar graphs, $K_5$-minor-free graphs, or specific degree constraints, this proof treats every even degree directly without restricting the graph class beyond the minimum degree requirement.

The authors explicitly state that the proof is a strengthening of the original conjecture, providing a 4-coloring with specific structural properties rather than just a decomposition. The work is presented as a definitive resolution to the conjecture, relying on a novel combination of cyclic word combinatorics and parity lemmas over finite fields.

Note on Authorship
The paper explicitly states that the proof is entirely due to "GPT 5.6 Pro," and the write-up was prepared with assistance from "GPT 5.6 Sol." The human author, Nikolay Ulyanov, acknowledges the role of AI in the generation of the mathematical argument and the exposition.