The r = 3 case of the "13/9 theorem" (Erdős #367 r-full extension)

This file formalizes an unconditional, elementary lower-bound construction (the r = 3 case of a new lower bound for the r-full extension of Erdős problem #367).

rFullPart r m is the "r-full part" of m: the product of the prime powers p ^ v occurring in the factorization of m for which r ≤ v_p(m). We write B₃ m := rFullPart 3 m.

The construction fixes a prime s ≠ 3, a "seed" t₀ with 1 ≤ t₀ ≤ s^3 such that s^3 ∣ g t₀, and sets t := t₀ + s^3, n := (t^3 - 1)^3. The three main results are:

• T1 : B₃ n = n;
• T2 : t^3 * s^3 ∣ B₃ (n+1);
• T3 : 512 * (B₃ n * B₃ (n+1))^9 > n^13, the integer form of B₃ n · B₃ (n+1) > n^{13/9}/2.

The "prime supply" (the existence of infinitely many suitable pairs (s, t₀)) is kept as a hypothesis and is not part of this development.

def Core139.rFullPart (r m : ℕ) : ℕ

The r-full part of m: the product of prime powers p ^ v_p(m) with r ≤ v_p(m).

Equations

• Core139.rFullPart r m = (Finsupp.filter (fun (p : ℕ) => r ≤ m.factorization p) m.factorization).prod fun (p v : ℕ) => p ^ v

def Core139.g (t : ℕ) : ℕ

The auxiliary polynomial g t = t^6 - 3 t^3 + 3 (with natural-number subtraction).

Equations

• Core139.g t = t ^ 6 - 3 * t ^ 3 + 3

Generic facts about rFullPart

theorem Core139.rFullPart_pos (r M : ℕ) : 1 ≤ rFullPart r M

rFullPart is always positive (it is a product of prime powers, each ≥ 1).

theorem Core139.rFullPart_pow (r m : ℕ) (hm : 1 ≤ m) : rFullPart r (m ^ r) = m ^ r

For m ≥ 1, the r-full part of m ^ r is m ^ r itself: every prime dividing m ^ r has multiplicity r * v_p(m) ≥ r, so the filter keeps the entire factorization.

theorem Core139.factorization_rFullPart (r M : ℕ) : (rFullPart r M).factorization = Finsupp.filter (fun (p : ℕ) => r ≤ M.factorization p) M.factorization

The factorization of rFullPart r M is the filtered factorization.

theorem Core139.pow_dvd_rFullPart (r d M : ℕ) (hd : 1 ≤ d) (hM : M ≠ 0) (h : d ^ r ∣ M) : d ^ r ∣ rFullPart r M

If d ≥ 1 and d ^ r ∣ M then d ^ r ∣ rFullPart r M: each prime p ∣ d has v_p(M) ≥ r * v_p(d) ≥ r, so it survives the filter and v_p(rFullPart r M) = v_p(M).

Arithmetic facts about g

theorem Core139.g_add (t : ℕ) (ht : 2 ≤ t) : g t + 3 * t ^ 3 = t ^ 6 + 3

For t ≥ 2, the natural subtraction in g is exact: g t + 3 t^3 = t^6 + 3.

theorem Core139.g_cast {R : Type u_1} [CommRing R] (t : ℕ) (ht : 2 ≤ t) : ↑(g t) = ↑t ^ 6 - 3 * ↑t ^ 3 + 3

Casting g to any commutative ring (for t ≥ 2): (g t : R) = t^6 - 3 t^3 + 3.

The construction

def Core139.tval (s t₀ : ℕ) : ℕ

The shifted seed t = t₀ + s^3.

Equations

• Core139.tval s t₀ = t₀ + s ^ 3

def Core139.nval (s t₀ : ℕ) : ℕ

The constructed integer n = (t^3 - 1)^3.

Equations

• Core139.nval s t₀ = (Core139.tval s t₀ ^ 3 - 1) ^ 3

theorem Core139.tval_ge (s t₀ : ℕ) (hs : Nat.Prime s) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ s ^ 3) : 9 ≤ tval s t₀

Basic bound: t = t₀ + s^3 ≥ 9 (since s ≥ 2 so s^3 ≥ 8, and t₀ ≥ 1).

theorem Core139.key_identity (s t₀ : ℕ) (hs : Nat.Prime s) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ s ^ 3) : nval s t₀ + 1 = tval s t₀ ^ 3 * g (tval s t₀)

Key identity: n + 1 = t^3 * g t, i.e. (t^3 - 1)^3 + 1 = t^3 (t^6 - 3 t^3 + 3).

theorem Core139.s3_dvd_g_t (s t₀ : ℕ) (hs : Nat.Prime s) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ s ^ 3) (hroot : s ^ 3 ∣ g t₀) : s ^ 3 ∣ g (tval s t₀)

Congruence step: s^3 ∣ g t. Since t ≡ t₀ (mod s^3) and g is a polynomial, g t ≡ g t₀ ≡ 0 (mod s^3).

theorem Core139.s_not_dvd_t (s t₀ : ℕ) (hs : Nat.Prime s) (hs3 : s ≠ 3) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ s ^ 3) (hroot : s ^ 3 ∣ g t₀) : ¬s ∣ tval s t₀

s does not divide t: otherwise s ∣ g t together with s ∣ t^6, s ∣ 3 t^3 would force s ∣ 3, hence s = 3, contradicting hs3.

The three theorems

theorem Core139.T1 (s t₀ : ℕ) (hs : Nat.Prime s) (_hs3 : s ≠ 3) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ s ^ 3) (_hroot : s ^ 3 ∣ g t₀) : rFullPart 3 (nval s t₀) = nval s t₀

(T1) The 3-full part of n is n. Since n = (t^3-1)^3 is a perfect cube with t^3 - 1 ≥ 1, this is rFullPart_pow.

(The hypotheses hs3 and hroot are part of the construction's hypothesis structure but turn out to be unnecessary for this particular statement.)

theorem Core139.T2 (s t₀ : ℕ) (hs : Nat.Prime s) (hs3 : s ≠ 3) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ s ^ 3) (hroot : s ^ 3 ∣ g t₀) : tval s t₀ ^ 3 * s ^ 3 ∣ rFullPart 3 (nval s t₀ + 1)

(T2) t^3 * s^3 divides the 3-full part of n + 1. Both t^3 and s^3 divide n+1 (via n+1 = t^3 g t and s^3 ∣ g t), each survives into B₃ by pow_dvd_rFullPart, and they are coprime since s ∤ t.

theorem Core139.T3 (s t₀ : ℕ) (hs : Nat.Prime s) (hs3 : s ≠ 3) (ht₀ : 1 ≤ t₀ ∧ t₀ ≤ s ^ 3) (hroot : s ^ 3 ∣ g t₀) : 512 * (rFullPart 3 (nval s t₀) * rFullPart 3 (nval s t₀ + 1)) ^ 9 > nval s t₀ ^ 13

(T3) The integer form of B₃(n) B₃(n+1) > n^{13/9} / 2: 512 * (B₃ n * B₃ (n+1))^9 > n^13.

Proof chain: B₃ n = n and t^3 s^3 ≤ B₃ (n+1), with t ≤ 2 s^3 giving 2 (B₃ n · B₃ (n+1)) ≥ n t^4; raising to the 9-th power and using t^9 > n (so t^36 > n^4) yields 512 (B₃ n · B₃ (n+1))^9 ≥ n^9 t^36 > n^13.