Optimality of Wouter van Doorn's Upper Bound for the Mayer-Erd\H{o}s Farey Problem

技术摘要：Wouter van Doorn 关于 Mayer–Erdős 费雷序列（Farey Problem）上界的优越性研究

问题陈述
本文探讨了关于阶数为 $n$ 的费雷序列 $F_n$ 的一个特定问题。$F_n$ 由所有满足 $a/b \in [0, 1]$ 且 $b \le n$ 的最简分数组成，并按递增顺序排列。研究的核心对象是“排序不良”（badly ordered）对的概念。若两个费雷分数 $a/b < c/d$ 满足分子增加而分母减少（即 $a < c$ 且 $b > d$），则称它们为排序不良。

本文研究的量 $f(n)$ 定义为在 $F_n$ 中任意两个排序不良分数之间所包含的费雷分数的最小数量。该问题等价于 Erdős 问题 1005，该问题旨在寻找渐近常数 $c$，使得保证的同向排序费雷分数的最大范围渐近于 $cn$。Mayer 提出了这一问题，Erdős 确定了线性下界，但精确的渐近常数一直悬而未决。最近，Wouter van Doorn 确定了上界 $f(n) \le n/4 + O(1)$，并推测该上界是优的。

方法论
该证明过程虽然属于初等数学范畴，但过程精细，依赖于解析数论与组合估计的结合。其策略分为建立匹配的下界以及回顾现有的上界。

1. 简化为初等区间：
   作者首先证明任何排序不良对 $a/b < c/d$ 都包含一个特定的“初等区间” $I_{a,b} = (a/b, (a+1)/(b-1))$。因此，证明 $f(n)$ 的下界可以转化为证明对于所有有效的 $a, b$，区间 $I_{a,b}$ 内的费雷分数数量至少为 $n/4 - o(n)$。

2. 辅助估计：
   证明利用了几个关键引理：

   • 原初进展（Primitive Progressions）： 一个关于线性丢番图方程在一定范围内互质解数量的估计。
   • 一致费雷计数（Uniform Farey Count）： 给定任意区间 $J$ 内费雷分数数量的标准估计，即 $\frac{3}{\pi^2}|J|n^2 + O(n \log n)$。
   • 费雷间隙（Farey Gaps）： $F_Q$ 中连续分数的性质，特别是间隙长度为 $1/ss'$，且分母之和超过$Q$。
   • 欧拉函数增量（核心引擎）： 一个关于函数 $S(x) = \sum_{1 \le e < x} (1 - e/x)\frac{\phi(e)}{e}$ 的关键引理（引理 5）。作者证明了对于 $x \ge 0, y \ge 2$，有 $S(x+y) - S(x) \ge y/4$。该不等式是产生常数 $1/4$ 的来源。

3. 下界的分类讨论：
   为了证明 $N_n(a, b)$（即 $I_{a,b}$ 中的计数）的一致下界，作者根据分母 $b$ 以及区间内是否存在“小”有理数进行了分类讨论：

   • 小分母情况： 若 $b$ 较小（$b \le n/\log^2 n$），则使用标准的统一费雷计数即可。
   • 大分母情况： 若 $b$ 较大，则相对于低阶费雷序列 $Q = \lfloor b^{2/3} \rfloor$ 对区间进行分析。
     • 情况 A（区间内含有小有理数）： 若 $I_{a,b}$ 包含一个分母 $s \le Q$ 的最简有理数 $h/s$，则利用引理 5 通过加权欧拉函数和来对计数进行下界估计，从而显示该和至少为 $s/4$。
     • 情况 B（区间内不含小有理数）： 若不存在此类有理数，则 $I_{a,b}$ 位于 $F_Q$ 的一个间隙内。作者分析了该间隙的端点，表明“较小”的端点（其分母为 $O(b^{1/3})$）允许进行类似的欧拉函数和估计，从而同样得出 $n/4$ 的界限。

4. 上界：
   文中包含了 van Doorn 的构造，用以展示上界。通过选取特定的分数 $L = (2m-1)/4m$ 和 $R = 2m/(4m-1)$（其中 $m \approx n/4$），作者证明了两者之间的分数数量恰好为 $m + O(1) \approx n/4$。

主要贡献与结果

• 主定理： 本文证明了 $f(n) = (1/4 + o(1))n$。
• 优越性： 该结果证实了 Wouter van Doorn 的猜想，即他的上界 $f(n) \le n/4 + O(1)$ 在渐近常数意义上是优的。
• 解决 Erdős 问题 1005： 本工作确定了 Erdős 问题 1005 所请求的渐近常数恰好为 $c = 1/4$。
• 技术创新： 证明引入了一个稳健的一维加权欧拉函数和增量估计（引理 5），这成为了导出 $1/4$ 常数的引擎。

意义
本文通过确定排序不良对之间最小间隙的精确渐近行为，解决了费雷序列理论中的一个长期问题。通过将上界与严谨的下界相匹配，作者填补了常数 $c$ 的空白，将其确定为 $1/4$。该工作被认为在工具使用上是初等的（避免了沉重的数学工具），但在执行上非常精细，特别是在不同分母范围内对欧拉函数和进行统一处理方面。该结果通过 Lean 4 进行了形式化验证，确保了证明策略的正确性。