Track amplification for Erdős 624: a common hole for $2^s$ tracks gives $H(n+s)>m+s$

Proved

Erdos624.track_amplification

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

combinatoricserdos-problems

Let $H(n)$ be the least $m$ such that some $f:\mathcal P(X)\to X$ , $|X|=n$ , satisfies $\{f(A):A\subseteq Y\}=X$ for all $Y\subseteq X$ with $|Y|\ge m$ (Erdős Problem 624). Say $\mathrm{TrackBad}(n,m,s)$ holds if for every family of maps $g_B:\mathcal P(U)\to U$ ( $|U|=n$ ) indexed by the subsets $B$ of an $s$ -set $Z$ , there are $Y\subseteq U$ with $|Y|=m$ and $u\in U$ such that $u\notin\{g_B(A):A\subseteq Y\}$ for every $B$ . Theorem. If $n\ge1$ and $\mathrm{TrackBad}(n,m,s)$ , then

H(n+s)>m+s.

Given $f$ on $U\sqcup Z$ , set $g_B(A)=\pi(f(A\cup B))$ for a retraction $\pi$ onto $U$ ; a common hole $u$ is missed by $f$ on $Y\cup Z$ . This turns a multi-track deficiency statement into an additive gain in the threshold.

Formalization Note. $U=\mathrm{Fin}\,n$ , $Z=\mathrm{Fin}\,s$ , $U\sqcup Z=\mathrm{Fin}(n+s)$ . The hypothesis $n\ge1$ is necessary: for $n=0$ there are no maps into $U$ and TrackBad holds vacuously.

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem track_amplification {n m s : ℕ} (hn : 0 < n)
    (h : ∀ g : Finset (Fin s) → Finset (Fin n) → Fin n, ∃ Y : Finset (Fin n), #Y = m ∧
      ∃ u : Fin n, ∀ B : Finset (Fin s), ∀ A ∈ Y.powerset, g B A ≠ u) :
    m + s < H (n + s) := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Formal Conjectures 624.lean; Theorem B4 of GPT 6.1 Sol; lemma proposed by GPT 6.1 Sol (Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph

Track amplification for Erdős 624: a common hole for 2s2^s2s tracks gives H(n+s)>m+sH(n+s)>m+sH(n+s)>m+s

Track amplification for Erdős 624: a common hole for $2^s$ tracks gives $H(n+s)>m+s$