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

技术摘要：Erdős–Sós 两两之和问题中 5/8 界的锐利上界

问题陈述
本文研究了关于两两之和（pairwise sums）的 Erdős–Sós 猜想的一个特定情形。令 $f_3(N)$ 表示最小整数，使得任何满足 $|A| \geq f_3(N)$ 的子集 $A \subseteq \{1, \dots, N\}$ 都包含三个互不相同的元素 $a, b, c \in A$，使得它们的两两之和 $a+b$、$a+c$ 和 $b+c$ 均包含在 $A$ 中。被称为“两两之和三元组自由”（pairwise-sum triple-free）的集合是指不存在此类三元组的集合。该研究的核心目标是确定 $f_3(N)$ 的渐近行为。

在此项工作之前，一个标准构造 $A = [\frac{N}{8}, \frac{N}{4}] \cup [\frac{N}{2}, N]$ 表明 $f_3(N) \geq \frac{5}{8}N + O(1)$。本文的目标是证明与之匹配的上界，从而解决 Erdős 问题 865，并确定精确的渐近常数。

方法论
该证明是自洽的，依赖于组合归纳法、加法数论以及一种“折叠”（folding）技术。其方法论通过以下关键步骤进行：

1. 折叠加法引理 (Lemma 2.1)：
   作者首先建立了一个关于“折叠”区间的引理。对于一个集合 $B \subseteq \{1, \dots, m-1\}$，若其中任意两个不同元素的和不等于 $m$ 也不等于模 $m$ 意义下的 $B$ 中元素，则该引理界定了 $B$ 相对于“碰撞集” $C(B)$ 的大小。具体而言，它证明了 $|B| - |C(B)| \leq \frac{m}{4} + 2$。该证明利用了反射对称性（$B \to -B$）和对 $|B|$ 的归纳论证，分析了两个最小元素之和是否属于 $C(B)$ 的情况。

2. 折叠引理 (Lemma 3.1)：
   作者引入了围绕枢轴元素 $h \in A$ 的“折叠”操作。通过将集合 $A$ 划分为小于 $h$ 的元素（$X$）以及形式为 $h+r$ 且 $r < h$ 的元素（$Y$），作者将 $A$ 的大小与交集 $B_h = X \cap Y$ 的结构联系起来。该引理表明，如果 $A$ 是三元组自由的，则 $|X| + |Y|$ 的和被 $\frac{5}{4}h - |E \setminus C(B_h)| + 1$ 所限制，其中 $E$ 代表区间 $[1, h-1]$ 中的“空隙”。这一步有效地将界定全局集合大小的问题转化为分析模 $h$ 的局部加法性质。

3. 归纳上界 (第 4 节)：
   主定理通过对 $H$（其中 $N=2H$）进行强归纳法得到证明。证明根据区间下半部分的最大元素与上半部分最小元素之间的间隙分为两种情况：

   • 情况 1 ($s \leq 4e$)： 围绕枢轴 $h = q$（上半部分中最小的元素）进行折叠。作者表明，由于 $A$ 的下部与上部之间的间隙，强制产生了足够数量的“缺失”元素（$|E \setminus C(B_h)|$）以满足该界限。
   • 情况 2 ($s > 4e$)： 围绕枢轴 $h = p$（下半部分中最大的元素）进行折叠。在这种情况下，巨大的间隙意味着集合的下部是稀疏的。作者对下半部分应用归纳假设，并结合折叠引理来推导该界限。

主要贡献与结果

• 锐利上界： 本文证明了对于所有 $N$，任何满足 $|A| \geq \frac{5}{8}N + C$（其中 $C$ 为某个绝对常数）的子集 $A \subseteq [1, N]$ 都包含一个两两之和三元组。
• 解决 Erdős 问题 865： 通过将新的上界与现有的下界构造相结合，本文确立了 $f_3(N) = \frac{5}{8}N + O(1)$。这证实了常数 $5/8$ 是最优的。
• 形式化： 作者指出，此前关于从粗略界限到锐利界限简化的条件版本已在 Lean 4/Mathlib 中完成了形式化。该形式化过程没有使用任何 “sorries”（占位符）且未添加任何公理，验证了简化步骤的逻辑正确性。
• 精细化猜想： 文中提到了由 Stijn Cambie 提出的关于特定 $N \pmod 8$ 时精确最大规模的更精细的猜想，但主要结果仍保持为渐近的 $5/8$ 界限。

意义
本文声称通过提供一个自洽的证明，解决了 Erdős 问题 865 中的锐利 $5/8$ 上界。其意义在于填补了已知构造与该特定两两之和问题理论上限之间的空白。这项工作被呈现为一个完整的数学证明，并通过 Lean 进行的形式化还原增加了严谨性，确保了组合论证的有效性，而不依赖于未经验证的假设。作者明确指出，证明是自洽的，且所有隐含常数均为绝对常数。