Alon palette inequality: $L_f(W\cup\{a,b\})\ge d_a+d_b+|S_a\cap S_b|$ (Erdős 624)

Let $C$ be a finite set of colours and $f:\mathcal P(U)\to C$ an arbitrary map on the finite subsets of a set $U$. Let $W\subseteq U$ be finite with $|C|=4\cdot 2^{|W|}$ (in the application $|W|=k-2$ and $|C|=n=2^k$, so $q:=2^{|W|}=n/4$). For $a\notin W$ define the palette

Then for distinct $a,b\notin W$, writing $L_f(Y)=|C|-|f[\mathcal P(Y)]|$,

Proof idea: $\mathcal P(W\cup\{a,b\})$ splits into four blocks of size $q$; two of them contribute at most $2q$ colours and the two one-point blocks contribute exactly $S_a\cup S_b$.

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.