Erdős Problem #137: the deterministic squarefree-capacity reduction

This file isolates the deterministic half of the squarefree-counting argument for very bad intervals. It contains no analytic number theory — no Pandey squarefree-counting theorem, no Baker–Harman–Pintz prime-in-interval input, no Mertens estimate. Everything below is a finite valuation computation checked on the standard Mathlib axioms, building on the elementary TaoPoint mechanism.

The mechanism

Suppose the block [n, n+k-1] is very bad, i.e. F k n = ∏_{i<k} (n+i) is powerful. Consider the squarefree terms of the block, those n + i with Squarefree (n + i). We claim:

• (no large prime) A squarefree term n + i has no prime factor p ≥ k. Indeed, if p ∣ n + i with p ≥ k prime, then veryBad_large_prime_sq forces p^2 ∣ n + i, i.e. (n+i).factorization p ≥ 2, contradicting Squarefree.natFactorization_le_one. (sqfree_term_no_large_prime.)

So every squarefree term is (k-1)-smooth: its prime support lies in Nat.primesBelow k.

• (per-prime capacity) For a fixed prime p < k, the number of block terms n + i (i < k) divisible by p is at most ⌊k/p⌋ + 1, by the interval-count Ioc_dvd_le (the same i ↦ n+i bijection idiom as div_le_factorization_F in Base). Each squarefree term contributes valuation ≤ 1 at p, so v_p(∏ squarefree terms) ≤ ⌊k/p⌋ + 1.

Hence pointwise on factorizations the squarefree product divides the small-prime capacity ∏_{p < k} p^{⌊k/p⌋+1}, and Nat.le_of_dvd yields the size form.

Note on the exponent

We use k/p + 1 (= ⌊k/p⌋ + 1), not a ceiling, because Ioc_dvd_le proves exactly the bound ⌊L/p⌋ + 1 on the number of multiples of p in an interval of length L = k.

Deterministic companion

This is the deterministic companion to an external, unformalized squarefree-counting theorem (Pandey) bounding the number of squarefree terms in a block. That analytic input is not formalized here; only the deterministic capacity bound for the product of the squarefree terms is.

Counting obstruction

Bounding each squarefree term below by n turns the product bound into a count bound. With SqfreeBlockCount k n := #{i < k | Squarefree (n+i)} we have n ^ SqfreeBlockCount k n ≤ SqfreeBlockProduct k n ≤ SmoothCapacity k, and the capacity factors as SmoothCapacity k = L k * P k ≤ k! · 4^k ≤ (4k)^k (Legendre's first layer L ∣ k! plus the primorial bound P ≤ 4^k). Hence enough squarefree terms forces non-powerfulness: not_powerful_of_sqfree_count_beats_fourk says (4k)^k < n ^ SqfreeBlockCount k n ⟹ ¬ Powerful. This is the deterministic interface to an external squarefree-count lower bound (Pandey, not formalized here): supply any n and a count exceeding log_n ((4k)^k) and the block cannot be powerful.

Main results (Mathlib's three axioms only)

• sqfree_term_no_large_prime : a squarefree block term has no prime factor ≥ k.
• powerful_sqfree_product_dvd_smooth_capacity : the squarefree product divides the capacity.
• powerful_sqfree_product_le_smooth_capacity : the size form (via Nat.le_of_dvd).
• powerful_sqfree_count_capacity_bound : the counting form n^count ≤ SmoothCapacity.
• smoothCapacity_eq_L_mul_P, smoothCapacity_le_four_mul_pow : capacity = L·P ≤ (4k)^k.
• not_powerful_of_sqfree_count_beats_fourk : explicit count ⟹ non-powerful obstruction.

The squarefree-term index set, its product, and the smooth capacity

def Erdos137.SqfreeBlockIndices (k n : ℕ) : Finset ℕ

The indices i < k whose block term n + i is squarefree.

Equations

• Erdos137.SqfreeBlockIndices k n = {i ∈ Finset.range k | Squarefree (n + i)}

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

The product of the squarefree block terms ∏_{i : Squarefree (n+i)} (n + i).

Equations

• Erdos137.SqfreeBlockProduct k n = ∏ i ∈ Erdos137.SqfreeBlockIndices k n, (n + i)

def Erdos137.SmoothCapacity (k : ℕ) : ℕ

The small-prime capacity ∏_{p < k} p^{⌊k/p⌋+1}. The exponent is k/p + 1 (not a ceiling), matching exactly what Ioc_dvd_le proves about the count of multiples of p in a length-k interval.

Equations

• Erdos137.SmoothCapacity k = ∏ p ∈ k.primesBelow, p ^ (k / p + 1)

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

theorem Erdos137.smoothCapacity_pos (k : ℕ) : 1 ≤ SmoothCapacity k

theorem Erdos137.smoothCapacity_ne_zero (k : ℕ) : SmoothCapacity k ≠ 0

The deterministic obstruction: squarefree terms have no large prime

theorem Erdos137.sqfree_term_no_large_prime {k n i p : ℕ} (hn : 1 ≤ n) (hPow : Powerful (F k n)) (hi : i < k) (hsq : Squarefree (n + i)) (hp : Nat.Prime p) (hkp : k ≤ p) : ¬p ∣ n + i

No large prime in a squarefree term. If F k n is powerful, i < k, n + i is squarefree, and p ≥ k is prime, then p ∤ n + i. Otherwise veryBad_large_prime_sq forces p^2 ∣ n + i, contradicting squarefreeness (Squarefree.natFactorization_le_one).

Per-prime valuation bound

def Erdos137.BlockDvdIndices (k n p : ℕ) : Finset ℕ

The set of squarefree-term indices whose term is divisible by p.

Equations

• Erdos137.BlockDvdIndices k n p = {i ∈ Erdos137.SqfreeBlockIndices k n | p ∣ n + i}

theorem Erdos137.blockDvdIndices_card_le {k n p : ℕ} (hn : 1 ≤ n) (hp : 1 ≤ p) : (BlockDvdIndices k n p).card ≤ k / p + 1

Per-prime capacity count. For p ≥ 1, the number of squarefree-term indices i with p ∣ n + i is at most ⌊k/p⌋ + 1. The squarefree-divisible index set is a subset of all indices i < k with p ∣ n + i, which biject (via i ↦ n + i) onto {x ∈ (n-1, n-1+k] | p ∣ x}, counted by Ioc_dvd_le (the same idiom as div_le_factorization_F).

theorem Erdos137.sqfreeBlockProduct_factorization_le_count {k n p : ℕ} (hn : 1 ≤ n) : (SqfreeBlockProduct k n).factorization p ≤ (BlockDvdIndices k n p).card

Valuation of the squarefree product at p is bounded by the count. Each squarefree term contributes valuation ≤ 1 at p (and 0 if p ∤ n+i), so summing over the squarefree indices gives v_p(∏) ≤ #{i : Squarefree ∧ p ∣ n+i} = #(BlockDvdIndices k n p).

theorem Erdos137.smoothCapacity_factorization (k p : ℕ) : (SmoothCapacity k).factorization p = if p ∈ k.primesBelow then k / p + 1 else 0

Factorization of the capacity. For prime p < k, v_p(SmoothCapacity k) = ⌊k/p⌋ + 1; for p ∉ primesBelow k, it is 0.

Main results

theorem Erdos137.powerful_sqfree_product_dvd_smooth_capacity {k n : ℕ} (hn : 1 ≤ n) (hPow : Powerful (F k n)) : SqfreeBlockProduct k n ∣ SmoothCapacity k

The squarefree product divides the small-prime capacity. If F k n is powerful, then ∏_{i : Squarefree (n+i)} (n+i) divides ∏_{p < k} p^{⌊k/p⌋+1}. Pointwise on factorizations: a prime p ≥ k cannot divide any squarefree term (sqfree_term_no_large_prime), so its valuation in the product is 0 ≤ the capacity's; a prime p < k has valuation ≤ #(divisible squarefree terms) ≤ ⌊k/p⌋ + 1 (sqfreeBlockProduct_factorization_le_count, blockDvdIndices_card_le); a non-prime contributes 0.

theorem Erdos137.powerful_sqfree_product_le_smooth_capacity {k n : ℕ} (hn : 1 ≤ n) (hPow : Powerful (F k n)) : SqfreeBlockProduct k n ≤ SmoothCapacity k

Size form. If F k n is powerful, the product of the squarefree block terms is at most the small-prime capacity ∏_{p < k} p^{⌊k/p⌋+1}. Immediate from the divisibility form via Nat.le_of_dvd.

Counting form of the obstruction and explicit capacity bound

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

Number of squarefree terms in the block.

Equations

• Erdos137.SqfreeBlockCount k n = (Erdos137.SqfreeBlockIndices k n).card

theorem Erdos137.sqfreeBlockProduct_ge_pow {k n : ℕ} : n ^ SqfreeBlockCount k n ≤ SqfreeBlockProduct k n

The product of the squarefree block terms is at least n ^ SqfreeBlockCount.

theorem Erdos137.powerful_sqfree_count_capacity_bound {k n : ℕ} (hn : 1 ≤ n) (hPow : Powerful (F k n)) : n ^ SqfreeBlockCount k n ≤ SmoothCapacity k

Counting form of the squarefree-capacity obstruction.

theorem Erdos137.not_powerful_of_sqfree_capacity_exceeded {k n : ℕ} (hn : 1 ≤ n) (hcap : SmoothCapacity k < n ^ SqfreeBlockCount k n) : ¬Powerful (F k n)

If the squarefree count is large enough to beat capacity, the block is not powerful.

theorem Erdos137.smoothCapacity_eq_L_mul_P (k : ℕ) : SmoothCapacity k = L k * P k

The squarefree-capacity product is exactly L k * P k.

theorem Erdos137.L_dvd_factorial (k : ℕ) : L k ∣ k.factorial

L k divides k! (Legendre's first layer).

theorem Erdos137.L_le_factorial (k : ℕ) : L k ≤ k.factorial

theorem Erdos137.smoothCapacity_le_four_mul_pow (k : ℕ) : SmoothCapacity k ≤ (4 * k) ^ k

Coarse explicit capacity bound: SmoothCapacity k ≤ (4*k)^k.

theorem Erdos137.not_powerful_of_sqfree_count_beats_fourk {k n : ℕ} (hn : 1 ≤ n) (hbeat : (4 * k) ^ k < n ^ SqfreeBlockCount k n) : ¬Powerful (F k n)

Fully explicit squarefree-count obstruction.

theorem Erdos137.not_powerful_of_sqfree_term_large_prime {k n i p : ℕ} (hn : 1 ≤ n) (hi : i < k) (hsq : Squarefree (n + i)) (hp : Nat.Prime p) (hkp : k ≤ p) (hpdvd : p ∣ n + i) : ¬Powerful (F k n)

A squarefree term with a prime factor p ≥ k rules out powerfulness.

theorem Erdos137.not_powerful_of_exists_sqfree_term_large_prime {k n : ℕ} (hn : 1 ≤ n) (h : ∃ i < k, Squarefree (n + i) ∧ ∃ (p : ℕ), Nat.Prime p ∧ k ≤ p ∧ p ∣ n + i) : ¬Powerful (F k n)

Existential version.

Abstract squarefree-splice template

def Erdos137.SqfreeCapacityBeatenOnRange (Range : ℕ → ℕ → Prop) : Prop

A range predicate on which the squarefree count beats the deterministic capacity. This is the external interface for a squarefree-counting input (e.g. Pandey's): it is not proved here, only consumed. Mirrors the PrimeInBlockOnRange pattern of the abstract BHP splice.

Equations

• Erdos137.SqfreeCapacityBeatenOnRange Range = ∀ (k n : ℕ), 3 ≤ k → 1 ≤ n → Range k n → Erdos137.SmoothCapacity k < n ^ Erdos137.SqfreeBlockCount k n

theorem Erdos137.squarefree_range_not_powerful {Range : ℕ → ℕ → Prop} (hRange : SqfreeCapacityBeatenOnRange Range) {k n : ℕ} (hk : 3 ≤ k) (hn : 1 ≤ n) (hR : Range k n) : ¬Powerful (F k n)

Abstract squarefree splice. On any range where the squarefree count beats the capacity, no powerful block exists. The external squarefree-counting input enters only as the premise hRange; no analytic number theory is formalized here.