Prove2Me

Alon per-core average: 32∑a≠b∈RLf(W∪{a,b})≥n ∣R∣(∣R∣−1)32\sum_{a\ne b\in R}L_f(W\cup\{a,b\})\ge n\,|R|(|R|-1) for ∣R∣≥7|R|\ge7 (Erdős 624)

Proved
Erdos624.alon_core_average

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

combinatoricserdos-problems

Let CC be a finite set of colours, f:P(U)→Cf:\mathcal P(U)\to C arbitrary, and W⊆UW\subseteq U finite with ∣C∣=n=4⋅2∣W∣|C|=n=4\cdot2^{|W|}. Let R⊆UR\subseteq U be a finite set disjoint from WW with ∣R∣≥7|R|\ge7. Writing Lf(Y)=n−∣f[P(Y)]∣L_f(Y)=n-|f[\mathcal P(Y)]|, the sum over ordered pairs of distinct points satisfies

32∑a∈R ∑b∈R∖{a}Lf(W∪{a,b})  ≥  n ∣R∣ (∣R∣−1).32\sum_{a\in R}\ \sum_{b\in R\setminus\{a\}} L_f(W\cup\{a,b\})\;\ge\; n\,|R|\,(|R|-1).

Proof: palette inequality termwise, then Cauchy–Schwarz over the nn colours for the overlap counts; the threshold ∣R∣≥7|R|\ge7 is exactly what the extremal computation needs.

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 alon_core_average {U : Type*} [DecidableEq U] {C : Type*} [Fintype C] [DecidableEq C]
    (f : Finset U → C) (W R : Finset U) (hRW : Disjoint R W) (hR : 7 ≤ #R)
    (hC : Fintype.card C = 4 * 2 ^ #W) :
    Fintype.card C * (#R * (#R - 1)) ≤
      32 * ∑ a ∈ R, ∑ b ∈ R.erase a,
        (Fintype.card C - #((insert a (insert b W)).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