图谜题III.1：萨比杜西相容性猜想的证明
Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture
浏览论文内容
中文总结 AI 辅助
对有限连通多重图\(G\)，在其顶点度数为偶数且最小度数至少为\(4\)时，证明其边可按特定规则划分为回路，并能四着色，每条边的颜色对及对应子图满足一定条件，同时给出Lean 4形式化证明。
中文摘要 AI 辅助
我们证明了萨比杜西相容性猜想。设\(G\)为有限连通多重图，其每个顶点度数为偶数且最小度数至少为\(4\)，\(T\)为恰好遍历每条边一次的闭迹。\(G\)的边可划分为回路（连通的\(2 -\)正则子图），使得没有回路在\(T\)中任何位置包含连续使用的两条边。实际上，边可四着色，使得每对这样的边接收两种不同颜色，且每种颜色的边构成的子图在每个顶点度数为偶数。作者的GitHub上也有Lean 4形式化证明。
英文摘要
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.
