Erdős Problem #137: the parametric g-block framework (unifying g = 3 and g = 5)

Erdos137/JointFiniteness.lean develops the triple (g = 3) radical-decomposition route and Erdos137/SpliceFiniteness.lean the quintic (g = 5) route. Both are the same argument run with a different block length g. This file factors that duplication into ONE parametric g-block framework: every 3/5 in the two existing chains is replaced by a symbolic g, and the master inequality, per-k bound, and finiteness wrapper are proved once, for all g ≥ 3.

The unified master inequality

The headline is master_ineq_g: under the normalized block radical hypothesis BlockRadLBg g, for k ≥ g ≥ 3 and a powerful F k n (n ≥ 1),

n ^ ((g - 2) * k) · L k ^ g ≤ (k ^ (2k)) ^ g · P k ^ (2g).

This specializes EXACTLY to both recorded thresholds:

• g = 3 ⟹ n ^ k · L^3 ≤ (k^{2k})^3 · P^6 — the JointFiniteness/SmoothRefinement threshold (master_ineq, since (3 - 2) * k = k);
• g = 5 ⟹ n ^ {3k} · L^5 ≤ (k^{2k})^5 · P^{10} — the SpliceFiniteness threshold (master_ineq5, since (5 - 2) * k = 3k).

There are TWO exponent readings of master_ineq_g, and they must not be conflated. With only the proved lower bound L k ≥ 1, the master inequality gives the coarse threshold n > k^{2g/(g-2) + o(1)}; as g → ∞ this exponent tends to 2, i.e. toward k^{2 + ε} — NOT k^{1 + ε}. The k^{1 + ε} reading appears only after the unformalized Mertens lower bound log L k = k log k − O(k) (so L k = k^{k − o(k)}), which sharpens the threshold to n > k^{g/(g-2) + o(1)}; that exponent tends to 1. So fixed large g reaches the pen-and-paper k^{1 + ε} floor only in the Mertens-sharpened reading, never from the coarse formal bound alone. The formal .Finite wrapper deliberately uses the coarse explicit bound n ≤ Mg g k; the sharp exponent stays an external asymptotic reading of the master inequality. This is also NOT an unconditional improvement: for each FIXED g the abc/Langevin constant packaged in BlockRadLBg g depends on g (the implied constant degrades with the block length) — the known ceiling of the radical method, trading a sharper exponent for a worse constant, and the constant is exactly what abc would supply. So this is not a uniform growing-g theorem.

The two guards

• 3 ≤ g is needed for the exponent (g - 2) ≥ 1 (so n ≤ n^{(g-2)k}) and for the smooth/squaring arithmetic 2(g-1)/g - 1 = (g-2)/g ≥ 0.
• g ≤ k is a CONSISTENCY guard built into BlockRadLBg. For g > k there are no g-blocks (⌊k/g⌋ = 0), the block-radical product is the empty product 1, and the hypothesis (F k n)^{(g-1)/g} ≤ 1 would be inconsistent (it would force F k n ≤ 1).

What is proved vs. hypothesized

• Proved (Mathlib's three axioms only): the generic block product identity blocksg_prod_eq, the radical-of-product decomposition rad_blocksg_decomp, the overlap bound Wg_le_pow (Wg ∣ k!, Legendre), the smooth-refined master inequality master_ineq_g, the explicit per-k bound powerful_bound_g, and the finiteness wrapper g_finiteness.
• Hypothesis (analytic input, NOT formalized): BlockRadLBg g is the normalized tail-absorbed block radical lower bound — it packages the abc/Langevin constant, the epsilon loss, and the omitted k mod g tail into one explicit Prop. abc itself is NOT formalized; it enters only as a premise, so it does not appear in any axiom footprint.

The shared low-level helpers (rad_dvd_self, factorization_rad, rad_dvd_rad_of_dvd, Ioc_dvd_count, Ioc_dvd_le, div_le_factorization_factorial, pow_le_F, le_F, the smooth refinement smooth_refinement, P, L, …) are imported and reused verbatim from Erdos137.Base, not re-proved.

This framework sits ABOVE the concrete g = 3, 5 modules: JointFiniteness defines B/overlap/W literally as Bg 3/overlapg 3/Wg 3 and SpliceFiniteness defines B5/overlap5/W5 as the g = 5 instances, with their public lemmas re-derived as thin wrappers of the generic theorems below.

Two routes: SMOOTH vs. CRUDE

There are now TWO parametric routes off the same block chain, and they must not be conflated:

• SMOOTH (master_ineq_g, PART C): n ^ ((g-2) k) · L ^ g ≤ (k^{2k})^g · P ^ {2g}. This refines the bare powerful inequality rad ^ 2 ≤ F by the smooth gain L, so it carries a sharper exponent — threshold k ^ {2g/(g-2) + o(1)} (coarse L ≥ 1 reading) or k ^ {g/(g-2) + o(1)} (Mertens reading). But the sharpening is only realized through the unformalized Mertens lower bound on L; the formal .Finite wrapper falls back on the coarse explicit Mg.
• CRUDE (master_ineq_crude_g, PART E): n ^ (g - 2) ≤ k ^ (2 * g), a clean INTEGER inequality carrying NO L/P factor — it uses only rad ^ 2 ≤ F. The exponent is weaker but the threshold is the exact, fully explicit k ^ {2g/(g-2)} with no o(1) and no Mertens input: g = 3 → k^6, g = 4 → k^4 (since n^2 ≤ k^8 ↔ n ≤ k^4), g = 6 → k^3.

So: the crude route gives a fully explicit constant at a worse exponent; the smooth route gives a sharper exponent only via the unformalized Mertens reading. The crude g = 3 instance recovers the recorded not_powerful_of_large threshold n > k^6 exactly.

PART A — the generic g-block combinatorics (literal 3/5 → g)

def Erdos137.Bg (g k n : ℕ) : ℕ

The block product Bg g k n = ∏_{j<⌊k/g⌋} F g (n+g·j) = F (g⌊k/g⌋) n: the part of F k n covered by the g-blocks (dropping the k % g tail). Generic form of B/B5.

Equations

• Erdos137.Bg g k n = ∏ j ∈ Finset.range (k / g), Erdos137.F g (n + g * j)

def Erdos137.overlapg (g k n p : ℕ) : ℕ

overlapg g p = ∑_j [p ∈ (F g (n+g·j)).primeFactors] is the number of g-blocks p divides. Generic form of overlap/overlap5.

Equations

• Erdos137.overlapg g k n p = ∑ j ∈ Finset.range (k / g), if p ∈ (Erdos137.F g (n + g * j)).primeFactors then 1 else 0

def Erdos137.Wg (g k n : ℕ) : ℕ

The over-count Wg g k n := ∏_{p ∈ (Bg g k n).primeFactors} p ^ (overlapg p − 1). Generic form of W/W5.

Equations

• Erdos137.Wg g k n = ∏ p ∈ (Erdos137.Bg g k n).primeFactors, p ^ (Erdos137.overlapg g k n p - 1)

theorem Erdos137.blocksg_prod_eq {g : ℕ} (_hg : 1 ≤ g) (k n : ℕ) : ∏ j ∈ Finset.range (k / g), F g (n + g * j) = F (g * (k / g)) n

The product over the ⌊k/g⌋ blocks, ∏_{j<⌊k/g⌋} F g (n + g·j), equals F (g · ⌊k/g⌋) n. Generic form of triples_prod_eq/blocks5_prod_eq. The (hg : 1 ≤ g) guard makes the stride positive in the telescoping; it is not actually needed here (the induction is on k / g), but is recorded to match the parametric setting.

theorem Erdos137.Bg_eq {g : ℕ} (hg : 1 ≤ g) (k n : ℕ) : Bg g k n = F (g * (k / g)) n

Bg g k n = F (g * (k/g)) n.

theorem Erdos137.blocksg_prod_dvd {g : ℕ} (hg : 1 ≤ g) (k n : ℕ) : ∏ j ∈ Finset.range (k / g), F g (n + g * j) ∣ F k n

The product of the g-blocks divides F k n. Generic form of triples_prod_dvd.

theorem Erdos137.Bg_dvd_F {g : ℕ} (hg : 1 ≤ g) (k n : ℕ) : Bg g k n ∣ F k n

Bg g k n divides F k n (generic form of B_dvd_F/B5_dvd_F).

theorem Erdos137.Bg_ne_zero {g : ℕ} (hg : 1 ≤ g) {n : ℕ} (hn : 1 ≤ n) (k : ℕ) : Bg g k n ≠ 0

Bg g k n ≠ 0 for n ≥ 1.

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

For n ≥ 1 each block F g (n + g·j) is nonzero.

theorem Erdos137.factorization_blocksg_rad (g k n p : ℕ) (hn : 1 ≤ n) : (∏ j ∈ Finset.range (k / g), rad (F g (n + g * j))).factorization p = overlapg g k n p

The p-adic valuation of the product of the block radicals equals overlapg g k n p.

theorem Erdos137.factorization_rad_Bg {g : ℕ} (hg : 1 ≤ g) {k n : ℕ} (hn : 1 ≤ n) (p : ℕ) : (rad (Bg g k n)).factorization p = if p ∈ (Bg g k n).primeFactors then 1 else 0

The p-valuation of rad (Bg g k n) is 1 if p ∈ (Bg g k n).primeFactors, else 0.

theorem Erdos137.overlapg_pos_of_mem_primeFactors {g k n p : ℕ} (hn : 1 ≤ n) (hp : p ∈ (Bg g k n).primeFactors) : 1 ≤ overlapg g k n p

A prime in the support of Bg g k n divides some block, hence overlapg ≥ 1.

theorem Erdos137.mem_primeFactors_of_overlapg_pos {g k n p : ℕ} (hn : 1 ≤ n) (h : 1 ≤ overlapg g k n p) : p ∈ (Bg g k n).primeFactors

If overlapg g k n p ≥ 1 then p ∈ (Bg g k n).primeFactors.

theorem Erdos137.factorization_Wg {g k n : ℕ} (_hn : 1 ≤ n) (p : ℕ) : (Wg g k n).factorization p = if p ∈ (Bg g k n).primeFactors then overlapg g k n p - 1 else 0

The p-valuation of the over-count Wg g k n.

theorem Erdos137.rad_blocksg_decomp {g : ℕ} (hg : 1 ≤ g) {k n : ℕ} (hn : 1 ≤ n) : ∏ j ∈ Finset.range (k / g), rad (F g (n + g * j)) = rad (Bg g k n) * Wg g k n

Radical-of-product decomposition (generic g), exact form. ∏_j rad (F g (n+g·j)) = rad (Bg g k n) * Wg g k n. Generic form of rad_triples_decomp/rad_blocks5_decomp.

theorem Erdos137.rad_Bg_dvd_rad_F {g : ℕ} (hg : 1 ≤ g) {k n : ℕ} (hn : 1 ≤ n) : rad (Bg g k n) ∣ rad (F k n)

rad (Bg g k n) ∣ rad (F k n).

theorem Erdos137.rad_blocksg_le {g : ℕ} (hg : 1 ≤ g) {k n : ℕ} (hn : 1 ≤ n) : ∏ j ∈ Finset.range (k / g), rad (F g (n + g * j)) ≤ rad (F k n) * Wg g k n

Decomposition inequality (the usable form, generic g): ∏_j rad (F g (n+g·j)) ≤ rad (F k n) * Wg g k n (generic form of rad_triples_le/rad_5blocks_le).

The overlap bound Wg g k n ≤ k^k

def Erdos137.firstHit (g n p j : ℕ) : ℕ

The "first hit" map used to inject the counted g-blocks into the multiples of p in the spanning interval. firstHit g n p j is n + g·j + r₀, where r₀ < g is the least block offset with p ∣ (n + g·j + r₀) (defaulting to g - 1 if none — that branch is never taken for counted blocks). Replaces the hardcoded if … then … else … chains of overlap_le/overlap5_le by a uniform construction that works for any block length g.

Equations

• Erdos137.firstHit g n p j = n + g * j + Option.getD {r ∈ Finset.range g | p ∣ n + g * j + r}.min (g - 1)

theorem Erdos137.firstHit_mem_Icc (g n p j : ℕ) : firstHit g n p j ∈ Finset.Icc (n + g * j) (n + g * j + (g - 1))

firstHit g n p j lies in the block [n + g·j, n + g·j + (g-1)].

theorem Erdos137.overlapg_le {g : ℕ} (hg : 1 ≤ g) {k n p : ℕ} (hn : 1 ≤ n) : overlapg g k n p ≤ k / p + 1

Overlap bound (combinatorial core, generic g). overlapg g k n p ≤ ⌊k/p⌋ + 1 for n ≥ 1. The ⌊k/g⌋ blocks span ≤ k consecutive integers, and a prime p divides at most ⌊k/p⌋ + 1 of any ≤ k consecutive integers. Generic form of overlap_le/overlap5_le.

theorem Erdos137.Wg_dvd_factorial {g : ℕ} (hg : 1 ≤ g) {k n : ℕ} (hn : 1 ≤ n) : Wg g k n ∣ k.factorial

Overlap product divides k! (generic g). Wg g k n ∣ k!. Generic form of W_dvd_factorial/W5_dvd_factorial.

theorem Erdos137.Wg_le_pow {g : ℕ} (hg : 1 ≤ g) {k n : ℕ} (hn : 1 ≤ n) : Wg g k n ≤ k ^ k

Overlap bound (generic g): Wg g k n ≤ k^k. Since Wg ∣ k! (Legendre) and k! ≤ k^k. Generic form of W_le_pow/W5_le_pow.

PART B — the generic block radical hypothesis

def Erdos137.BlockRadLBg (g : ℕ) : Prop

Tail-absorbed g-block radical input. NORMALIZED hypothesis (not the literal blockwise abc/Langevin statement): packages the abc constant, epsilon loss, and omitted tail. The guard g ≤ k is essential — for g > k there are no g-blocks (⌊k/g⌋ = 0), the RHS is the empty product 1, and (F k n)^{(g-1)/g} ≤ 1 would be inconsistent.

Equations

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

PART C — the unified master inequality and finiteness

theorem Erdos137.master_ineq_g (g : ℕ) (hBlock : BlockRadLBg g) (hg : 3 ≤ g) {k n : ℕ} (hk : g ≤ k) (hn : 1 ≤ n) (hPow : Powerful (F k n)) : ↑n ^ ((g - 2) * k) * ↑(L k) ^ g ≤ (↑k ^ (2 * k)) ^ g * ↑(P k) ^ (2 * g)

Smooth-refined master inequality (generic g). Under BlockRadLBg g, for k ≥ g ≥ 3 and a powerful F k n with n ≥ 1:

n ^ ((g - 2) * k) · L k ^ g ≤ (k ^ (2k)) ^ g · P k ^ (2g).

This is master_ineq5's proof with the symbolic exponent g in place of 5, the block exponent (g-1)/g in place of 4/5, and the intermediate (g-2)/g in place of 3/5. Specializes to master_ineq (g = 3) and master_ineq5 (g = 5).

def Erdos137.Mg (g k : ℕ) : ℕ

The explicit generic g-block finiteness bound Mg g k = (k^{2k})^g · P k^{2g}. Generic form of Msplice.

Equations

• Erdos137.Mg g k = (k ^ (2 * k)) ^ g * Erdos137.P k ^ (2 * g)

theorem Erdos137.not_powerful_g (g : ℕ) (hBlock : BlockRadLBg g) (hg : 3 ≤ g) {k n : ℕ} (hk : g ≤ k) (hn : 1 ≤ n) (hthr : Mg g k < n ^ ((g - 2) * k) * L k ^ g) : ¬Powerful (F k n)

Exact generic threshold. Under BlockRadLBg g, if the exact master threshold is violated — Mg g k < n^{(g-2)k} · L k ^ g — then F k n is not powerful. This is the generic form of not_powerful_g5; it carries the sharp exponent (the L k ^ g factor) before any coarse L ≥ 1 collapse, and powerful_bound_g/g_finiteness are its corollaries.

theorem Erdos137.powerful_bound_g (g : ℕ) (hBlock : BlockRadLBg g) (hg : 3 ≤ g) {k n : ℕ} (hk : g ≤ k) (hn : 1 ≤ n) (hPow : Powerful (F k n)) : n ≤ Mg g k

Explicit per-k bound (generic g). A powerful F k n (with k ≥ g ≥ 3, n ≥ 1) forces n ≤ Mg g k. Generic form of powerful_bound_g5; the corollary of not_powerful_g after the coarse L ≥ 1 collapse and n ≤ n^{(g-2)k}.

theorem Erdos137.g_finiteness (g : ℕ) (hBlock : BlockRadLBg g) (hg : 3 ≤ g) {k : ℕ} (hk : g ≤ k) : {n : ℕ | 1 ≤ n ∧ Powerful (F k n)}.Finite

Generic g-block per-fixed-k finiteness (from BlockRadLBg g ALONE). For k ≥ g ≥ 3, under the single analytic hypothesis BlockRadLBg g, the set of n ≥ 1 with F k n powerful is finite: every such n satisfies n ≤ Mg g k. Generic form of g5_finiteness.

PART E — the crude (non-smooth) route

The crude route drops the smooth gain L/P entirely and uses only the bare powerful inequality rad (F k n) ^ 2 ≤ F k n (powerful_rad_sq_le). It yields a weaker exponent than the smooth route (master_ineq_g), but with a fully explicit constant and a clean INTEGER master inequality n ^ (g - 2) ≤ k ^ (2 * g) — the exact threshold k ^ (2 * g / (g - 2)) with no o(1) and no unformalized Mertens input:

• g = 3 ⟹ n ^ 1 ≤ k ^ 6 (threshold k ^ 6, matching not_powerful_of_large);
• g = 4 ⟹ n ^ 2 ≤ k ^ 8 ↔ n ≤ k ^ 4 (threshold k ^ 4);
• g = 6 ⟹ n ^ 4 ≤ k ^ {12} ↔ n ≤ k ^ 3 (threshold k ^ 3).

Contrast the SMOOTH master_ineq_g (n ^ ((g-2) k) · L ^ g ≤ …): that route carries the sharper exponent k ^ {2g/(g-2) + o(1)} (coarse reading) / k ^ {g/(g-2) + o(1)} (Mertens reading), but the sharpening is only available through the unformalized Mertens lower bound on L. The crude route below trades that sharper exponent for a fully explicit, formalized integer constant.

theorem Erdos137.master_ineq_crude_g (g : ℕ) (hBlock : BlockRadLBg g) (hg : 3 ≤ g) {k n : ℕ} (hk : g ≤ k) (hn : 1 ≤ n) (hPow : Powerful (F k n)) : n ^ (g - 2) ≤ k ^ (2 * g)

Crude master inequality (generic g, non-smooth). Under BlockRadLBg g, for k ≥ g ≥ 3 and a powerful F k n with n ≥ 1, the clean INTEGER inequality

n ^ (g - 2) ≤ k ^ (2 * g).

This is not_powerful_of_large's real chain (Φ^{(g-1)/g} ≤ rad · k^k, square using the crude rad ^ 2 ≤ Φ, divide by Φ, use n^k ≤ Φ) run with the symbolic exponents (g-1)/g, (g-2)/g, then raised to the g-th power and the common k-th power dropped via Nat.pow_le_pow_iff_left. Specializes to the g = 3 threshold n ≤ k^6 and the g = 4 threshold n^2 ≤ k^8 (n ≤ k^4).

def Erdos137.Mcrude (g k : ℕ) : ℕ

The right-hand side of the crude master inequality: Mcrude g k = k ^ (2 * g), so the exact threshold is Mcrude g k < n ^ (g - 2). For example g = 3 gives k^6 < n, while g = 4 gives k^8 < n^2, equivalently k^4 < n. (Note Mcrude g k is the bound on n^{g-2}, not on n itself unless g = 3.)

Equations

• Erdos137.Mcrude g k = k ^ (2 * g)

theorem Erdos137.not_powerful_crude_g (g : ℕ) (hBlock : BlockRadLBg g) (hg : 3 ≤ g) {k n : ℕ} (hk : g ≤ k) (hn : 1 ≤ n) (hthr : k ^ (2 * g) < n ^ (g - 2)) : ¬Powerful (F k n)

Crude per-k non-powerfulness (generic g). Under BlockRadLBg g, for k ≥ g ≥ 3, if the crude threshold is violated — k ^ (2 * g) < n ^ (g - 2) — then F k n is not powerful. Corollary of master_ineq_crude_g.

theorem Erdos137.powerful_bound_crude_g (g : ℕ) (hBlock : BlockRadLBg g) (hg : 3 ≤ g) {k n : ℕ} (hk : g ≤ k) (hn : 1 ≤ n) (hPow : Powerful (F k n)) : n ≤ k ^ (2 * g)

Explicit crude per-k bound (generic g). A powerful F k n (with k ≥ g ≥ 3, n ≥ 1) forces n ≤ k ^ (2 * g). From n ^ (g - 2) ≤ k ^ (2 * g) via g - 2 ≥ 1 and n ≤ n ^ (g - 2).

theorem Erdos137.crude_g_finiteness (g : ℕ) (hBlock : BlockRadLBg g) (hg : 3 ≤ g) {k : ℕ} (hk : g ≤ k) : {n : ℕ | 1 ≤ n ∧ Powerful (F k n)}.Finite

Crude per-fixed-k finiteness (generic g). For k ≥ g ≥ 3, under BlockRadLBg g ALONE, the set of n ≥ 1 with F k n powerful is finite: every such n satisfies n ≤ k ^ (2 * g). The crude analogue of g_finiteness, with a fully explicit threshold.