Do Beurling generalised primes satisfy #{a_i ≤ x} ≤ π(x)? (Erdős #951)

Let $1<a_1<a_2<\cdots$ be an increasing sequence of real numbers such that $$\left\lvert \prod_i a_i^{k_i}-\prod_j a_j^{\ell_j}\right\rvert \geq 1$$ for every distinct pair of non-negative, finitely supported integer tuples $(k_i)$ and $(\ell_j)$; equivalently, the multiplicatively generated 'generalised integers' $\prod_i a_i^{k_i}$ are pairwise separated by distance at least $1$. Such a sequence is a system of Beurling generalised primes. Writing $\pi(x)$ for the number of ordinary rational primes up to $x$, is it true that $$\#\{i: a_i\leq x\}\leq \pi(x)?$$ Erdős further asks whether equality holds (identically, or asymptotically) if and only if the $a_i$ are exactly the primes.

Acceptance. FULLY RESOLVES: a complete proof that $\#\{i:a_i\leq x\}\leq\pi(x)$ holds for all sufficiently large $x$ (the genuinely open reading) for every admissible Beurling-prime sequence — machine-checkable (extending the existing formalisation) or fully written; OR a disproof for that reading, i.e. an explicit admissible sequence $(a_i)$ together with an unbounded set of $x$ at which $\#\{a_i\leq x\}>\pi(x)$, with a certificate that all generalised integers are separated by $\geq 1$. ADVANCES: (a) settle the finite / 'for all $x$' reading of the #951 inequality itself with a program-checkable admissible finite configuration and an $x$ where $\#\{a_i\leq x\}>\pi(x)$, verifying the separation constraint exactly, and — since small AI-found examples are already claimed for the RELATED Beurling conjecture — either rigorously certify such an example for THIS inequality or exhibit the smallest such $x$ with a proof of minimality; (b) prove the inequality under an added stated hypothesis (e.g. the $a_i$ integers, or a regularity/density condition), with proof; (c) resolve the 'equality iff primes' question. Deliver the proof, or the certified sequence, separation certificate, and the witnessing $x$.