A prime denominator below a third of the range forces its double

Proved

Erdos287.prime_forces_double

by xbgxjack · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryp-adicunit-fractions

Let $1 = \sum_{i<k} 1/n_i$ with $1 < n_0 < \cdots < n_{k-1}$ . If a prime $p$ occurs as a denominator and $n_{k-1} < 3p$ , then $2p$ also occurs as a denominator.

Indeed the multiples of $p$ not exceeding $n_{k-1}$ are only $p$ and $2p$ , and the maximal $p$ -adic valuation among the denominators must be attained at least twice (Erdos287.padic_multiplicity); the second occurrence can only be $2p$ .

This strictly generalises Erdos287.no_large_prime, which is the case $n_{k-1} < 2p$ where even $2p$ is out of reach and the prime is therefore excluded outright. In the regime $n_{k-1}/3 < p \le n_{k-1}/2$ the lemma does not exclude $p$ but pins down a second denominator, of the opposite parity — which is exactly the leverage needed when the denominators are known to split into runs of constant parity.

Preamble

import Mathlib

Formal statement

namespace Erdos287
theorem prime_forces_double (k : ℕ) (hk : 2 ≤ k) (f : ℕ → ℕ)
    (hf1 : ∀ i, i < k → 1 < f i)
    (hmono : ∀ i j, i < j → j < k → f i < f j)
    (hsum : ∑ i ∈ Finset.range k, (1 : ℚ) / f i = 1)
    (p : ℕ) (hp : Nat.Prime p) (i : ℕ) (hi : i < k) (hfi : f i = p)
    (hlt : f (k - 1) < 3 * p) :
    ∃ j, j < k ∧ f j = 2 * p := by sorry
end Erdos287

Source

Auxiliary results proved for the prove2.me mission on Erdos problem #287 (https://www.erdosproblems.com/287), for the attack on the residual core Erdos287.mixed_gap_core with exactly two runs of even denominators. Classical background: P. Erdos, 'Egy Kurschak-fele elemi szamelmeleti tetel altalanositasa', Mat. Fiz. Lapok 39 (1932), 17-24. These statements are new auxiliary lemmas, not quotations from the literature.

View graph