Rank construction: $r$ maps $\mathcal P(U)\to U$ jointly cover $U$ on every $k$ -set when $n\le r(k+1)$

Proved

Erdos624.rank_cover

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

combinatoricserdos-problems

Theorem. Let $|U|=n\ge1$ , $r,k\ge0$ with $n\le r(k+1)$ . Then there are maps $g_0,\dots,g_{r-1}:\mathcal P(U)\to U$ such that for every $k$ -set $Y\subseteq U$ ,

\bigcup_{i<r}\{g_i(A):A\subseteq Y\}=U.

The maps depend only on $|A|$ (each point of $U$ is assigned a slot $(i,\ell)$ and $g_i(A)$ is the point in slot $(i,|A|)$ ). In the context of Erdős Problem 624, this shows that a family of $r$ maps need have no common omitted point on any $k$ -set once $n\le r(k+1)$ , so any common-hole lemma for several maps needs $k$ large compared with $n/r$ .

Formalization Note. $U=\mathrm{Fin}\,n$ , maps indexed by $\mathrm{Fin}\,r$ .

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem rank_cover (r n k : ℕ) (hn : 0 < n) (h : n ≤ r * (k + 1)) :
    ∃ g : Fin r → Finset (Fin n) → Fin n,
      ∀ Y : Finset (Fin n), #Y = k → ∀ u : Fin n, ∃ i, ∃ A ⊆ Y, g i A = u := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); definitions from Formal Conjectures 624.lean; (B.6)/(B.L3) of claim from GPT 6.1 Sol (fourth answer, Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph

Rank construction: rrr maps P(U)→U\mathcal P(U)\to UP(U)→U jointly cover UUU on every kkk-set when n≤r(k+1)n\le r(k+1)n≤r(k+1)

Rank construction: $r$ maps $\mathcal P(U)\to U$ jointly cover $U$ on every $k$ -set when $n\le r(k+1)$