Erdős Problem #137: the elementary structure of a "very bad interval"

Erdos137/Finiteness.lean and Erdos137/JointFiniteness.lean formalize the conditional finiteness of powerful products F k n = n(n+1)⋯(n+k-1) under radical lower bounds. This file isolates the elementary, deterministic structural facts attached to a very bad interval — Terence Tao's name (erdosproblems.com/137) for a block [n, n+k-1] whose product F k n is powerful.

The point is entirely valuation-theoretic and uses no radical/abc input:

• Among k consecutive integers a prime p ≥ k divides at most one factor, because two factors differ by < k ≤ p (prime_dvd_two_terms_eq).
• Hence in a very bad block, all of v_p(F k n) comes from that single factor n + i, and powerfulness forces v_p ≥ 2, so p ^ 2 ∣ n + i (veryBad_large_prime_sq).
• In particular a prime p that equals one of the factors and exceeds the block length cannot occur in a very bad block: it would have to be a square, which a prime is not (prime_term_gt_length_not_powerful, prime_in_block_not_powerful).

The last statement is exactly the elementary mechanism that pairs with a Baker–Harman–Pintz type input (a prime in every short interval [n, n+k-1]) to rule out very bad blocks: a single prime that is itself a term of the block and is larger than the block length kills powerfulness.

Tao's analytic density theorem (very bad intervals have density O(x^{2/5+o(1)})) is not formalized here; only the deterministic uniqueness/valuation facts above. The two-term linear relation extraction that is Tao's next step is likewise not formalized.

Main results (all unconditional — Mathlib's three axioms only)

• prime_dvd_two_terms_eq : a prime p ≥ k divides at most one of the k block factors.
• veryBad_large_prime_sq : in a very bad block, a prime p ≥ k dividing a factor squares it.
• prime_term_gt_length_not_powerful / prime_in_block_not_powerful : a prime that is a block factor and exceeds the block length prevents powerfulness.

def Erdos137.VeryBad (k n : ℕ) : Prop

A very bad interval (Tao, erdosproblems.com/137): the block [n, n+k-1] whose product F k n = ∏_{i<k}(n+i) is powerful. For k ≥ 2 this is exactly a powerful product of ≥ 2 consecutive integers; the difference of two factors being < k, together with the resulting coprimality of factors away from primes < k, is what feeds the Erdős #137 obstruction.

Equations

• Erdos137.VeryBad k n = Erdos137.Powerful (Erdos137.F k n)

theorem Erdos137.prime_dvd_two_terms_eq {p n k i j : ℕ} (_hp : Nat.Prime p) (hk : k ≤ p) (hi : i < k) (hj : j < k) (hpi : p ∣ n + i) (hpj : p ∣ n + j) : i = j

Prime uniqueness in a block. If a prime p is at least the block length k, it divides at most one of the k consecutive factors n, n+1, …, n+k-1: two distinct factors n+i, n+j with i, j < k differ by |i-j| < k ≤ p, so a common prime divisor would divide a nonzero number smaller than p, which is impossible.

theorem Erdos137.veryBad_large_prime_sq {p n k i : ℕ} (hp : Nat.Prime p) (hk : k ≤ p) (hi : i < k) (hn : 1 ≤ n) (hbad : VeryBad k n) (hpi : p ∣ n + i) : p ^ 2 ∣ n + i

Very bad block + large prime ⟹ the prime squares the unique factor it touches. If F k n is powerful, p ≥ k is prime, and p ∣ n + i for some i < k, then p ^ 2 ∣ n + i.

By prime_dvd_two_terms_eq the prime p divides only the factor n + i among the k block factors, so v_p(F k n) = ∑_{j<k} v_p(n+j) = v_p(n+i). Powerfulness gives p ^ 2 ∣ F k n, hence v_p(F k n) ≥ 2, so v_p(n+i) ≥ 2, i.e. p ^ 2 ∣ n + i.

theorem Erdos137.prime_term_gt_length_not_powerful {p n k i : ℕ} (hp : Nat.Prime p) (hpk : k < p) (hi : i < k) (hn : 1 ≤ n) (hterm : n + i = p) : ¬VeryBad k n

A prime factor exceeding the block length kills powerfulness. If p is prime, p > k (so p ≥ k), i < k, and the factor n + i equals p, then the block [n, n+k-1] is not very bad: powerfulness would force p ^ 2 ∣ n + i = p by veryBad_large_prime_sq, impossible for a prime p ≥ 2.

This is the elementary lemma that combines with a Baker–Harman–Pintz prime-in-short-interval input: a prime p > k lying inside [n, n+k-1] cannot occur in a very bad interval.

theorem Erdos137.prime_in_block_not_powerful {p n k : ℕ} (hp : Nat.Prime p) (hpk : k < p) (hn : 1 ≤ n) (hmem : ∃ i < k, n + i = p) : ¬Powerful (F k n)

Restatement. If some factor of the block equals a prime p larger than the block length k, then F k n is not powerful. (Directly: prime_term_gt_length_not_powerful unfolding VeryBad.)