Erdős Problem #137: shared g-independent base layer

This file collects the low-level, g-independent helpers shared by every block route (JointFiniteness g = 3, SpliceFiniteness g = 5, and the parametric BlockFramework). It sits directly above Finiteness and below BlockFramework, so the generic framework and the concrete g = 3, 5 instances all derive from one base.

Two groups of helpers live here:

• Block-tiling / radical algebra (from the old JointFiniteness): the multiplicativity of F (F_add, F_dvd_F_add), the radical's prime support and factorization (rad_dvd_self, primeFactors_rad, factorization_rad, rad_dvd_rad_of_dvd), the elementary size bounds le_F, le_F', pow_le_F, the interval-divisor counts (Ioc_dvd_count, Ioc_dvd_le), and the Legendre i = 1 term div_le_factorization_factorial.
• The smooth/rough split (from the old SmoothRefinement): the primorial-type quantities P, L, the split Ssmooth/Rrough, and the smooth refinement rad (F k n) ^ 2 * L k ≤ F k n * P k ^ 2 (smooth_refinement).

None of these mentions any block length g (or the concrete B/W/overlap of a route), so they are proved once here and reused verbatim downstream.

Basic facts about F and block tilings

theorem Erdos137.F_add (a b n : ℕ) : F (a + b) n = F a n * F b (n + a)

F splits as a product of an initial block and a shifted tail: F (a + b) n = F a n * F b (n + a).

theorem Erdos137.F_dvd_F_add (a b n : ℕ) : F a n ∣ F (a + b) n

F a n divides F (a + b) n.

The radical's prime support and factorization (general facts)

theorem Erdos137.rad_dvd_self {m : ℕ} (_hm : m ≠ 0) : rad m ∣ m

rad m ∣ m for m ≠ 0.

theorem Erdos137.primeFactors_rad {m : ℕ} (hm : m ≠ 0) : (rad m).primeFactors = m.primeFactors

The prime support of rad m is exactly m.primeFactors (for m ≠ 0).

theorem Erdos137.factorization_rad {m : ℕ} (hm : m ≠ 0) (p : ℕ) : (rad m).factorization p = if p ∈ m.primeFactors then 1 else 0

General fact: rad m is squarefree, so (rad m).factorization p = 1 if p ∈ m.primeFactors, else 0.

theorem Erdos137.rad_dvd_rad_of_dvd {a b : ℕ} (hb : b ≠ 0) (hab : a ∣ b) : rad a ∣ rad b

rad is monotone under divisibility: a ∣ b, b ≠ 0 ⟹ rad a ∣ rad b (their prime supports are nested).

Elementary size bounds on F k n

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

n ≤ F k n for k ≥ 1, n ≥ 1 (the first factor is n, the rest are ≥ 1).

theorem Erdos137.le_F' {k n : ℕ} (hk : 1 ≤ k) (hn : 1 ≤ n) : k ≤ F k n

k ≤ F k n for k ≥ 1, n ≥ 1 (the last factor n+k-1 ≥ k divides the product).

theorem Erdos137.pow_le_F {k n : ℕ} : n ^ k ≤ F k n

Elementary lower bound n^k ≤ F k n. Each of the k factors of F k n is ≥ n. This is the size input (log F ≥ k log n) that turns W ≤ k^k into the clean n > k^6 threshold.

Counting multiples of a prime in an interval (for the overlap bound)

theorem Erdos137.Ioc_dvd_count (a b p : ℕ) (hab : a ≤ b) : {x ∈ Finset.Ioc a b | p ∣ x}.card = b / p - a / p

Exact count of multiples of p in (a, b]: #{x ∈ Ioc a b | p ∣ x} = b/p − a/p.

theorem Erdos137.Ioc_dvd_le (a L p : ℕ) (hp : 1 ≤ p) : {x ∈ Finset.Ioc a (a + L) | p ∣ x}.card ≤ L / p + 1

The number of multiples of p in an interval of length L is at most ⌊L/p⌋ + 1.

theorem Erdos137.div_le_factorization_factorial {k p : ℕ} (hp : Nat.Prime p) : k / p ≤ k.factorial.factorization p

For a prime p, ⌊k/p⌋ ≤ (k!).factorization p (the i = 1 term of Legendre's formula).

The primorial-type quantities P k and L k

def Erdos137.P (k : ℕ) : ℕ

P k = ∏_{p ∈ primesBelow k} p — the product of the primes < k (the primorial of k).

Equations

• Erdos137.P k = ∏ p ∈ k.primesBelow, p

def Erdos137.L (k : ℕ) : ℕ

L k = ∏_{p ∈ primesBelow k} p ^ (k / p) — the smooth-part lower bound (L ∣ k! by Legendre, L = (k!)^{1-o(1)}).

Equations

• Erdos137.L k = ∏ p ∈ k.primesBelow, p ^ (k / p)

theorem Erdos137.P_pos (k : ℕ) : 1 ≤ P k

theorem Erdos137.L_pos (k : ℕ) : 1 ≤ L k

theorem Erdos137.L_ne_zero (k : ℕ) : L k ≠ 0

theorem Erdos137.P_le_4_pow (k : ℕ) : P k ≤ 4 ^ k

P k ≤ 4 ^ k (Mathlib's primorial_le_four_pow; primesBelow k are the primes ≤ k - 1, a subset of the primes counted by primorial k).

The smooth/rough split of F k n

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

The smooth part S k n = ∏_{p | F, p < k} p ^ v_p(F).

Equations

• Erdos137.Ssmooth k n = ∏ p ∈ (Erdos137.F k n).primeFactors with p < k, p ^ (Erdos137.F k n).factorization p

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

The rough part R k n = ∏_{p | F, ¬ p < k} p ^ v_p(F).

Equations

• Erdos137.Rrough k n = ∏ p ∈ (Erdos137.F k n).primeFactors with ¬p < k, p ^ (Erdos137.F k n).factorization p

theorem Erdos137.Ssmooth_mul_Rrough {k n : ℕ} (hn : 1 ≤ n) : Ssmooth k n * Rrough k n = F k n

S · R = F for n ≥ 1.

theorem Erdos137.Ssmooth_pos {k n : ℕ} (_hn : 1 ≤ n) : 1 ≤ Ssmooth k n

theorem Erdos137.Rrough_pos {k n : ℕ} (_hn : 1 ≤ n) : 1 ≤ Rrough k n

Bound on the smooth radical: rad(S)^2 ≤ P^2

theorem Erdos137.smooth_rad_dvd_P {k n : ℕ} : ∏ p ∈ (F k n).primeFactors with p < k, p ∣ P k

∏_{p | F, p < k} p ∣ P k: the smooth prime factors are a subset of primesBelow k.

theorem Erdos137.smooth_rad_le_P {k n : ℕ} : ∏ p ∈ (F k n).primeFactors with p < k, p ≤ P k

∏_{p | F, p < k} p ≤ P k.

Bound on the rough part: ∏_{p | F, ¬ p<k} p^2 ≤ R (powerful)

theorem Erdos137.rough_sq_le {k n : ℕ} (hF : F k n ≠ 0) (hP : Powerful (F k n)) : (∏ p ∈ (F k n).primeFactors with ¬p < k, p) ^ 2 ≤ Rrough k n

For powerful F (≠ 0), ∏_{p|F, ¬p<k} p^2 ≤ R k n: each such prime has v_p(F) ≥ 2.

The smooth lower bound: L ∣ S and L ≤ S

We need v_p(F) ≥ ⌊k/p⌋ for every prime p < k. Among the k consecutive integers n, …, n+k-1 (the multiset (n-1, n-1+k] shifted), at least ⌊k/p⌋ are divisible by p, and each such factor contributes at least 1 to v_p(F).

theorem Erdos137.div_le_factorization_F {k n p : ℕ} (hn : 1 ≤ n) (hp : Nat.Prime p) : k / p ≤ (F k n).factorization p

The count of multiples of p among the k consecutive integers n, …, n+k-1 is at least ⌊k/p⌋. Stated via the exact Ioc count: #{x ∈ (n-1, n-1+k] | p ∣ x} = (n-1+k)/p − (n-1)/p ≥ k/p.

theorem Erdos137.L_dvd_F {k n : ℕ} (hn : 1 ≤ n) : L k ∣ F k n

L k ∣ F k n for n ≥ 1: v_p(L) = ⌊k/p⌋ ≤ v_p(F) for every prime p < k.

theorem Erdos137.L_le_smooth {k n : ℕ} (hn : 1 ≤ n) : L k ∣ Ssmooth k n

L k ≤ S k n (the smooth part): L ∣ F and L's primes are exactly the smooth primes, so in fact L ∣ S; we only need L ≤ S.

rad (F k n) factored through the smooth/rough split

theorem Erdos137.rad_smooth_rough_split (k n : ℕ) : rad (F k n) = (∏ p ∈ (F k n).primeFactors with p < k, p) * ∏ p ∈ (F k n).primeFactors with ¬p < k, p

rad (F k n) = (∏_{p|F, p<k} p) · (∏_{p|F, ¬p<k} p).

The smooth refinement

theorem Erdos137.smooth_refinement {k n : ℕ} (hn : 1 ≤ n) (hP : Powerful (F k n)) : rad (F k n) ^ 2 * L k ≤ F k n * P k ^ 2

Smooth-part radical refinement. For n ≥ 1 and a powerful F k n, rad (F k n) ^ 2 * L k ≤ F k n * P k ^ 2. Equivalently rad(F)^2 ≤ (P^2 / L) · F; this sharpens the crude rad(F)^2 ≤ F (powerful_rad_sq_le) by the smooth gain L.