Maps depending only on $|A|$ have small joint image (Erdős 624)

Proved

Erdos624.rank_only_bound

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

combinatoricserdos-problems

Theorem. Let $U$ be a set and $g_i(A)=h_i(|A|)$ for $i<r$ . For every finite $Y\subseteq U$ ,

\Bigl|\bigcup_{i<r}\{g_i(A):A\subseteq Y\}\Bigr|\le r\,(|Y|+1).

For $|U|=2^k$ , $|Y|=k$ , $r=2$ and $k\ge4$ this is $<2^k$ , so the rank construction that defeats the two-map common-hole claim at $k=3$ cannot work for larger $k$ .

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem rank_only_bound {U : Type*} [DecidableEq U] (r : ℕ) (h : Fin r → ℕ → U)
    (Y : Finset U) :
    #(((univ : Finset (Fin r)) ×ˢ Y.powerset).image (fun p => h p.1 (#p.2))) ≤ r * (#Y + 1) := by sorry

end Erdos624

Source

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

View graph

Maps depending only on ∣A∣|A|∣A∣ have small joint image (Erdős 624)

Maps depending only on $|A|$ have small joint image (Erdős 624)