Arithmetic of the rank-rich exclusion: $|Q|^4\le2^{132}n^3$, $64|Q|\ge n\Rightarrow n\le2^{156}$ (Erdős 624)

Pure arithmetic. Let $n,s$ be natural numbers with $n>0$. If $n\le 64s$ and $s^4\le 2^{132}n^3$, then $n\le2^{156}$.

In the cross-review, $s=|\mathcal Q_2|$ and the bound $|\mathcal Q_2|^4\le2^{132}n^3$ is the $a=2$ case of the assumed packing theorem (P); the conclusion gives the $k\ge157$ exclusion. (P) is not claimed here; it enters only as the numeric hypothesis $h_2$.

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 12 Step 17 cross-review / resilience analysis of the two-track (PAIR) case. It does not settle Erdős Problem 624, PAIR or Step 17.