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

Resumo Técnico: Uma Prova da Conjectura de Compatibilidade de Sabidussi

Enunciado do Problema
O artigo aborda a conjectura de compatibilidade de Sabidussi no contexto de multigrafos conexos finitos. Especificamente, considera um multigrafo Euleriano $G$ (onde cada vértice possui grau par) com um grau mínimo $\delta(G) \geq 4$. Dada uma trilha fechada $T$ que atravessa cada aresta exatamente uma vez (um tour de Euler), o problema questiona se as arestas de $G$ podem ser particionadas em circuitos (subgrafos 2-regulares conexos) de tal forma que nenhum circuito contenha duas arestas que apareçam consecutivamente em $T$.

Na linguagem dos sistemas de transição, um tour de Euler induz um emparelhamento de meias-arestas em cada vértice. Uma decomposição de circuitos é "compatível" se nenhum circuito emparelha meias-arestas que foram prescritas como uma transição pelo tour. A conjectura afirma que tal decomposição compatível sempre existe sob as restrições de grau dadas.

Metodologia
A prova procede através de uma redução do problema teórico de grafos para um problema combinatório envolvendo palavras cíclicas, seguida por uma construção algébrica usando argumentos de paridade sobre o corpo $\mathbb{F}_2$.

1. Redução para Palavras Cíclicas:
   Os autores definem uma palavra cíclica $w = (v_0, v_1, \dots, v_{m-1})$ representando a sequência de vértices visitados pelo tour de Euler $T$. As arestas do tour correspondem a "lacunas" entre essas letras. O problema é reformulado como encontrar uma coloração dessas lacunas com elementos de $\mathbb{F}_2^2$ (uma 4-coloração) de modo que:

• Lacunas adjacentes (correspondentes a arestas consecutivas no tour) recebam cores diferentes.
• Para cada vértice $v$ no grafo, as cores atribuídas às lacunas incidentes às ocorrências de $v$ satisfaçam uma condição de paridade: cada cor aparece um número par de vezes entre as incidências das lacunas.

2. Estrutura Algébrica:
   O cerne da prova baseia-se em dois lemas estabelecidos na Seção 3:

• Lema 3.1 (Paridade de quatro cores): Uma família de elementos em $\mathbb{F}_2^2$ contém cada elemento um número par de vezes se, e somente se, sua soma linear é zero e sua soma quadrática (definida via uma forma bilinear específica $q(x) = x_1x_2$) é zero.
• Lema 3.2 (Balanceamento de três estados): Um princípio de seleção global declarando que, para um conjunto finito $U$ e um conjunto de três elementos $\Sigma$, se certas condições de simetria e soma zero forem atendidas por uma função $\beta$, o número de atribuições que satisfazem um sistema de restrições locais é ímpar (e, portanto, não nulo).

3. Construção da Coloração:
   A prova constrói a coloração de lacunas necessária através de:

• Definição de "padrões locais" $\Delta_{a,t}$ para cada letra $a$ na palavra cíclica, que atribuem valores não nulos em $\mathbb{F}_2^2$ às ocorrências de $a$ de modo que sua soma seja zero.
• Definição de termos de interação $\beta_{ab}$ entre letras distintas baseados na ordem de suas ocorrências na palavra.
• Aplicação do Lema 3.2 para selecionar um estado específico $t_a \in \Omega$ (onde $\Omega = \mathbb{F}_2^2 \setminus \{0\}$) para cada letra $a$. Esta seleção garante que as restrições de interação desapareçam.
• Uso dessas seleções para definir uma sequência $y_i$ (diferenças entre as cores das lacunas) e integração delas para recuperar as cores das lacunas $x_i$.
• Verificação de que a coloração resultante satisfaz a condição de grau par para cada classe de cor em cada vértice, mostrando que a soma das cores e a soma de suas formas quadráticas são nulas, invocando o Lema 3.1.

Contribuições e Resultados Principais

• Teorema 1.1: O artigo prova que, para qualquer multigrafo Euleriano finito com grau mínimo de pelo menos 4 e qualquer tour de Euler $T$, existe uma coloração $\chi: E(G) \to \mathbb{F}_2^2$ tal que arestas consecutivas em $T$ possuem cores diferentes, e cada vértice possui grau par em cada classe de cor.
• Corolário 1.2: Como consequência, o grafo $G$ admite uma decomposição de circuitos compatível com o sistema de transição induzido por $T$.
• Melhoria no Double Cover de Ciclos: O artigo observa que, na presença de um circuito dominante, o resultado implica que um grafo cúbico $H$ possui um 5-ciclo double cover contendo esse circuito. Isso melhora o teorema de 8-ciclo double cover recentemente provado (atribuído à OpenAI no texto) para grafos com um circuito dominante.
• Formalização: A prova foi totalmente formalizada no provador de teoremas Lean.

Significância e Alegações
O artigo afirma fornecer uma prova completa da conjectura de compatibilidade de Sabidussi, um problema que vem sendo estudado desde o trabalho de Kotzig (1968) e Fleischner (1980). Embora resultados anteriores tivessem estabelecido a conjectura para grafos planares, grafos sem minoração de $K_5$, ou restrições de grau específicas, esta prova trata cada grau par diretamente sem restringir a classe do grafo além do requisito de grau mínimo.

Os autores afirmam explicitamente que a prova é um fortalecimento da conjecta original, fornecendo uma 4-coloração com propriedades estruturais específicas em vez de apenas uma decomposição. O trabalho é apresentado como uma resolução definitiva para a conjectura, baseando-se em uma combinação inovadora de combinatória de palavras cíclicas e lemas de paridade sobre corpos finitos.

Nota sobre Autoria
O artigo declara explicitamente que a prova deve inteiramente a "GPT 5.6 Pro", e a redação foi preparada com assistência de "GPT 5.6 Sol". O autor humano, Nikolay Ulyanov, reconhece o papel da IA na geração do argumento matemático e da exposição.