Erdős Problem #137: powerful products of consecutive integers (conditional finiteness)

Erdős Problem #137 asks whether the product of k ≥ 3 consecutive positive integers, F k n = n(n+1)⋯(n+k-1), can ever be powerful (a number N with p ∣ N ⟹ p² ∣ N).

This file formalizes the deduction that, under the Granville–Langevin radical lower bound RadLB k (a consequence of the abc conjecture, taken here as an explicit hypothesis — it is NOT proved here), F k n is powerful for only finitely many n, for each fixed k ≥ 3. The underlying mathematics is due to Shorey–Tijdeman (2016) and Langevin / Granville; this is a formalization of the deduction, not a new result.

Main results

• lemma_star (unconditional): rad m ^ 2 * B2 m ≤ m ^ 2.
• powerful_rad_sq_le: a powerful N ≠ 0 satisfies rad N ^ 2 ≤ N.
• erdos137_eventually_not_powerful / erdos137_finite (conditional on RadLB, k ≥ 3): F k n is powerful for only finitely many n.

The radical bound RadLB is the only nonelementary input and appears as a hypothesis.

Definitions

def Erdos137.rad (m : ℕ) : ℕ

The radical of m: product of its distinct prime factors. rad(0) = rad(1) = 1 by convention.

Equations

• Erdos137.rad m = ∏ p ∈ m.factorization.support, p

def Erdos137.B2 (m : ℕ) : ℕ

The 2-full (powerful) part of m: product of p^{a_p} over primes with a_p ≥ 2.

Equations

• Erdos137.B2 m = ∏ p ∈ m.factorization.support with 2 ≤ m.factorization p, p ^ m.factorization p

def Erdos137.F (k n : ℕ) : ℕ

Product of k consecutive integers starting at n.

Equations

• Erdos137.F k n = ∏ i ∈ Finset.range k, (n + i)

Auxiliary lemmas

theorem Erdos137.prime_of_mem_factorization_support {m p : ℕ} (hp : p ∈ m.factorization.support) : Nat.Prime p

Every element of the factorization support is a prime.

theorem Erdos137.rad_pos (m : ℕ) : 1 ≤ rad m

theorem Erdos137.F_pos {k n : ℕ} (hn : 1 ≤ n) : 1 ≤ F k n

theorem Erdos137.F_ne_zero {k n : ℕ} (hn : 1 ≤ n) : F k n ≠ 0

theorem Erdos137.factor_le_mul {k n i : ℕ} (_hk : 1 ≤ k) (hn : 1 ≤ n) (hi : i < k) : n + i ≤ k * n

theorem Erdos137.F_le_pow {k n : ℕ} (hk : 1 ≤ k) (hn : 1 ≤ n) : F k n ≤ (k * n) ^ k

LEMMA STAR

theorem Erdos137.lemma_star (m : ℕ) (hm : m ≠ 0) : rad m ^ 2 * B2 m ≤ m ^ 2

Bridge to ℝ

theorem Erdos137.B2_le_sq_div_rad_sq (m : ℕ) (hm : m ≠ 0) : ↑(B2 m) ≤ ↑m ^ 2 / ↑(rad m) ^ 2

theorem Erdos137.rad_cast_pos (m : ℕ) : 0 < ↑(rad m)

RadLB hypothesis and conditional theorem

def Erdos137.RadLB (k : ℕ) : Prop

The Granville--Langevin radical lower bound, taken as a hypothesis. For every ε > 0 there is C > 0 such that rad(F(k,n)) ≥ C · n^{k-1-ε} for all n ≥ 1.

Equations

• Erdos137.RadLB k = ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ↑(Erdos137.rad (Erdos137.F k n)) ≥ C * ↑n ^ (↑k - 1 - ε)

Erdős #137: conditional finiteness of powerful products

def Erdos137.Powerful (N : ℕ) : Prop

N is powerful if every prime dividing N divides it with multiplicity at least two, i.e. p ∣ N → p ^ 2 ∣ N for all primes p.

Equations

• Erdos137.Powerful N = ∀ (p : ℕ), Nat.Prime p → p ∣ N → p ^ 2 ∣ N

theorem Erdos137.powerful_B2_eq {N : ℕ} (hN : N ≠ 0) (hP : Powerful N) : B2 N = N

For powerful N, the 2-full part B2 N is all of N.

theorem Erdos137.powerful_rad_sq_le {N : ℕ} (hN : N ≠ 0) (hP : Powerful N) : rad N ^ 2 ≤ N

For powerful N ≠ 0, rad N ^ 2 ≤ N.

theorem Erdos137.erdos137_eventually_not_powerful (k : ℕ) (hk : 3 ≤ k) (hRadLB : RadLB k) : ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → ¬Powerful (F k n)

Main conditional finiteness theorem (k ≥ 3).

theorem Erdos137.erdos137_finite (k : ℕ) (hk : 3 ≤ k) (hRadLB : RadLB k) : {n : ℕ | 1 ≤ n ∧ Powerful (F k n)}.Finite

The set of positive n for which F k n is powerful is finite (k ≥ 3, conditional on RadLB).