Erdős Problem #367: Consecutive Powerful Parts

We prove that limsup_{n→∞} B₂(n)·B₂(n+1)·B₂(n+2) / (n²·log n) = ∞, where B₂(m) = ∏_{p^e ∥ m, e≥2} p^e is the powerful (2-full) part of m.

Equivalently (the cofinal form, which is what makes it a limsup rather than a mere sup): ∀ M : ℝ, ∀ N : ℕ, ∃ n ≥ N, B₂(n) * B₂(n+1) * B₂(n+2) > M * n² * log n, i.e. the ratio exceeds every M for arbitrarily large n.

Strategy

We use the Pell equation x² - 8y² = 1 (fundamental solution (3,1)) to produce triples (n, n+1, n+2) where n = 8y² is powerful, n+1 = x² is powerful, and n+2 = x²+1 has a large powerful part thanks to the algebraic structure of ℤ[√2].

What is proved

All lemmas and theorems are fully proved with no sorry statements. #print axioms erdos367 shows only the three standard axioms: propext, Classical.choice, Quot.sound.

Powerful part

def Erdos367.powerfulPart (m : ℕ) : ℕ

The powerful (2-full) part of m: ∏_{p^e ∥ m, e ≥ 2} p^e.

Equations

• Erdos367.powerfulPart m = m.factorization.prod fun (p e : ℕ) => if e ≥ 2 then p ^ e else 1

def Erdos367.IsPowerful (m : ℕ) : Prop

A number is powerful if every prime factor has exponent ≥ 2.

Equations

• Erdos367.IsPowerful m = ∀ (p : ℕ), Nat.Prime p → p ∣ m → 2 ≤ m.factorization p

theorem Erdos367.powerfulPart_of_powerful {m : ℕ} (hm : m ≠ 0) (h : IsPowerful m) : powerfulPart m = m

theorem Erdos367.isPowerful_sq {k : ℕ} (hk : k ≠ 0) : IsPowerful (k ^ 2)

theorem Erdos367.powerfulPart_sq {k : ℕ} (hk : k ≠ 0) : powerfulPart (k ^ 2) = k ^ 2

theorem Erdos367.isPowerful_eight_mul_sq {y : ℕ} (hy : y ≠ 0) : IsPowerful (8 * y ^ 2)

theorem Erdos367.powerfulPart_eight_mul_sq {y : ℕ} (hy : y ≠ 0) : powerfulPart (8 * y ^ 2) = 8 * y ^ 2

theorem Erdos367.powerfulPart_ge_of_prime_sq_dvd {m p : ℕ} (hm : m ≠ 0) (hp : Nat.Prime p) (hd : p ^ 2 ∣ m) : p ^ 2 ∣ powerfulPart m

Pell sequence for x² - 8y² = 1

def Erdos367.pellXY : ℕ → ℤ × ℤ

Joint recurrence for Pell solutions (X_j, Y_j) with X_j² - 8·Y_j² = 1.

Equations

• Erdos367.pellXY 0 = (1, 0)
• Erdos367.pellXY j.succ = match Erdos367.pellXY j with | (x, y) => (3 * x + 8 * y, x + 3 * y)

def Erdos367.pellX (j : ℕ) : ℤ

X component of Pell solutions for x² - 8y² = 1.

Equations

• Erdos367.pellX j = (Erdos367.pellXY j).1

def Erdos367.pellY (j : ℕ) : ℤ

Y component of Pell solutions for x² - 8y² = 1.

Equations

• Erdos367.pellY j = (Erdos367.pellXY j).2

@[simp]

theorem Erdos367.pellX_zero : pellX 0 = 1

@[simp]

theorem Erdos367.pellY_zero : pellY 0 = 0

@[simp]

theorem Erdos367.pellX_succ (j : ℕ) : pellX (j + 1) = 3 * pellX j + 8 * pellY j

@[simp]

theorem Erdos367.pellY_succ (j : ℕ) : pellY (j + 1) = pellX j + 3 * pellY j

theorem Erdos367.pellX_pos (j : ℕ) : 0 < pellX j

theorem Erdos367.pellY_nonneg (j : ℕ) : 0 ≤ pellY j

theorem Erdos367.pellY_pos {j : ℕ} (hj : 0 < j) : 0 < pellY j

theorem Erdos367.pell_identity (j : ℕ) : pellX j ^ 2 - 8 * pellY j ^ 2 = 1

Pell identity. X_j² - 8·Y_j² = 1.

theorem Erdos367.pellY_le_pellX (j : ℕ) : pellY j ≤ pellX j

pellY j ≤ pellX j for all j.

theorem Erdos367.pellY_ge_self (j : ℕ) : ↑j ≤ pellY j

Lower bound: j ≤ Y_j. The Pell Y-sequence grows at least linearly, so the witness index j can be pushed arbitrarily large.

theorem Erdos367.pellX_le_pow (j : ℕ) : pellX j ≤ 11 ^ j

Upper bound: pellX j ≤ 11 ^ j.

The triple (n_j, n_j + 1, n_j + 2)

def Erdos367.pellN (j : ℕ) : ℕ

n_j = 8 · Y_j², a powerful number for j ≥ 1.

Equations

• Erdos367.pellN j = (8 * Erdos367.pellY j ^ 2).toNat

theorem Erdos367.pellN_eq (j : ℕ) : ↑(pellN j) = 8 * pellY j ^ 2

theorem Erdos367.pellN_pos {j : ℕ} (hj : 0 < j) : 0 < pellN j

theorem Erdos367.pellN_ge_self (j : ℕ) : j ≤ pellN j

Lower bound: j ≤ n_j. Since n_j = 8·Y_j² and j ≤ Y_j, the witness n_j grows at least linearly, so it exceeds any prescribed threshold.

theorem Erdos367.L0 (j : ℕ) : pellN j + 1 = (pellX j).toNat ^ 2

L0. n_j + 1 = X_j² (as natural numbers).

theorem Erdos367.L1 {j : ℕ} (hj : 0 < j) : powerfulPart (pellN j) = pellN j

L1. B₂(n_j) = n_j for j ≥ 1: n_j = 8·Y_j² is powerful.

theorem Erdos367.L2 (j : ℕ) : powerfulPart (pellN j + 1) = pellN j + 1

L2. B₂(n_j + 1) = n_j + 1: n_j + 1 = X_j² is a perfect square.

theorem Erdos367.L3 (j : ℕ) : pellN j + 2 = (pellX j).toNat ^ 2 + 1

L3. n_j + 2 = X_j² + 1.

theorem Erdos367.product_lower_bound {j : ℕ} (hj : 0 < j) : powerfulPart (pellN j) * powerfulPart (pellN j + 1) * powerfulPart (pellN j + 2) = pellN j * (pellN j + 1) * powerfulPart (pellN j + 2)

For j ≥ 1, the triple product simplifies using L1 and L2.

The algebraic BOOST

For a prime p ≡ 5 mod 8, the fundamental unit α = 3 + √8 of ℤ[√8] satisfies α^{(p+1)/2·p} ≡ -1 mod p² in ℤ[√8]. In concrete terms: with L = (p+1)/2 · p, pellX L ≡ -1 (mod p²) and pellY L ≡ 0 (mod p²).

Proof sketch: Since p ≡ 5 mod 8, (2/p) = -1 (Legendre symbol), so p is inert in ℤ[√2]. The Frobenius on ℤ[√2]/p ≅ 𝔽_{p²} sends √2 ↦ -√2, giving (1+√2)^p ≡ 1-√2 = -(1+√2)^{-1} (mod p), hence α^{(p+1)/2} ≡ -1 (mod p). Hensel lifting (via the structure of (ℤ[√2]/p^a)×) gives α^{(p+1)/2·p} ≡ -1 (mod p²).

theorem Erdos367.alpha_pow (j : ℕ) : { re := 3, im := 2 } ^ j = { re := pellX j, im := 2 * pellY j }

theorem Erdos367.eps_sq : { re := 1, im := 1 } ^ 2 = { re := 3, im := 2 }

theorem Erdos367.sqrtd_pow_odd (k : ℕ) : Zsqrtd.sqrtd ^ (2 * k + 1) = { re := 0, im := 2 ^ k }

theorem Erdos367.euler_two_mod (p : ℕ) (hp : Nat.Prime p) (hp5 : p % 8 = 5) : ↑p ∣ 2 ^ (p / 2) + 1

theorem Erdos367.frobenius_eps (p : ℕ) (hp : Nat.Prime p) (hp5 : p % 8 = 5) : ↑p ∣ ({ re := 1, im := 1 } ^ p).re - 1 ∧ ↑p ∣ ({ re := 1, im := 1 } ^ p).im + 1

theorem Erdos367.eps_succ_mod (p : ℕ) (hp : Nat.Prime p) (hp5 : p % 8 = 5) : ↑p ∣ ({ re := 1, im := 1 } ^ (p + 1)).re + 1 ∧ ↑p ∣ ({ re := 1, im := 1 } ^ (p + 1)).im

theorem Erdos367.hensel_lift (p : ℕ) (hp : Nat.Prime p) (hp2 : p ≠ 2) (z : ℤ√2) (hre : ↑p ∣ z.re + 1) (him : ↑p ∣ z.im) : ↑p ^ 2 ∣ (z ^ p).re + 1 ∧ ↑p ^ 2 ∣ (z ^ p).im

theorem Erdos367.pell_boost (p : ℕ) (hp : Nat.Prime p) (hp5 : p % 8 = 5) : have L := (p + 1) / 2 * p; ↑p ^ 2 ∣ pellX L + 1 ∧ ↑p ^ 2 ∣ pellY L

From BOOST to divisibility of n_j + 2

theorem Erdos367.pell_sq_plus_one_div (L : ℕ) (m : ℤ) (_hm : 0 < m) (hx : m ∣ pellX L + 1) (hy : m ∣ pellY L) (hL_odd : L % 2 = 1) : m ∣ 4 * (pellX ((L + 1) / 2) ^ 2 + 1)

If pellX L ≡ -1 (mod m) and pellY L ≡ 0 (mod m) with L odd, then m ∣ 4·((pellX ((L+1)/2))² + 1). This uses the doubling formula for Pell sequences.

theorem Erdos367.prime_sq_dvd_pellN_plus2 (p : ℕ) (hp : Nat.Prime p) (hp5 : p % 8 = 5) : have L := (p + 1) / 2 * p; have j := (L + 1) / 2; ↑p ^ 2 ∣ ↑(pellN j) + 2

Key lemma and main theorem

Assembly + Divergence (combined in erdos367_key)

Given a finite set S of primes ≡ 5 mod 8, form L = lcm_{p∈S}((p+1)/2 · p) (odd), set j = (L+1)/2. By a generalized BOOST (extending pell_boost to odd multiples via α^{kL₀} = (α^{L₀})^k ≡ (-1)^k), p² ∣ n_j + 2 for each p ∈ S. Since the p² are coprime, B₂(n_j+2) ≥ ∏_{p∈S} p².

The ratio ∏ p² / log(n_j) grows as (1/log α) · ∏ 2p/(p+1) → ∞, since each factor 2p/(p+1) > 1 and there are infinitely many such primes (Dirichlet: Nat.setOf_prime_and_eq_mod_infinite in Mathlib).

Helper lemmas for erdos367_key

theorem Erdos367.zsqrt2_pow_cong_one (m : ℤ) (z : ℤ√2) (k : ℕ) (hre : m ∣ z.re - 1) (him : m ∣ z.im) : m ∣ (z ^ k).re - 1 ∧ m ∣ (z ^ k).im

theorem Erdos367.zsqrt2_odd_pow_neg_one (m : ℤ) (z : ℤ√2) (t : ℕ) (hre : m ∣ z.re + 1) (him : m ∣ z.im) (ht : t % 2 = 1) : m ∣ (z ^ t).re + 1 ∧ m ∣ (z ^ t).im

theorem Erdos367.generalized_boost_pellN (p : ℕ) (hp : Nat.Prime p) (hp5 : p % 8 = 5) (L : ℕ) (hL_dvd : (p + 1) / 2 * p ∣ L) (hL_odd : L % 2 = 1) : p ^ 2 ∣ pellN ((L + 1) / 2) + 2

theorem Erdos367.infinite_primes_5_mod_8 : {p : ℕ | Nat.Prime p ∧ p % 8 = 5}.Infinite

Infinitely many primes are ≡ 5 mod 8.

theorem Erdos367.exists_finset_of_infinite {α : Type u_1} {S : Set α} (hS : S.Infinite) (n : ℕ) : ∃ (T : Finset α), n ≤ T.card ∧ ∀ x ∈ T, x ∈ S

theorem Erdos367.finset_coprime_sq_dvd (S : Finset ℕ) (m : ℕ) (hS : ∀ p ∈ S, Nat.Prime p) (hdvd : ∀ p ∈ S, p ^ 2 ∣ m) : ∏ p ∈ S, p ^ 2 ∣ m

theorem Erdos367.pellN_lt_eleven_pow (j : ℕ) (_hj : 0 < j) : pellN j < 11 ^ (2 * j)

theorem Erdos367.prod_Mp_odd (S : Finset ℕ) (hS : ∀ p ∈ S, p % 8 = 5) : (∏ p ∈ S, (p + 1) / 2 * p) % 2 = 1

theorem Erdos367.prod_Mp_pos (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p ∧ p % 8 = 5) (_hne : S.Nonempty) : 0 < ∏ p ∈ S, (p + 1) / 2 * p

theorem Erdos367.ratio_bound_per_prime (p : ℕ) (hp : 5 ≤ p) (_hp_odd : p % 2 = 1) : 5 * ((p + 1) / 2 * p) ≤ 3 * p ^ 2

theorem Erdos367.prod_ratio_bound_nat (S : Finset ℕ) (hS : ∀ p ∈ S, 5 ≤ p ∧ p % 2 = 1) : 5 ^ S.card * ∏ p ∈ S, (p + 1) / 2 * p ≤ 3 ^ S.card * ∏ p ∈ S, p ^ 2

theorem Erdos367.erdos367_key (j₀ : ℕ) (N : ℝ) : ∃ (j : ℕ), j₀ ≤ j ∧ 0 < j ∧ ↑(powerfulPart (pellN j + 2)) > N * Real.log ↑(pellN j)

theorem Erdos367.erdos367 (M : ℝ) (N : ℕ) : ∃ (n : ℕ), N ≤ n ∧ ↑(powerfulPart n) * ↑(powerfulPart (n + 1)) * ↑(powerfulPart (n + 2)) > M * ↑n ^ 2 * Real.log ↑n

Main theorem (Erdős #367). For every M : ℝ and every threshold N : ℕ, there exists n ≥ N such that B₂(n) · B₂(n+1) · B₂(n+2) > M · n² · log(n).

Because the bound holds for arbitrarily large n, this is the genuine limsup_{n→∞} B₂(n)·B₂(n+1)·B₂(n+2) / (n²·log n) = ∞, not merely a supremum: the ratio exceeds every M cofinally often.