Erdős Problem #367 (k = 3 case), conditional on abc

We formalize:

1. rad(m) — the radical (squarefree kernel) of m
2. B₂(m) — the powerful (2-full) part of m
3. LEMMA STAR: rad(m)² · B₂(m) ≤ m²
4. Submultiplicativity of rad
5. The abc conjecture (as a hypothesis)
6. The main theorem: B₂(n) · B₂(n+1) · B₂(n+2) ≤ C'_ε · n^{2+ε}

Definitions

def Erdos367.Nat.rad (n : ℕ) : ℕ

The radical (squarefree kernel) of n: the product of distinct prime factors.

Equations

• Erdos367.Nat.rad n = n.primeFactors.prod id

def Erdos367.Nat.powerfulPart (n : ℕ) : ℕ

The powerful (2-full) part of n: ∏_{p : v_p(n) ≥ 2} p^{v_p(n)}.

Equations

• Erdos367.Nat.powerfulPart n = ∏ p ∈ n.primeFactors with 2 ≤ n.factorization p, p ^ n.factorization p

Basic properties of rad

@[simp]

theorem Erdos367.Nat.rad_zero : rad 0 = 1

@[simp]

theorem Erdos367.Nat.rad_one : rad 1 = 1

theorem Erdos367.Nat.rad_pos (n : ℕ) (_hn : 0 < n) : 0 < rad n

Basic properties of powerfulPart

@[simp]

theorem Erdos367.Nat.powerfulPart_zero : powerfulPart 0 = 1

@[simp]

theorem Erdos367.Nat.powerfulPart_one : powerfulPart 1 = 1

theorem Erdos367.Nat.powerfulPart_pos (n : ℕ) (_hn : 0 < n) : 0 < powerfulPart n

LEMMA STAR: rad(m)² · B₂(m) ≤ m²

The key integer-arithmetic lemma. For every m > 0, rad(m)² * powerfulPart(m) ≤ m².

Proof sketch: Write m = ∏ p^{a_p}. Then rad(m)² * B₂(m) = ∏{a_p=1} p² · ∏{a_p≥2} p^{2+a_p} m² = ∏ p^{2a_p} Compare primewise: for a_p = 1, 2 ≤ 2; for a_p ≥ 2, 2+a_p ≤ 2a_p.

theorem Erdos367.lemma_star (m : ℕ) (hm : 0 < m) : Nat.rad m ^ 2 * Nat.powerfulPart m ≤ m ^ 2

Submultiplicativity of rad

rad(a * b) ≤ rad(a) * rad(b) for positive a, b. This follows because primeFactors(ab) = primeFactors(a) ∪ primeFactors(b), and the product over a union is ≤ the product of products (intersection terms ≥ 1).

theorem Erdos367.Nat.rad_mul_le (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : rad (a * b) ≤ rad a * rad b

The abc conjecture (stated as a hypothesis)

def Erdos367.ABCConjecture : Prop

The abc conjecture: for every ε > 0, there exists C > 0 such that for all coprime positive integers a, b with a + b = c, we have c ≤ C · rad(abc)^{1+ε}.

Equations

• One or more equations did not get rendered due to their size.

Key identity and the abc application step

theorem Erdos367.squaring_trick (n : ℕ) : (n + 1) ^ 2 = n * (n + 2) + 1

(n+1)² = n(n+2) + 1, the "squaring trick" identity.

theorem Erdos367.rad_ignore_sq (n : ℕ) (hn : 0 < n) : Nat.rad (n * (n + 1) ^ 2 * (n + 2)) = Nat.rad (n * (n + 1) * (n + 2))

Main theorem: Erdős #367 (k=3), conditional on abc

Theorem. Assume abc. For every ε > 0, there exists C' > 0 such that for all n ≥ 1, B₂(n) · B₂(n+1) · B₂(n+2) ≤ C' · n^{2+ε}.

The proof proceeds in two stages: (1) Integer core: Use the squaring trick + abc to get (n+1)² ≤ C_ε · rad(n(n+1)(n+2))^{1+ε}, then apply rad submultiplicativity and LEMMA STAR to bound the radical in terms of n and the powerful parts. (2) Real-analytic rearrangement: Rearrange the resulting inequality using real-valued exponents to isolate B₂(n)B₂(n+1)B₂(n+2) ≤ C'·n^{2+ε}.

theorem Erdos367.integer_core_ineq (habc : ABCConjecture) (ε : ℝ) (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 0 < n → ↑(n + 1) ^ 2 ≤ C * (↑(Nat.rad n) * ↑(Nat.rad (n + 1)) * ↑(Nat.rad (n + 2))) ^ (1 + ε)

Helper: product of three LEMMA STAR instances (pure ℕ)

theorem Erdos367.triple_lemma_star (n : ℕ) (hn : 0 < n) : (Nat.rad n * Nat.rad (n + 1) * Nat.rad (n + 2)) ^ 2 * (Nat.powerfulPart n * Nat.powerfulPart (n + 1) * Nat.powerfulPart (n + 2)) ≤ (n * (n + 1) * (n + 2)) ^ 2

theorem Erdos367.real_analytic_rearrangement (habc : ABCConjecture) (ε : ℝ) (hε : 0 < ε) : ∃ (C' : ℝ), 0 < C' ∧ ∀ (n : ℕ), 0 < n → ↑(Nat.powerfulPart n * Nat.powerfulPart (n + 1) * Nat.powerfulPart (n + 2)) ≤ C' * ↑n ^ (2 + ε)

theorem Erdos367.erdos_367_k3 (habc : ABCConjecture) (ε : ℝ) (hε : 0 < ε) : ∃ (C' : ℝ), 0 < C' ∧ ∀ (n : ℕ), 0 < n → ↑(Nat.powerfulPart n * Nat.powerfulPart (n + 1) * Nat.powerfulPart (n + 2)) ≤ C' * ↑n ^ (2 + ε)

Main theorem (Erdős #367, k=3 case, conditional on abc). For every ε > 0, there exists C' > 0 such that for all n ≥ 1, B₂(n) · B₂(n+1) · B₂(n+2) ≤ C' · n^{2+ε}.