DISPROVED (LEAN), the site's label; its suffix is a catalog label explained under Formalization. The status-defining source is Ruzsa's theorem (Proc. London Math. Soc. (3) 54 (1987), 38--56, refereed): an essential component $A$ satisfies $\lvert A\cap\{1,\ldots,N\}\rvert\ge(\log N)^{1+c}$ for some $c>0$ and all large $N$, while a lacunary set has only $O(\log N)$ elements up to $N$, so the answer is no. The claim page is Ruzsa, accepted on the site curator's credit and the refereed publication; the 2026 Lean development that declares itself a formalization of his theorem is linked there and gives no formalized evidence, since this corpus has not built or audited it.