# P3064: Sabidussi's Compatibility Conjecture

- ID: `P3064`
- Reference: `sabidussi-compatibility-conjecture`
- Page: https://theoremdb.org/statements/P3064
- Record maturity: Reviewed problem with recorded work

## Problem

Let \(G\) be a finite connected Eulerian multigraph with minimum degree at least \(4\), with loops and parallel edges allowed, and let \(T\) be an Euler tour of \(G\). Prove that the labelled edges of \(G\) can be partitioned into circuits so that no circuit contains two edges consecutive in the cyclic order of \(T\).

### Context

The Euler tour fixes a cyclic transition at each passage through a vertex. A compatible decomposition asks that each circuit avoid every transition prescribed by that tour.

### Problem setup

- **Definition (Compatible circuit decomposition).** A partition of all labelled edges into circuits in which no circuit uses either edge pair from a transition induced by the Euler tour.
- **Convention.** The cyclic transition from the last tour edge to the first is included. Loops and parallel edges are allowed.

### What counts as a solution

- Produce a partition of all labelled edges into connected 2-regular circuits, using every edge exactly once, such that every cyclic pair of consecutive tour edges belongs to different circuits.
- A formal certificate must cover loops, parallel edges, the closing tour transition, the minimum-degree hypothesis, and the circuit-decomposition conclusion.

## Status

The 2026 preprint reduces the graph problem to a four-colouring theorem for gaps of a cyclic word and derives a compatible circuit decomposition. [1](#reference-1)

**Review status:** Review pending.

**Lean verification:** not Lean-verified.

### Resolution argument

Orient every edge in the direction of the given Euler tour and record the vertex at each passage. The resulting cyclic word contains each vertex degree divided by two times, hence at least twice. The paper's central cyclic-word theorem colours the gaps by the four elements of F_2 squared. Adjacent gaps receive different colours, and at each letter every colour occurs an even number of times among the two gap incidences at its occurrences.

Transfer each gap colour to the corresponding tour edge. Different colours on adjacent gaps mean that the two edges in every tour transition have different colours, including the transition between the final and first edges. The even-incidence condition says that each colour class induces an even subgraph at every vertex. Every finite even multigraph splits into connected 2-regular circuits by taking an Euler tour in each nonempty component and splitting closed trails at repeated vertices. Apply this decomposition separately to the four colour classes. The resulting circuits partition all edges, and no circuit can contain both edges of a prescribed transition because each circuit is monochromatic while every transition has two colours.

The cyclic-word theorem is proved with two parity lemmas over F_2. Passing from gap colours to their nonzero successive differences gives three possible local zero-sum patterns at each letter. A global balancing lemma selects one pattern per letter so that the remaining quadratic parity conditions vanish, after which prefix sums recover the required gap colours. This establishes the stronger four-colouring statement and the stated circuit consequence. Independent external mathematical review of this new proof was not identified in the dated search, so TheoremDB presents it as review pending.

## Work

### Claimed proof and review record

**Proposition 1 (A compatible circuit decomposition is claimed for every eligible Euler tour).** The 2026 preprint reduces the graph problem to a four-colouring theorem for gaps of a cyclic word and derives a compatible circuit decomposition.

Orient every edge in the direction of the given Euler tour and record the vertex at each passage. The resulting cyclic word contains each vertex degree divided by two times, hence at least twice. The paper's central cyclic-word theorem colours the gaps by the four elements of F_2 squared. Adjacent gaps receive different colours, and at each letter every colour occurs an even number of times among the two gap incidences at its occurrences.

Transfer each gap colour to the corresponding tour edge. Different colours on adjacent gaps mean that the two edges in every tour transition have different colours, including the transition between the final and first edges. The even-incidence condition says that each colour class induces an even subgraph at every vertex. Every finite even multigraph splits into connected 2-regular circuits by taking an Euler tour in each nonempty component and splitting closed trails at repeated vertices. Apply this decomposition separately to the four colour classes. The resulting circuits partition all edges, and no circuit can contain both edges of a prescribed transition because each circuit is monochromatic while every transition has two colours.

The cyclic-word theorem is proved with two parity lemmas over F_2. Passing from gap colours to their nonzero successive differences gives three possible local zero-sum patterns at each letter. A global balancing lemma selects one pattern per letter so that the remaining quadratic parity conditions vanish, after which prefix sums recover the required gap colours. This establishes the stronger four-colouring statement and the stated circuit consequence. Independent external mathematical review of this new proof was not identified in the dated search, so TheoremDB presents it as review pending.

### Background and intake notes

- Original intake status: CLAIMED RESOLVED in arXiv:2607.13225v1, posted July 14, 2026. The author supplies a public Lean formalization. Independent external mathematical review was not identified as of 2026-08-01.
- The paper attributes the conjecture to Gert Sabidussi and says Herbert Fleischner recorded it.
- The paper says GPT-5.6 Pro generated the proof and GPT-5.6 Sol helped with the writeup. Nikolay Ulyanov authored the paper and Lean project.
- The public Lean endpoint proves the compatibility consequence for the loop-and-parallel-edge model. The paper's stronger four-colouring statement is outside this entry's target.
- Challenge.lean contains an intentional statement placeholder and is excluded from the production source scan. The production modules report no sorry or admit. TheoremDB has not yet rerun the source in its controlled verifier.

### Formalizations

- **Formalization 1** (reported): A public Lean 4.31.0 development proves the compatibility endpoint and records a clean upstream audit; controlled TheoremDB verification is still pending. [2](#reference-2)

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `sabidussi-compatibility-conjecture`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

1 declaration, with 0 open proof obligations.

### Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary

- State: source contains no sorry; verification pending
- Role: target declaration
- Lean world: `lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+sabidussi-lean@da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa`

```lean
theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary
    {G : LoopMultigraph V E} (T : G.EulerTour)
    (hmin : ∀ v : V, 4 ≤ G.degree v) :
    ∃ S : G.OrdinaryCircuitDecomposition, S.Compatible T
```

### Continue Lean verification

Lean work is attached and awaits signed verification. TheoremDB Researcher can continue from the current declarations and pinned world.

[Continue Lean verification with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20sabidussi-compatibility-conjecture%0A%0AExact%20title%3A%20Sabidussi's%20Compatibility%20Conjecture%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fsabidussi-compatibility-conjecture%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>Nikolay Ulyanov, Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture, arXiv:2607.13225v1 (2026). Abstract; Section 1; Theorem 1.1; Statement of AI use https://arxiv.org/abs/2607.13225v1
   - Also cited at Abstract; Section 1 definitions, Theorem 1.1, attribution, Statement of AI use, and acknowledgements
   - Also cited at Abstract; Section 1; Theorem 1.1; Statement of AI use; acknowledgements
   - Also cited at Abstract and Sections 1-4, especially Theorems 1.1 and 2.1
   - preprint; primary source; v1; checked 2026-08-01
   - Source use: original_summary
   - States a stronger four-colouring theorem, derives the compatibility conjecture, and records that GPT-5.6 Pro generated the proof with GPT-5.6 Sol assisting the writeup.
   - Source used to formulate or check the problem record.
   - States a stronger four-colouring theorem, derives the compatibility conjecture, records that GPT-5.6 Pro generated the proof with GPT-5.6 Sol assisting the writeup, and thanks Tom de Groot for exposition suggestions.
   - Source named by the research packet.
2. <a id="reference-2"></a>Nikolay Ulyanov, sabidussi-lean, commit da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa (2026). Sabidussi/OrdinaryCircuit.lean, theorem loop_sabidussi_compatibility_ordinary; formalization.yaml; VERIFICATION.md https://github.com/gexahedron/sabidussi-lean/tree/da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa
   - Also cited at Sabidussi/OrdinaryCircuit.lean theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary and VERIFICATION.md
   - software; software source; da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa; checked 2026-08-01
   - Source use: citation_only
   - Pinned Lean 4.31.0 formalization of the circuit-decomposition consequence and upstream verification record.
3. <a id="reference-3"></a>Herbert Fleischner, Eulersche Linien und Kreisüberdeckungen, die vorgegebene Durchgänge in den Kanten vermeiden, Journal of Combinatorial Theory, Series B 29(2) (1980), 145-167. Original recording; attribution cross-checked in Ulyanov, Section 1 https://dblp.org/rec/journals/jct/Fleischner80
   - journal_article; reference source
   - Source use: original_summary
   - Records the conjecture attributed to Gert Sabidussi and proves the planar case.