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

Technical Summary: Optimality of Wouter van Doorn's Upper Bound for the Mayer–Erdős Farey Problem

Problem Statement
The paper addresses a specific question regarding the Farey sequence of order $n$, denoted $F_n$, which consists of all reduced fractions $a/b \in [0, 1]$ with $b \le n$, arranged in increasing order. The central object of study is the concept of "badly ordered" pairs. Two fractions $a/b < c/d$ in $F_n$ are defined as badly ordered if their numerators increase while their denominators decrease (i.e., $a < c$ and $b > d$).

The paper investigates the quantity $f(n)$, defined as the minimum number of Farey fractions strictly between any two badly ordered fractions in $F_n$. This problem is equivalent to Erdős Problem 1005, which asks for the asymptotic constant $c$ such that the largest guaranteed range of similarly ordered Farey fractions is asymptotic to $cn$. While Mayer initiated the question and Erdős established a linear lower bound, the precise asymptotic constant remained open. Recent work by Wouter van Doorn established the upper bound $f(n) \le n/4 + O(1)$ and conjectured that this bound is optimal.

Methodology
The proof is elementary yet delicate, relying on a combination of analytic number theory and combinatorial estimates. The strategy is divided into establishing a matching lower bound and reviewing the existing upper bound.

1. Reduction to Elementary Intervals:
   The authors first demonstrate that any badly ordered pair $a/b < c/d$ contains a specific "elementary interval" $I_{a,b} = (a/b, (a+1)/(b-1))$. Consequently, proving the lower bound for $f(n)$ reduces to showing that for all valid $a, b$, the number of Farey fractions in $I_{a,b}$ is at least $n/4 - o(n)$.

2. Auxiliary Estimates:
   The proof utilizes several key lemmas:

   • Primitive Progressions: An estimate for the number of coprime solutions to linear Diophantine equations within a range.
   • Uniform Farey Count: A standard estimate for the number of Farey fractions in an arbitrary interval $J$, given by $\frac{3}{\pi^2}|J|n^2 + O(n \log n)$.
   • Farey Gaps: Properties of consecutive fractions in $F_Q$, specifically that the gap length is $1/ss'$ and the sum of denominators exceeds $Q$.
   • Totient Increments (The Core Engine): A critical lemma (Lemma 5) concerning the function $S(x) = \sum_{1 \le e < x} (1 - e/x)\frac{\phi(e)}{e}$. The authors prove that $S(x+y) - S(x) \ge y/4$ for $x \ge 0, y \ge 2$. This inequality is the source of the constant $1/4$.

3. Case Analysis for the Lower Bound:
   To prove the uniform lower bound for $N_n(a, b)$ (the count of fractions in $I_{a,b}$), the authors split the analysis based on the denominator $b$ and the presence of "small" rationals within the interval:

   • Small Denominators: If $b$ is small ($b \le n/\log^2 n$), the standard uniform Farey count suffices.
   • Large Denominators: If $b$ is large, the interval is analyzed relative to the Farey sequence of a lower order $Q = \lfloor b^{2/3} \rfloor$.
     • Case A (Small Rational Inside): If $I_{a,b}$ contains a reduced rational $h/s$ with $s \le Q$, the count is bounded below using a weighted sum of totient functions, leveraging Lemma 5 to show the sum is at least $s/4$.
     • Case B (No Small Rational Inside): If no such rational exists, $I_{a,b}$ lies within a gap of $F_Q$. The authors analyze the endpoints of this gap, showing that the "small" endpoint (with denominator $O(b^{1/3})$) allows for a similar totient-sum estimation, again yielding the $n/4$ bound.

4. Upper Bound:
   The paper includes the construction by van Doorn to demonstrate the upper bound. By choosing specific fractions $L = (2m-1)/4m$ and $R = 2m/(4m-1)$ (where $m \approx n/4$), the authors show that the number of fractions between them is exactly $m + O(1) \approx n/4$.

Key Contributions and Results

• Main Theorem: The paper proves that $f(n) = (1/4 + o(1))n$.
• Optimality: This result confirms Wouter van Doorn's conjecture that his upper bound $f(n) \le n/4 + O(1)$ is optimal in terms of the asymptotic constant.
• Resolution of Erdős Problem 1005: The work determines the requested asymptotic constant for Erdős Problem 1005 to be exactly $c = 1/4$.
• Technical Innovation: The proof introduces a robust one-dimensional increment estimate for a weighted totient sum (Lemma 5), which serves as the engine for deriving the $1/4$ constant.

Significance
The paper resolves a long-standing question in the theory of Farey sequences by pinning down the exact asymptotic behavior of the minimum gap between badly ordered fractions. By matching the upper bound with a rigorous lower bound, the authors close the gap on the constant $c$, establishing it as $1/4$. The work is noted for being elementary in its tools (avoiding heavy machinery) but delicate in its execution, particularly in the uniform handling of the totient sums across different ranges of denominators. The result is further validated by a formalization in Lean 4, ensuring the correctness of the proof strategy.