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

Resumen Técnico: Un Límite Agudo de 5/8 para un Problema de Sumas por Pares de Erdős–Sós

Enunciado del Problema
El artículo aborda un caso específico de la conjetura de Erdős–Sós relativa a las sumas por pares. Sea $f_3(N)$ el menor entero tal que todo subconjunto $A \subseteq \{1, \dots, N\}$ con $|A| \geq f_3(N)$ contiene elementos distintos $a, b, c \in A$ que satisfacen la condición de que sus sumas por pares $a+b$, $a+c$ y $b+c$ están todas contenidas dentro de $A$. Tal conjunto se denomina "libre de triples de suma por pares" si no existe tal triple. El problema central es determinar el comportamiento asintótico de $f_3(N)$.

Antes de este trabajo, una construcción estándar $A = [\frac{N}{8}, \frac{N}{4}] \cup [\frac{N}{2}, N]$ demostró que $f_3(N) \geq \frac{5}{8}N + O(1)$. El objetivo del artículo es probar el límite superior correspondiente, resolviendo así el Problema 865 de Erdős y estableciendo la constante asintótica exacta.

Metodología
La demostración es autónoma y se basa en una combinación de inducción combinatoria, teoría de números aditivos y una técnica de "plegado" (folding). La metodología procede a través de los siguientes pasos clave:

1. El Lema de Suma Plegada (Lema 2.1):
   Los autores establecen primero un lema sobre un intervalo "plegado". Para un conjunto $B \subseteq \{1, \dots, m-1\}$ donde ningún par distinto suma $m$ o otro elemento en $B$ (módulo $m$), el lema acota el tamaño de $B$ en relación con el conjunto de "colisiones" $C(B)$. Específicamente, demuestra que $|B| - |C(B)| \leq \frac{m}{4} + 2$. La prueba utiliza la simetría de reflexión ($B \to -B$) y un argumento inductivo sobre $|B|$, analizando los casos donde la suma de los dos elementos más pequeños pertenece a $C(B)$ o no.

2. El Lema de Plegado (Lema 3.1):
   Los autores introducen una operación de "plegado" alrededor de un elemento pivote $h \in A$. Al particionar el conjunto $A$ en elementos menores que $h$ ($X$) y elementos de la forma $h+r$ donde $r < h$ ($Y$), relacionan el tamaño de $A$ con la estructura de la intersección $B_h = X \cap Y$. El lema demuestra que si $A$ es libre de triples, la suma de los tamaños $|X| + |Y|$ está acotada por $\frac{5}{4}h - |E \setminus C(B_h)| + 1$, donde $E$ representa los "huecos" en el intervalo $[1, h-1]$. Este paso reduce efectivamente el problema de acotar el tamaño global del conjunto al análisis de propiedades aditivas locales módulo $h$.

3. Límite Superior Inductivo (Sección 4):
   El teorema principal se prueba mediante inducción fuerte sobre $H$ (donde $N=2H$). La prueba se divide en dos casos basados en la brecha entre el elemento más grande en la mitad inferior del intervalo y el elemento más pequeño en la mitad superior:

   • Caso 1 ($s \leq 4e$): El conjunto se pliega alrededor del pivote $h = q$ (el elemento más pequeño en la parte superior). Los autores muestran que la brecha entre la parte inferior y la superior de $A$ fuerza un número suficiente de elementos "faltantes" ($|E \setminus C(B_h)|$) para satisfacer el límite.
   • Caso 2 ($s > 4e$): El conjunto se pliega alrededor de $h = p$ (el elemento más grande en la parte inferior). Aquí, la gran brecha implica que la porción inferior del conjunto es dispersa. Los autores aplican la hipótesis de inducción al segmento inferior y combinan esto con el lema de plegado para derivar el límite.

Contribuciones Clave y Resultados

• Límite Superior Agudo: El artículo demuestra que para todo $N$, todo subconjunto $A \subseteq [1, N]$ con $|A| \geq \frac{5}{8}N + C$ (para alguna constante absoluta $C$) contiene un triple de suma por pares.
• Resolución del Problema 865 de Erdős: Al combinar el nuevo límite superior con la construcción de límite inferior existente, el artículo establece que $f_3(N) = \frac{5}{8}N + O(1)$. Esto confirma que la constante $5/8$ es la mejor posible.
• Formalización: Los autores señalan que una versión condicional anterior de la reducción de un límite más grueso al límite agudo ha sido formalizada en Lean 4/Mathlib. Esta formalización no utiliza "sorries" (marcadores de posición) ni axiomas añadidos, verificando la solidez lógica de los pasos de reducción.
• Conjetura Refinada: El artículo menciona una fórmula conjetural más aguda sugerida por Stijn Cambie respecto al tamaño máximo exacto para valores específicos de $N$ módulo 8, aunque el resultado principal sigue siendo el límite asintótico de $5/8$.

Significado
El artículo afirma resolver el Problema 865 de Erdős al proporcionar una prueba autónoma del límite agudo de $5/8$. Su importancia radica en cerrar la breancia entre la construcción conocida y el límite teórico superior para este problema específico de sumas por pares. El trabajo se presenta como una prueba matemática completa, con la rigurosidad añadida de una reducción formalizada en Lean, asegurando la validez de los argumentos combinatorios sin depender de supuestos no verificados. Los autores declaran explícitamente que la prueba es autónoma y que todas las constantes implícitas son absolutas.