One commutative-aggregate map suffices: constant-surplus common holes against any second map (Erdős 624)

Proved

Erdos624.one_structured_map

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

combinatoricserdos-problems

Let $U$ be a finite set with $n=2^k$ elements. For a map $g:\mathcal P(U)\to U$ and $Y\subseteq U$ write $I_g(Y)=\{g(A):A\subseteq Y\}$ . For $B\subseteq U$ let $\mathcal K_B$ be the set of $k$ -subsets $Y\supseteq B$ .

Let $M$ be a finite commutative monoid, $v:U\to M$ and $\psi:M\to U$ arbitrary, and let $h(A)=\psi\bigl(\prod_{x\in A}v(x)\bigr)$ (a commutative-aggregate map). Write $b=2^{2t}$ .

Theorem. Let $k\ge3$ and $t,d\ge0$ with

|M|<\binom{n-2t(d-1)}{t},\qquad 2td\le k-2,\qquad 64(b-1)^d\le b^d.

Then there is a core $S\subseteq U$ with $|S|\le k-2$ (depending only on $v$ ) such that for every map $g:\mathcal P(U)\to U$ ,

n\,|\mathcal K_S|\;\le\;64\sum_{Y\in\mathcal K_S}\bigl(n-|I_h(Y)\cup I_g(Y)|\bigr).

So $h$ and an arbitrary second map miss, on average over the $k$ -sets through $S$ , at least $n/64$ common points. Context: Erdős Problem 624 asks whether $H(n)-\log_2 n\to\infty$ , where $H(n)$ is the least $m$ such that some $f:\mathcal P(X)\to X$ ( $|X|=n$ ) satisfies $f[\mathcal P(Y)]=X$ for all $|Y|\ge m$ . By an earlier track-amplification result it would suffice to show that, for large $k$ , any two maps $\mathcal P(U)\to U$ with $|U|=2^k$ have a common hole: a $k$ -set $Y$ and a point $u$ missed by both maps on $\mathcal P(Y)$ . This handles the case where one of the two maps is a commutative aggregate; the other map is unrestricted. These results do not settle Problem 624.

Formalization Note. Counting form with natural numbers (truncated subtraction is harmless since $|I_g(Y)|\le n$ ); $U$ is an arbitrary Fintype with Fintype.card U = 2 ^ k.

Preamble

import Mathlib
import Definitions.Def_Erdos624_defs
open Finset

Formal statement

namespace Erdos624

theorem one_structured_map {U : Type*} [Fintype U] [DecidableEq U] {M : Type*} [CommMonoid M] [Fintype M]
    (k t d : ℕ) (hk : 3 ≤ k) (hU : Fintype.card U = 2 ^ k) (v : U → M) (ψ : M → U)
    (h7 : Fintype.card M < (2 ^ k - 2 * t * (d - 1)).choose t)
    (hd : 2 * t * d ≤ k - 2) (hb : 64 * (2 ^ (2 * t) - 1) ^ d ≤ (2 ^ (2 * t)) ^ d) :
    ∃ S : Finset U, #S ≤ k - 2 ∧ ∀ g : Finset U → U,
      2 ^ k * #((powersetCard k (univ : Finset U)).filter (fun Y => S ⊆ Y)) ≤
        64 * ∑ Y ∈ (powersetCard k (univ : Finset U)).filter (fun Y => S ⊆ Y),
          (2 ^ k - #(Y.powerset.image (fun A => ψ (∏ x ∈ A, v x)) ∪ Y.powerset.image g)) := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); derived from GPT 6.1 Sol's analysis (sixth report, Oct 2026), relayed by Ethan Cheung; Lean-verified by Grok Bot for Ethan Cheung (Oct 24 2026)

View graph