Erdős Problem #137: term-level rough-part structure in a very bad interval

If the block product F k n = n(n+1)⋯(n+k-1) is powerful, then for each individual term n+i, the part supported on primes p ≥ k is itself powerful. A prime p ≥ k divides at most one of the k block factors, so powerfulness of the whole product forces p^2 ∣ n+i. This is the local anatomy behind Tao's "very bad interval" language. No abc, no radical lower bound, no analytic number theory.

def Erdos137.SmoothPartBelow (k m : ℕ) : ℕ

The part of m supported on primes < k.

Equations

• Erdos137.SmoothPartBelow k m = ∏ p ∈ m.primeFactors with p < k, p ^ m.factorization p

def Erdos137.RoughPartAbove (k m : ℕ) : ℕ

The part of m supported on primes p ≥ k (written ¬ p < k to pair with Finset.prod_filter_mul_prod_filter_not).

Equations

• Erdos137.RoughPartAbove k m = ∏ p ∈ m.primeFactors with ¬p < k, p ^ m.factorization p

theorem Erdos137.smoothPartBelow_pos (k m : ℕ) : 1 ≤ SmoothPartBelow k m

theorem Erdos137.roughPartAbove_pos (k m : ℕ) : 1 ≤ RoughPartAbove k m

theorem Erdos137.roughPartAbove_ne_zero (k m : ℕ) : RoughPartAbove k m ≠ 0

theorem Erdos137.smoothPartBelow_mul_roughPartAbove {k m : ℕ} (hm : m ≠ 0) : SmoothPartBelow k m * RoughPartAbove k m = m

Term-level smooth/rough factorization: SmoothPartBelow k m * RoughPartAbove k m = m.

theorem Erdos137.roughPartAbove_dvd_self {k m : ℕ} (hm : m ≠ 0) : RoughPartAbove k m ∣ m

theorem Erdos137.factorization_roughPartAbove (k m p : ℕ) : (RoughPartAbove k m).factorization p = if p ∈ {q ∈ m.primeFactors | ¬q < k} then m.factorization p else 0

Factorization of the term-level rough part.

theorem Erdos137.prime_dvd_roughPartAbove_imp {k m p : ℕ} (hp : Nat.Prime p) (hpdvd : p ∣ RoughPartAbove k m) : p ∈ m.primeFactors ∧ k ≤ p

If a prime divides the rough part, it is a prime factor of m and is ≥ k.

theorem Erdos137.roughPartAbove_powerful_of_block_powerful {k n i : ℕ} (hn : 1 ≤ n) (hPow : Powerful (F k n)) (hi : i < k) : Powerful (RoughPartAbove k (n + i))

Rough part of each term is powerful in a very bad interval.

theorem Erdos137.term_decomposes_smooth_times_powerful_rough {k n i : ℕ} (hn : 1 ≤ n) (hPow : Powerful (F k n)) (hi : i < k) : SmoothPartBelow k (n + i) * RoughPartAbove k (n + i) = n + i ∧ Powerful (RoughPartAbove k (n + i))

Every term in a very bad interval = (k-smooth part) · (powerful k-rough part).

Squarefree terms have trivial rough part

theorem Erdos137.powerful_dvd_squarefree_eq_one {d m : ℕ} (hdne : d ≠ 0) (hmne : m ≠ 0) (hdvd : d ∣ m) (hsq : Squarefree m) (hPow : Powerful d) : d = 1

A nonzero powerful divisor of a nonzero squarefree number is 1. A small reusable helper: if d ∣ m, m is squarefree, and d is powerful, then every prime valuation of d is both ≥ 2 if nonzero (powerfulness) and ≤ 1 (since d ∣ m squarefree), so all valuations of d vanish.

theorem Erdos137.roughPartAbove_eq_one_of_squarefree_term {k n i : ℕ} (hn : 1 ≤ n) (hPow : Powerful (F k n)) (hi : i < k) (hsq : Squarefree (n + i)) : RoughPartAbove k (n + i) = 1

Squarefree term corollary. In a powerful block, the k-rough part of a squarefree term is trivial: if F k n is powerful and n+i is squarefree, then n+i has no prime factor p ≥ k, so all of its prime support lies below k.