A sharp 5/8 bound for an Erd\H{o}s-Sós pairwise-sums problem

Resumo Técnico: Um Limite Estrito de 5/8 para um Problema de Somas Pares de Erdős–Sós

Enunciado do Problema
O artigo aborda um caso específico da conjectura de Erdős–Sós relativa a somas pares. Seja $f_3(N)$ o menor inteiro tal que todo subconjunto $A \subseteq \{1, \dots, N\}$ com $|A| \geq f_3(N)$ contém elementos distintos $a, b, c \in A$ satisfazendo a condição de que suas somas pares $a+b$, $a+c$ e $b+c$ estão todas contidas em $A$. Tal um conjunto é denominado "livre de triplas de somas pares" se nenhum tal triplo existe. O problema central é determinar o comportamento assintótico de $f_3(N)$.

Antes deste trabalho, uma construção padrão $A = [\frac{N}{8}, \frac{N}{4}] \cup [\frac{N}{2}, N]$ demonstrou que $f_3(N) \geq \frac{5}{8}N + O(1)$. O objetivo do artigo é provar o limite superior correspondente, resolvendo assim o Problema 865 de Erdős e estabelecendo a constante assintótica exata.

Metodologia
A prova é autossuficiente e baseia-se em uma combinação de indução combinatória, teoria aditiva dos números e uma técnica de "dobramento" (folding). A metodologia procede através das seguintes etapas principais:

1. O Lema Aditivo Dobrado (Lema 2.1):
   Os autores estabelecem primeiro um lema sobre um intervalo "dobrado". Para um conjunto $B \subseteq \{1, \dots, m-1\}$ onde nenhum par distinto soma $m$ ou outro elemento em $B$ (módulo $m$), o lema limita o tamanho de $B$ em relação ao conjunto de "colisões" $C(B)$. Especificamente, prova que $|B| - |C(B)| \leq \frac{m}{4} + 2$. A prova utiliza simetria de reflexão ($B \to -B$) e um argumento indutivo sobre $|B|$, analisando casos onde a soma dos dois menores elementos pertence a $C(B)$ ou não.

2. O Lema de Dobramento (Lema 3.1):
   Os autores introduzem uma operação de "dobramento" em torno de um elemento pivô $h \in A$. Ao particionar o conjunto $A$ em elementos menores que $h$ ($X$) e elementos da forma $h+r$ onde $r < h$ ($Y$), eles relacionam o tamanho de $A$ à estrutura da interseção $B_h = X \cap Y$. O lema demonstra que, se $A$ for livre de triplas, a soma dos tamanhos $|X| + |Y|$ é limitada por $\frac{5}{4}h - |E \setminus C(B_h)| + 1$, onde $E$ representa as "lacunas" no intervalo $[1, h-1]$. Esta etapa efetivamente reduz o problema de limitar o tamanho global do conjunto para analisar propriedades aditivas locais módulo $h$.

3. Limite Superior Indutivo (Seção 4):
   O teorema principal é provado por indução forte sobre $H$ (onde $N=2H$). A prova divide-se em dois casos baseados na lacuna entre o maior elemento na metade inferior do intervalo e o menor elemento na metade superior:

   • Caso 1 ($s \leq 4e$): O conjunto é dobrado em torno do pivô $h = q$ (o menor elemento na metade superior). Os autores mostram que a lacuna entre as partes inferior e superior de $A$ força um número suficiente de elementos "faltantes" ($|E \setminus C(B_h)|$) para satisfazer o limite.
   • Caso 2 ($s > 4e$): O conjunto é dobrado em torno de $h = p$ (o maior elemento na metade inferior). Aqui, a grande lacuna implica que a parte inferior do conjunto é esparsa. Os autores aplicam a hipótese de indução ao segmento inferior e combinam isso com o lema de dobramento para derivar o limite.

Contribuições Principais e Resultados

• Limite Superior Estrito: O artigo prova que, para todo $N$, todo subconjunto $A \subseteq [1, N]$ com $|A| \geq \frac{5}{8}N + C$ (para alguma constante absoluta $C$) contém uma tripla de soma par.
• Resolução do Problema 865 de Erdős: Combinando o novo limite superior com a construção de limite inferior existente, o artigo estabelece que $f_3(N) = \frac{5}{8}N + O(1)$. Isso confirma que a constante $5/8$ é a melhor possível.
• Formalização: Os autores observam que uma versão condicional anterior da redução de um limite mais grosseiro para o limite estrito foi formalizada em Lean 4/Mathlib. Esta formalização não utiliza "sorries" (espaços reservados) nem axiomas adicionais, verificando a validade lógica das etapas de redução.
• Conjectura Refinada: O artigo menciona uma fórmula conjectural mais precisa sugerida por Stijn Cambie em relação ao tamanho máximo exato para $N$ módulo 8, embora o resultado principal permaneça o limite assintótico de $5/8$.

Significância
O artigo afirma resolver o Problema 865 de Erdős ao fornecer uma prova autossuficiente do limite estrito de $5/8$. Sua significância reside em fechar a lacuna entre a construção conhecida e o limite teórico superior para este problema específico de somas pares. O trabalho é apresentado como uma prova matemática completa, com o rigor adicional de uma redução formalizada em Lean, garantindo a validade dos argumentos combinatórios sem depender de suposições não verificadas. Os autores declaram explicitamente que a prova é autossuficiente e que todas as constantes implícitas são absolutas.