Erdős Problem #137: a refined deterministic overlap bound

This file isolates a deterministic sharpening of the universal overlap bound Wg g k n ≤ k^k of BlockFramework. It contains no analytic number theory — no abc/Langevin constant, no Mertens estimate, no growing-g input. Everything below is a finite valuation computation checked on the standard Mathlib axioms (propext, Classical.choice, Quot.sound).

The refinement

Recall Wg g k n = ∏_{p ∈ (Bg g k n).primeFactors} p ^ (overlapg g k n p - 1), where overlapg g k n p counts the ⌊k/g⌋ blocks F g (n + g·j) that p divides. BlockFramework bounds the exponent two ways:

• overlapg_le: overlapg g k n p ≤ ⌊k/p⌋ + 1 (interval-count: p hits ≤ ⌊k/p⌋ + 1 of any k consecutive integers), giving Wg ∣ k! and Wg ≤ k^k.
• (new, easy) overlapg_le_numBlocks: overlapg g k n p ≤ ⌊k/g⌋ (there are only ⌊k/g⌋ blocks), reflecting that a prime hits at most ~k/g blocks.

Combining the two — the exponent overlapg - 1 is ≤ min(⌊k/p⌋, ⌊k/g⌋) — gives the refined capacity

WgRefinedCap g k = ∏_{p ≤ k} p ^ min(⌊k/p⌋, ⌊k/g⌋),

and Wg g k n ∣ WgRefinedCap g k (Wg_dvd_refinedCap), hence Wg g k n ≤ WgRefinedCap g k (Wg_le_refinedCap). This improves the exact overlap factor from k^k toward a finite product whose heuristic logarithm is k log(k/g) + O(k) (each prime contributes ≤ ⌊k/g⌋ instead of the generic ⌊k/p⌋, capping the small primes that dominate the k^k bound).

Modest scope — what is and is NOT claimed

This is a contained deterministic improvement of the overlap factor, NOT a new exponent claim. In particular:

• For fixed g it coincides in scale with the existing k^k/Mg/Mcrude bounds: the refined master inequalities below carry WgRefinedCap g k exactly where the old ones carried k^k, and for fixed g no asymptotic improvement to the per-k threshold follows.
• No uniform-in-g abc conclusion is claimed. The heuristic k log(k/g) (vs. k log k for k^k) is the only place the refinement could matter, and it would matter only for a growing-g strategy. Realizing that requires a uniform-in-g Langevin/abc constant A_g ≪ g² log g (discriminant scale) which is an open pen-and-paper problem, NOT formalized here. The heuristic logarithm and the A_g target are remarks only.

So WgRefinedCap is a strictly sharper deterministic cap on the overcount; whether it ever beats k^k usefully is gated entirely on the unformalized uniform-A_g input.

Note on the k + 1

WgRefinedCap ranges over Nat.primesBelow (k + 1), i.e. primes p ≤ k, rather than p < k. Including the single boundary prime p = k is a deliberate, harmless choice: it makes the divisibility Wg ∣ WgRefinedCap hold directly (the prime p = k, if it divides a block, satisfies overlapg - 1 ≤ ⌊k/k⌋ = 1), without a separate large-prime lemma. It does not change the heuristic logarithm k log(k/g) + O(k).

Main results (Mathlib's three axioms only)

• overlapg_le_numBlocks : overlapg g k n p ≤ ⌊k/g⌋.
• Wg_dvd_refinedCap : Wg g k n ∣ WgRefinedCap g k (the key valuation comparison).
• Wg_le_refinedCap : the size form Wg g k n ≤ WgRefinedCap g k.
• rad_blocksg_le_refined : the refined decomposition inequality ∏ rad ≤ rad(F k n)·WgRefinedCap.
• master_ineq_crude_g_refinedOverlap, master_ineq_g_refinedOverlap : the crude and smooth master inequalities of BlockFramework, restated with WgRefinedCap g k in place of k^k.

The number-of-blocks bound

theorem Erdos137.overlapg_le_numBlocks (g k n p : ℕ) : overlapg g k n p ≤ k / g

Number-of-blocks overlap bound. overlapg g k n p ≤ ⌊k/g⌋: the overlap is a sum of 0/1 indicators over the ⌊k/g⌋ blocks, so it is at most the number of blocks. This is the easy companion to overlapg_le (overlapg ≤ ⌊k/p⌋ + 1); their min powers the refined cap.

The refined capacity

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

The refined overlap capacity WgRefinedCap g k = ∏_{p ≤ k} p ^ min(⌊k/p⌋, ⌊k/g⌋).

The product ranges over Nat.primesBelow (k + 1), i.e. the primes p ≤ k; the exponent at p is min(⌊k/p⌋, ⌊k/g⌋), capping the generic Legendre exponent ⌊k/p⌋ by the number of blocks ⌊k/g⌋. Using k + 1 rather than k (so the boundary prime p = k is included) is a deliberate, harmless choice that makes Wg g k n ∣ WgRefinedCap g k hold without a separate large-prime lemma; the heuristic logarithm k log(k/g) + O(k) is unchanged by the single extra prime.

Equations

• Erdos137.WgRefinedCap g k = ∏ p ∈ (k + 1).primesBelow, p ^ min (k / p) (k / g)

theorem Erdos137.wgRefinedCap_pos (g k : ℕ) : 1 ≤ WgRefinedCap g k

1 ≤ WgRefinedCap g k (empty/prime-power factors are all ≥ 1). Mirrors smoothCapacity_pos.

theorem Erdos137.wgRefinedCap_ne_zero (g k : ℕ) : WgRefinedCap g k ≠ 0

theorem Erdos137.wgRefinedCap_factorization (g k p : ℕ) : (WgRefinedCap g k).factorization p = if p ∈ (k + 1).primesBelow then min (k / p) (k / g) else 0

Factorization of the refined capacity. For prime p ≤ k, v_p(WgRefinedCap g k) = min(⌊k/p⌋, ⌊k/g⌋); for p ∉ primesBelow (k+1), it is 0. Mirrors smoothCapacity_factorization.

The key divisibility

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

The overcount divides the refined capacity. Wg g k n ∣ WgRefinedCap g k. Pointwise on factorizations: at a prime p ≤ k, v_p(Wg) = overlapg - 1 ≤ min(⌊k/p⌋, ⌊k/g⌋) = v_p(cap) by overlapg_le (≤ ⌊k/p⌋ + 1) and overlapg_le_numBlocks (≤ ⌊k/g⌋); at any other prime, Wg's support (its prime factors) and the count overlapg ≤ ⌊k/p⌋ + 1 (which is 1 when p > k) force v_p(Wg) = 0. This refines Wg_dvd_factorial (Wg ∣ k!) by also capping each exponent at ⌊k/g⌋.

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

Size form of the refined overlap bound. Wg g k n ≤ WgRefinedCap g k, immediate from the divisibility Wg_dvd_refinedCap via Nat.le_of_dvd. The deterministic improvement of Wg ≤ k^k.

The refined decomposition inequality

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

Refined decomposition inequality. ∏_j rad (F g (n+g·j)) ≤ rad (F k n) · WgRefinedCap g k. The refined analogue of rad_blocksg_le: from the exact decomposition ∏ rad = rad(Bg)·Wg (rad_blocksg_decomp), rad(Bg) ∣ rad(F k n) (rad_Bg_dvd_rad_F), and Wg ≤ WgRefinedCap (Wg_le_refinedCap).

The refined master inequalities

These restate master_ineq_crude_g and master_ineq_g of BlockFramework with WgRefinedCap g k in place of the universal k^k factor. The proofs are the originals verbatim, substituting rad_blocksg_le_refined for rad_blocksg_le and (WgRefinedCap g k : ℝ) for (k : ℝ)^k.

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

Crude master inequality with the refined cap. Under BlockRadLBg g, for k ≥ g ≥ 3 and a powerful F k n with n ≥ 1:

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

The refined analogue of master_ineq_crude_g (whose RHS is k ^ (2 * g * k) = (k^{2k})^g). The chain Φ^{(g-1)/g} ≤ ∏rad ≤ rad·WgRefinedCap is squared with the crude rad² ≤ Φ, divided by Φ, combined with n^k ≤ Φ, and raised to the g-th power. The result is the exact refined-cap inequality n ^ ((g - 2) * k) ≤ WgRefinedCap g k ^ (2 * g) — note the k stays in the exponent here, since (unlike the old crude RHS (k^{2g})^k) the refined cap is not a perfect k-th power to divide out.

theorem Erdos137.master_ineq_g_refinedOverlap (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 ≤ ↑(WgRefinedCap g k) ^ (2 * g) * ↑(P k) ^ (2 * g)

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

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

The refined analogue of master_ineq_g (whose first RHS factor is (k^{2k})^g). The proof is the original, with rad_blocksg_le_refined/Wg_le_refinedCap and (WgRefinedCap g k : ℝ) in place of the k^k factor throughout the rpow chain.