Seventeen-packet obstruction: three rank-$(k-2)$ colours cannot see 17 packets with exact pair-union kernels at capacity 2 (Erdős 624)

Setting: $U$ is a finite set of inputs, $L:\mathcal P(U)\to\mathcal P(C)$ an arbitrary list map (the actual colour lists), $k$ a natural number. A colour $u$ is nonbottom if $u\notin L(\varnothing)$ and covering if every $k$-subset $Y\subseteq U$ contains some $A$ with $u\in L(A)$. An actual minimal witness of $u$ is $F\subseteq U$ with $u\in L(F)$ and $u\notin L(F')$ for every $F'\subsetneq F$. A valid label for $u$ is a map $p:U\to V$ into an $\mathbb F_2$-vector space with $\sum_{x\in F}p(x)=0$ for every actual minimal witness $F$ with $1\le|F|\le k$. For $T\subseteq U$, $\operatorname{rk}(T)=\dim\operatorname{span}p(T)$ and $\operatorname{rk}(U)=\dim\operatorname{span}p(U)$ (the dimension of the valid parity space). Theorem. Assume $|L(A)|\le2$ for all $A$. Let $c_1,c_2,c_3$ be three distinct nonbottom covering colours with valid labels $p_1,p_2,p_3$ of global rank $\ge k-2$ (stated as $k\le\operatorname{rk}_i(U)+2$). There do not exist 17 pairwise disjoint nonempty packets $P_1,\dots,P_{17}\subseteq U$ such that for all colours $i$ and distinct $j,\ell,m$: $|P_j\cup P_\ell\cup P_m|\le k$; $\sum_{x\in P_j\cup P_\ell}p_i(x)=0$; and every $G\subseteq P_j\cup P_\ell\cup P_m$ with $\sum_{x\in G}p_i(x)=0$ is $\varnothing$ or one of the three pair unions (together: the kernel condition (K) $\ker(p_i|_{P_j\cup P_\ell\cup P_m})=\operatorname{span}\{\chi_{P_j}+\chi_{P_\ell},\chi_{P_j}+\chi_{P_m}\}$).

This is the deterministic core of Sol's 'A Triple-Colour Ramsey Obstruction' (the probabilistic construction of the packets under a joint-balance hypothesis is not formalized here). In that note the packets have a common size $a$ with $3a\le k$; here only $|P_j\cup P_\ell\cup P_m|\le k$ is needed.

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 all $|Y|\ge m$. This is an auxiliary finite statement from Sol's Round 13 notes on the two-track (PAIR) case. It does not settle Erdős Problem 624, PAIR or Step 17; the initial near-critical population those notes start from is not established.