Prove2Me

Arithmetic of the dense-extraction target: n≤b∣S∣n\le b|S|, ∣S∣4≤2104a28n3⇒n≤2104a28b4|S|^4\le2^{104}a^{28}n^3\Rightarrow n\le2^{104}a^{28}b^4 (Erdős 624)

Proved
Erdos624.dense_extraction_target_arith

by Ethan Cheung · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problems

Pure arithmetic. Let a,b,n,sa,b,n,s be natural numbers with n>0n>0. If n≤b sn\le b\,s and s4≤2104a28n3s^4\le 2^{104}a^{28}n^3, then n≤2104a28b4n\le 2^{104}a^{28}b^4.

In the cross-review this is the step showing that the (unproved) dense-pool short-circuit extraction target, combined with the packing theorem (P) ∣S∣4≤2104a28n3|S|^4\le2^{104}a^{28}n^3, would bound nn. Neither (P) nor the extraction target is claimed here; both enter only as hypotheses h1,h2h_1,h_2 about numbers.

Context: Erdős Problem 624 asks whether H(n)−log⁡2n→∞H(n)-\log_2 n\to\infty, where H(n)H(n) is the least mm such that some f:P(X)→Xf:\mathcal P(X)\to X with ∣X∣=n|X|=n satisfies f[P(Y)]=Xf[\mathcal P(Y)]=X for all ∣Y∣≥m|Y|\ge m. This is an auxiliary finite statement from Sol's Round 12 Step 17 cross-review / resilience analysis of the two-track (PAIR) case. It does not settle Erdős Problem 624, PAIR or Step 17.

Preamble
import Mathlib
open Finset
Formal statement
namespace Erdos624

theorem dense_extraction_target_arith (a b n s : ℕ) (hn : 0 < n) (h1 : n ≤ b * s)
    (h2 : s ^ 4 ≤ 2 ^ 104 * a ^ 28 * n ^ 3) : n ≤ 2 ^ 104 * a ^ 28 * b ^ 4 := by sorry

end Erdos624
Source
Erdős Problem 624 (https://www.erdosproblems.com/624); Round 12: Sol's 'Step 17: First-Round Cross-Review' and 'Step 17: resilient relations below the top layer'; derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung; hand-checked and Lean-verified by Grok Bot for Ethan Cheung (Oct 24 2026). Auxiliary result only; does NOT settle PAIR / Step 17 / #624.

View graph