Prove2Me

Robust Alon inequality with a separate colour set: 32∑YLf(Y)≥n(nk)32\sum_Y L_f(Y)\ge n\binom nk (Erdős 624)

Proved
Erdos624.robust_alon_colours

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

combinatoricserdos-problems

Let k≥3k\ge3, n=2kn=2^k, let UU and CC be finite sets with ∣U∣=∣C∣=n|U|=|C|=n and let f:P(U)→Cf:\mathcal P(U)\to C be arbitrary. Then

32∑Y∈(Uk)(n−∣f[P(Y)]∣)  ≥  n(nk).32\sum_{Y\in\binom Uk}\bigl(n-|f[\mathcal P(Y)]|\bigr)\;\ge\; n\binom nk.

This is the robust Alon inequality with input and colour sets separated (the previously verified Erdos624.robust_alon_sum is the case C=U=Fin 2kC=U=\mathrm{Fin}\,2^k). It is the special case B=∅B=\emptyset, V=UV=U of the conditioned pool inequality.

Context: Erdős Problem 624 asks whether H(n)−log⁡2n→∞H(n)-\log_2 n\to\infty, where H(n)H(n) is the least mm such that some f:P(X)→Xf:\mathcal P(X)\to X with ∣X∣=n|X|=n satisfies f[P(Y)]=Xf[\mathcal P(Y)]=X for every ∣Y∣≥m|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 robust_alon_colours {U : Type*} [Fintype U] [DecidableEq U]
    {C : Type*} [Fintype C] [DecidableEq C] (k : ℕ) (hk : 3 ≤ k)
    (hU : Fintype.card U = 2 ^ k) (hC : Fintype.card C = 2 ^ k) (f : Finset U → C) :
    2 ^ k * #(powersetCard k (univ : Finset U)) ≤
      32 * ∑ Y ∈ powersetCard k (univ : Finset U), (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