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

Sintesi Tecnica: Un Limite Netto di 5/8 per un Problema delle Somme a Coppie di Erdős–Sós

Enunciato del Problema
Il saggio affronta un caso specifico della congettura di Erdős–Sós riguardante le somme a coppie. Sia $f_3(N)$ il minimo intero tale che ogni sottoinsieme $A \subseteq \{1, \dots, N\}$ con $|A| \geq f_3(N)$ contenga elementi distinti $a, b, c \in A$ soddisfacendo la condizione che le loro somme a coppie $a+b$, $a+c$ e $b+c$ siano tutte contenute in $A$. Un tale insieme è definito "privo di triple di somme a coppie" se non esiste tale tripla. Il problema centrale è determinare il comportamento asintotico di $f_3(N)$.

Prima di questo lavoro, una costruzione standard $A = [\frac{N}{8}, \frac{N}{4}] \cup [\frac{N}{2}, N]$ ha dimostrato che $f_3(N) \geq \frac{5}{8}N + O(1)$. L'obiettivo del saggio è dimostrare il limite superiore corrispondente, risolvendo così il Problema 865 di Erdős e stabilendo la costante asintotica esatta.

Metodologia
La dimostrazione è autosufficiente e si basa su una combinazione di induzione combinatoria, teoria additiva dei numeri e una tecnica di "ripiegamento" (folding). La metodologia procede attraverso queste fasi chiave:

1. Il Lemma Additivo Ripiegato (Lemma 2.1):
   Gli autori stabiliscono innanzitutto un lemma su un intervallo "ripiegato". Per un insieme $B \subseteq \{1, \dots, m-1\}$ dove nessuna coppia distinta somma a $m$ o a un altro elemento in $B$ (modulo $m$), il lemma limita la dimensione di $B$ rispetto all'insieme delle "collisioni" $C(B)$. Nello specifico, dimostra che $|B| - |C(B)| \leq \frac{m}{4} + 2$. La dimostrazione utilizza la simmetria di riflessione ($B \to -B$) e un argomento induttivo su $|B|$, analizzando i casi in cui la somma dei due elementi più piccoli appartiene a $C(B)$ o meno.

2. Il Lemma di Ripiegamento (Lemma 3.1):
   Gli autori introducono un'operazione di "ripiegamento" attorno a un elemento pivot $h \in A$. Partizionando l'insieme $A$ in elementi minori di $h$ ($X$) ed elementi della forma $h+r$ dove $r < h$ ($Y$), essi relazionano la dimensione di $A$ alla struttura dell'intersezione $B_h = X \cap Y$. Il lemma dimostra che se $A$ è privo di triple, la somma delle dimensioni $|X| + |Y|$ è limitata da $\frac{5}{4}h - |E \setminus C(B_h)| + 1$, dove $E$ rappresenta i "vuoti" nell'intervallo $[1, h-1]$. Questo passaggio riduce efficacemente il problema di limitare la dimensione globale dell'insieme all'analisi delle proprietà additive locali modulo $h$.

3. Limite Superiore Induttivo (Sezione 4):
   Il teorema principale è dimostrato per induzione forte su $H$ (dove $N=2H$). La dimostrazione si divide in due casi basati sul divario tra l'elemento più grande nella metà inferiore dell'intervallo e l'elemento più piccolo nella metà superiore:

   • Caso 1 ($s \leq 4e$): L'insieme viene ripiegato attorno al pivot $h = q$ (il più piccolo elemento della metà superiore). Gli autori mostrano che il divario tra la parte inferiore e quella superiore di $A$ impone un numero sufficiente di elementi "mancanti" ($|E \setminus C(B_h)|$) per soddisfare il limite.
   • Caso 2 ($s > 4e$): L'insieme viene ripiegato attorno a $h = p$ (il più grande elemento della metà inferiore). In questo caso, il grande divario implica che la porzione inferiore dell'insieme sia sparsa. Gli autori applicano l'ipotesi induttiva al segmento inferiore e combinano questo con il lemma di ripiegamento per derivare il limite.

Contributi Chiave e Risultati

• Limite Superiore Netto: Il saggio dimostra che per ogni $N$, ogni sottoinsieme $A \subseteq [1, N]$ con $|A| \geq \frac{5}{8}N + C$ (per una certa costante assoluta $C$) contiene una tripla di somme a coppie.
• Risoluzione del Problema 865 di Erdős: Combinando il nuovo limite superiore con la costruzione del limite inferiore esistente, il saggio stabilisce che $f_3(N) = \frac{5}{8}N + O(1)$. Ciò conferma che la costante $5/8$ è la migliore possibile.
• Formalizzazione: Gli autori notano che una versione condizionale precedente della riduzione da un limite più grossolano al limite netto è stata formalizzata in Lean 4/Mathlib. Questa formalizzazione non utilizza "sorries" (segnaposti) né assiomi aggiunti, verificando la validità logica dei passaggi di riduzione.
• Congettura Raffinata: Il saggio menziona una formula congetturale più precisa suggerita da Stijn Cambie riguardo alla dimensione massima esatta per specifici $N$ modulo 8, sebbene il risultato primario rimanga il limite asintotico di $5/8$.

Significatività
Il saggio sostiene di risolvere il Problema 865 di Erdős fornendo una dimostrazione autosufficiente del limite netto di $5/8$. La sua importanza risiede nel colmare il divario tra la costruzione nota e il limite teorico superiore per questo specifico problema di somme a coppie. Il lavoro è presentato come una prova matematica completa, con l'aggiunta del rigore di una riduzione formalizzata in Lean, garantendo la validità degli argomenti combinatori senza dipendere da assunzioni non verificate. Gli autori dichiarano esplicitamente che la dimostrazione è autosufficiente e che tutte le costanti implicite sono assolute.