Erdős Problem #137: the honest g = 5 per-k bound and the abstract splice machine

Erdos137/JointFiniteness.lean formalizes the radical-decomposition argument for triples (g = 3); Erdos137/SmoothRefinement.lean adds the smooth-part saving. This file develops the corresponding quintic (g = 5) block machinery and separates two logically distinct outputs.

Since the unification into Erdos137.BlockFramework, the g = 5 block objects (B5, overlap5, W5, Msplice) are the literal g = 5 instances of the generic framework, and the public combinatorial lemmas (B5_eq, B5_dvd_F, rad_5blocks_le, W5_dvd_factorial, W5_le_pow, master_ineq5, not_powerful_g5, powerful_bound_g5, g5_finiteness) are thin wrappers of their generic counterparts. The abstract splice machine (abstract_splice_no_counterexamples and friends) is unchanged.

What is formalized

• g5_finiteness / powerful_bound_g5 — per-k finiteness from one block input. From the single tail-absorbed hypothesis BlockRadLB5, for every fixed k ≥ 5 the set of n ≥ 1 with F k n powerful is finite; precisely, every such n satisfies n ≤ Msplice k = (k^{2k})^5 · P k^{10}. The proof is the formalized master inequality n^{3k} · L k^5 ≤ (k^{2k})^5 · P k^{10} (master_ineq5), using the quintic block radical input, the overlap bound W5 ≤ k^k, and the smooth-part refinement. The guard 5 ≤ k is essential: for k < 5 there are no quintic blocks (⌊k/5⌋ = 0). This is a per-k finiteness statement, NOT joint finiteness in (n, k).

• abstract_splice_no_counterexamples — an honest range-splice template. Parametric in two predicates Mid High : ℕ → ℕ → Prop. Given (i) CoversAll Mid High — every (k, n) with k ≥ 3, 1 ≤ n lies in n ≤ k, Mid k n, or High k n; (ii) PrimeInBlockOnRange Mid — a prime p > k that is a term of the block on the middle range; (iii) a high-range proof High k n → ¬ Powerful (F k n); it proves ¬ Powerful (F k n) for all such (k, n). The small range n ≤ k is discharged unconditionally by Bertrand via upper_half_prime_not_powerful.

The intended Pandey-free no-gap splice is an ASYMPTOTIC pen-and-paper reading of abstract_splice_no_counterexamples: take Mid = the Baker–Harman–Pintz range k < n ≤ k^{40/21−o(1)} (where BHP supplies a prime p > k in [n, n+k-1]) and High = the Mertens-sharpened quintic range n > k^{5/3+o(1)}. Since 5/3 < 40/21, these ranges overlap for all sufficiently large k, after the usual finite exceptional range (and k = 3, 4, handled by the triple route) is absorbed. Lean does NOT formalize Baker–Harman–Pintz, Mertens, or this asymptotic coverage; they enter only as the external premises of the abstract splice theorem, and a faithful instantiation would carry a finite-exception clause.

What is proved vs. hypothesized

• Proved (Mathlib's three axioms only): the g = 5 block product identities, the radical product decomposition, W5_le_pow (W5 ∣ k!, Legendre), master_ineq5, not_powerful_g5, powerful_bound_g5, g5_finiteness (all g = 5 instances of the generic framework), the unconditional small-n lemma upper_half_prime_not_powerful (Bertrand), prime_range_not_powerful, and abstract_splice_no_counterexamples.
• Hypotheses (analytic inputs, NOT formalized): BlockRadLB5 packages the abc/Langevin quintic block estimate, its constants, the epsilon loss, and the omitted tail into one explicit normalized hypothesis. PrimeInBlockOnRange, CoversAll, and the high-range proof are premises of the abstract splice (encoding BHP + Mertens + the exact exponents on the intended instantiation). All enter as premises, so they do NOT appear in the axiom footprint of any theorem. Unconditional Erdős #137 and abc remain open.

PART A — the g = 5 block objects as literal instances of the generic framework

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

The block product B5 k n = ∏_{j<⌊k/5⌋} F 5 (n+5j) = F (5⌊k/5⌋) n: the g = 5 instance of the generic Bg.

Equations

• Erdos137.B5 k n = Erdos137.Bg 5 k n

def Erdos137.overlap5 (k n p : ℕ) : ℕ

overlap5 p is the number of quintic blocks p divides: the g = 5 instance of overlapg.

Equations

• Erdos137.overlap5 k n p = Erdos137.overlapg 5 k n p

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

The over-count W5 k n: the g = 5 instance of the generic Wg.

Equations

• Erdos137.W5 k n = Erdos137.Wg 5 k n

theorem Erdos137.B5_eq (k n : ℕ) : B5 k n = F (5 * (k / 5)) n

B5 k n = F (5 * (k/5)) n. The g = 5 instance of Bg_eq.

theorem Erdos137.B5_dvd_F (k n : ℕ) : B5 k n ∣ F k n

B5 k n divides F k n (the g = 5 instance of Bg_dvd_F).

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

B5 k n ≠ 0 for n ≥ 1. The g = 5 instance of Bg_ne_zero.

theorem Erdos137.block5_ne_zero {n : ℕ} (hn : 1 ≤ n) (j : ℕ) : F 5 (n + 5 * j) ≠ 0

For n ≥ 1 each quintic block F 5 (n + 5j) is nonzero. The g = 5 instance of block_ne_zero.

theorem Erdos137.rad_blocks5_decomp {k n : ℕ} (hn : 1 ≤ n) : ∏ j ∈ Finset.range (k / 5), rad (F 5 (n + 5 * j)) = rad (B5 k n) * W5 k n

Radical-of-product decomposition (g = 5), exact form. ∏_j rad (F 5 (n+5j)) = rad (B5 k n) * W5 k n. The g = 5 instance of rad_blocksg_decomp.

theorem Erdos137.rad_B5_dvd_rad_F {k n : ℕ} (hn : 1 ≤ n) : rad (B5 k n) ∣ rad (F k n)

rad (B5 k n) ∣ rad (F k n). The g = 5 instance of rad_Bg_dvd_rad_F.

theorem Erdos137.rad_5blocks_le {k n : ℕ} (hn : 1 ≤ n) : ∏ j ∈ Finset.range (k / 5), rad (F 5 (n + 5 * j)) ≤ rad (F k n) * W5 k n

Decomposition inequality (the usable form, g = 5): ∏_j rad (F 5 (n+5j)) ≤ rad (F k n) * W5 k n. The g = 5 instance of rad_blocksg_le.

theorem Erdos137.overlap5_le {k n p : ℕ} (hn : 1 ≤ n) : overlap5 k n p ≤ k / p + 1

Overlap bound (combinatorial core, g = 5). overlap5 k n p ≤ ⌊k/p⌋ + 1 for n ≥ 1. The g = 5 instance of overlapg_le.

theorem Erdos137.W5_dvd_factorial {k n : ℕ} (hn : 1 ≤ n) : W5 k n ∣ k.factorial

Overlap product divides k! (g = 5). W5 k n ∣ k!. The g = 5 instance of Wg_dvd_factorial.

theorem Erdos137.W5_le_pow {k n : ℕ} (hn : 1 ≤ n) : W5 k n ≤ k ^ k

Overlap bound (g = 5): W5 k n ≤ k^k. The g = 5 instance of Wg_le_pow.

The genuine abc input (g = 5) and the master inequality

def Erdos137.BlockRadLB5 : Prop

Tail-absorbed quintic block radical input. This is a NORMALIZED asymptotic hypothesis, NOT the literal blockwise abc/Langevin statement: it packages the abc/Langevin constant, the epsilon loss, and the omitted k mod 5 tail into one explicit hypothesis. The guard 5 ≤ k is ESSENTIAL: for k < 5 there are no quintic blocks (⌊k/5⌋ = 0), the RHS is the empty product 1, and the bound (F k n)^{4/5} ≤ 1 would be false — i.e. the hypothesis would be inconsistent.

Equations

• Erdos137.BlockRadLB5 = ∀ (k n : ℕ), 5 ≤ k → 1 ≤ n → ↑(Erdos137.F k n) ^ (4 / 5) ≤ ↑(∏ j ∈ Finset.range (k / 5), Erdos137.rad (Erdos137.F 5 (n + 5 * j)))

theorem Erdos137.blockRadLB5_iff : BlockRadLB5 ↔ BlockRadLBg 5

BlockRadLB5 is exactly the g = 5 instance of the generic BlockRadLBg (the exponents 4/5 and (5-1)/5 agree, and the guard 5 ≤ k matches g ≤ k).

theorem Erdos137.master_ineq5 (hBlock5 : BlockRadLB5) {k n : ℕ} (hk : 5 ≤ k) (hn : 1 ≤ n) (hPow : Powerful (F k n)) : ↑n ^ (3 * k) * ↑(L k) ^ 5 ≤ (↑k ^ (2 * k)) ^ 5 * ↑(P k) ^ 10

Smooth-refined master inequality (g = 5). Under BlockRadLB5, for k ≥ 5 and a powerful F k n with n ≥ 1: n^{3k} · L k ^ 5 ≤ (k^{2k})^5 · P k ^ 10. The g = 5 instance of master_ineq_g ((5 - 2) * k = 3 * k, 2 * 5 = 10).

theorem Erdos137.not_powerful_g5 (hBlock5 : BlockRadLB5) {k n : ℕ} (hk : 5 ≤ k) (hn : 1 ≤ n) (hthr : (k ^ (2 * k)) ^ 5 * P k ^ 10 < n ^ (3 * k) * L k ^ 5) : ¬Powerful (F k n)

Headline (g = 5 threshold). Under BlockRadLB5 (the genuine abc input, the only hypothesis here), for k ≥ 5, if n exceeds the threshold (k^{2k})^5 · P^{10} < n^{3k} · L^5, then F k n is not powerful. The g = 5 ingredient 4/5 > 2/3 makes this n > k^{5/3 + o(1)}.

PART B — the small-n (Bertrand) input

theorem Erdos137.upper_half_prime_not_powerful {k n : ℕ} (hk : 2 ≤ k) (hn : 1 ≤ n) (hnk : n ≤ k) : ¬Powerful (F k n)

Small-n lemma (unconditional, via Bertrand). For 2 ≤ k, 1 ≤ n, and n ≤ k, the product F k n is not powerful.

Write N = n + k - 1 (the top of the block, the largest factor). Applying Mathlib's Bertrand postulate (Nat.exists_prime_lt_and_le_two_mul) at m = N / 2 (which is ≥ 1 since N ≥ 2) yields a prime p with N / 2 < p ≤ 2 ⌊N/2⌋ ≤ N. Hence:

• Upper / single-occurrence: 2p > 2 ⌊N/2⌋ ≥ N - 1, so 2p > N - 1, giving 2p > N (as 2p ≥ N/2·2 + 2 > N). Thus the only multiple of p in [1, N] that is itself a block factor is p (any other multiple is ≥ 2p > N), and p^2 ≥ (N/2+1)^2 > N too.
• Lower / membership: p > N / 2 = (n + k - 1) / 2 ≥ (n + n - 1) / 2 ≥ n - 1 (using n ≤ k), so p ≥ n; and p ≤ N = n + k - 1. Hence p = n + i₀ for some i₀ < k: p is a term.

Then v_p(F k n) = ∑_{i<k} v_p(n+i) = v_p(p) = 1 (every other factor < 2p is not a multiple of p), so p ∣ F but p^2 ∤ F, contradicting powerfulness. The single occurrence comes from 2p > N, not from p > k.

PART C — the honest g = 5 finiteness and the abstract splice machine

def Erdos137.Msplice (k : ℕ) : ℕ

The explicit g = 5 finiteness bound M k = (k^{2k})^5 · P k^{10}. The g = 5 instance of the generic Mg.

Equations

• Erdos137.Msplice k = Erdos137.Mg 5 k

theorem Erdos137.powerful_bound_g5 (hBlock5 : BlockRadLB5) {k n : ℕ} (hk : 5 ≤ k) (hn : 1 ≤ n) (hPow : Powerful (F k n)) : n ≤ Msplice k

Explicit bound form of the g = 5 deduction: a powerful F k n (with k ≥ 5, n ≥ 1) forces n ≤ Msplice k. The g = 5 instance of the generic powerful_bound_g.

theorem Erdos137.g5_finiteness (hBlock5 : BlockRadLB5) {k : ℕ} (hk : 5 ≤ k) : {n : ℕ | 1 ≤ n ∧ Powerful (F k n)}.Finite

Honest g = 5 finiteness (from BlockRadLB5 ALONE). For k ≥ 5, under the single analytic hypothesis BlockRadLB5, the set of n ≥ 1 with F k n powerful is finite: every such n satisfies the explicit bound n ≤ Msplice k = (k^{2k})^5 · P k^{10}. The g = 5 instance of the generic g_finiteness; involves no BHP, no Bertrand, and no Mertens — just BlockRadLB5.

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

Ranged prime-in-block input. PrimeInBlockOnRange Range says: on the range Range k n (with k ≥ 3, 1 ≤ n), the block [n, n+k-1] contains a prime p > k that is a term n + i of the block. This replaces the old too-strong global BHP: it only asks for a prime on whatever range Range it is instantiated at (e.g. the genuine Baker–Harman–Pintz range n ≤ k^{40/21}), never in "every" block. It enters as a hypothesis; Baker–Harman–Pintz is NOT formalized.

Equations

• Erdos137.PrimeInBlockOnRange Range = ∀ (k n : ℕ), 3 ≤ k → 1 ≤ n → Range k n → ∃ (p : ℕ), Nat.Prime p ∧ k < p ∧ ∃ i < k, n + i = p

theorem Erdos137.prime_range_not_powerful {Range : ℕ → ℕ → Prop} (hPrime : PrimeInBlockOnRange Range) {k n : ℕ} (hk : 3 ≤ k) (hn : 1 ≤ n) (hR : Range k n) : ¬Powerful (F k n)

Ranged prime deduction. Given a ranged prime input PrimeInBlockOnRange Range, for k ≥ 3, 1 ≤ n, and hR : Range k n, the product F k n is not powerful: the prime p > k supplied on the range is a term of the block, and prime_in_block_not_powerful (TaoPoint) rules out powerfulness.

def Erdos137.CoversAll (Mid High : ℕ → ℕ → Prop) : Prop

Coverage of the three ranges. CoversAll Mid High says every (k, n) with k ≥ 3, 1 ≤ n falls into the small range n ≤ k, the middle range Mid k n, or the high range High k n. On the intended instantiation, Mid = BHP range, High = Mertens-sharpened g = 5 range, and coverage is the inequality 5/3 < 40/21 (kept external).

Equations

• Erdos137.CoversAll Mid High = ∀ (k n : ℕ), 3 ≤ k → 1 ≤ n → n ≤ k ∨ Mid k n ∨ High k n

theorem Erdos137.abstract_splice_no_counterexamples {Mid High : ℕ → ℕ → Prop} (hCover : CoversAll Mid High) (hMid : PrimeInBlockOnRange Mid) (hHigh : ∀ (k n : ℕ), 3 ≤ k → 1 ≤ n → High k n → ¬Powerful (F k n)) {k n : ℕ} (hk : 3 ≤ k) (hn : 1 ≤ n) : ¬Powerful (F k n)

The abstract splice machine — the honest no-gap architecture. Parametric in two range predicates Mid High. Given:

• hCover : CoversAll Mid High — every (k, n) is small (n ≤ k), middle (Mid), or high (High);
• hMid : PrimeInBlockOnRange Mid — a prime p > k term of the block on the middle range;
• hHigh : ∀ k n, 3 ≤ k → 1 ≤ n → High k n → ¬ Powerful (F k n) — non-powerfulness on the high range;

then ¬ Powerful (F k n) for every (k, n) with k ≥ 3, 1 ≤ n. The small range is discharged unconditionally by upper_half_prime_not_powerful (Bertrand); the middle range by prime_range_not_powerful; the high range by the supplied hHigh. Baker–Harman–Pintz, Mertens, and the exact exponents live entirely inside the three premises — Lean never assumes them, so it never assumes "a prime in every block". For k ≥ 5, instantiating Mid = BHP range and High = Mertens-sharpened g = 5 range, with hHigh supplied by not_powerful_g5, gives the clean Pandey-free no-gap splice, whose analytic inputs remain external.