Conditioned Alon inequality on an arbitrary pool $V$ , $|V|\ge k+5$ , general colour set (Erdős 624)

Proved

Erdos624.conditioned_alon_pool

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

combinatoricserdos-problems

Let $k\ge2$ , $n=2^k$ , let $C$ be a finite set with $|C|=n$ , let $U$ be a finite set (of any size) and $f:\mathcal P(U)\to C$ arbitrary. Let $B,V\subseteq U$ with $|B|\le k-2$ and $|V|\ge k+5$ , and let $\mathcal K=\{Y\subseteq V: |Y|=k,\ B\subseteq Y\}$ . Then

32\sum_{Y\in\mathcal K}\bigl(n-|f[\mathcal P(Y)]|\bigr)\;\ge\; n\,|\mathcal K|.

(If $B\not\subseteq V$ both sides vanish.) The colour set keeps size $n=2^k$ although the pool $V$ may be much smaller than $n$ . This strengthens the previously verified Erdos624.conditioned_alon (which has colours $=$ inputs $=U$ , $|U|=2^k$ , pool $V=U$ , $k\ge3$ ).

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$ with $|X|=n$ satisfies $f[\mathcal P(Y)]=X$ for every $|Y|\ge m$ . This is an auxiliary finite inequality (the one-map 'robust Alon' loss bound and its ingredients) used in Sol's Round 10 analysis (parity-palette inequality, inequalities (11)/(13), top-layer-free resilience). It does not settle Erdős Problem 624, PAIR or Step 17.

Preamble

import Mathlib
open Finset

Formal statement

namespace Erdos624

theorem conditioned_alon_pool {U : Type*} [Fintype U] [DecidableEq U]
    {C : Type*} [Fintype C] [DecidableEq C] (k : ℕ) (hk : 2 ≤ k) (hC : Fintype.card C = 2 ^ k)
    (f : Finset U → C) (B V : Finset U) (hB : #B ≤ k - 2) (hV : k + 5 ≤ #V) :
    2 ^ k * #((powersetCard k V).filter (fun Y => B ⊆ Y)) ≤
      32 * ∑ Y ∈ (powersetCard k V).filter (fun Y => B ⊆ Y),
        (2 ^ k - #(Y.powerset.image f)) := by sorry

end Erdos624

Source

Erdős Problem 624 (https://www.erdosproblems.com/624); Round 10 consolidated report, section 'Proved: robust and conditioned Alon inequalities' (palette mechanism); derived from GPT 6.1 Sol's analysis, relayed by Ethan Cheung; proof reconstructed, 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

Conditioned Alon inequality on an arbitrary pool VVV, ∣V∣≥k+5|V|\ge k+5∣V∣≥k+5, general colour set (Erdős 624)

Conditioned Alon inequality on an arbitrary pool $V$ , $|V|\ge k+5$ , general colour set (Erdős 624)