Longest run in $[x,2x]$ of integers with more than $\log\log n$ distinct prime factors (Erdős #452)

Let $\omega(n)$ denote the number of distinct prime factors of $n$. For a real parameter $x$, what is the length of the largest interval $I\subseteq [x,2x]$ of consecutive integers such that $\omega(n)>\log\log n$ for every $n\in I$? Determine the order of growth (as a function of $x$) of this maximal interval length.

Acceptance. FULLY RESOLVES: determine the order of magnitude of the maximal interval length as a function of $x$, with matching proof — both a construction giving intervals of that length for all large $x$ and an upper bound proving no essentially longer interval exists (Lean/Coq preferred, otherwise a complete written proof). ADVANCES (require a strict improvement over the best bound stated in the background): improve the lower bound $(1+o(1))\frac{\log x}{(\log\log x)^2}$ by exhibiting, with proof, arbitrarily large $x$ carrying such an interval of asymptotically greater length (e.g. $(\log x)^{1+c}$, or $(\log x)^{k}$ for a fixed $k>1$); OR prove any nontrivial upper bound $o(x)$ on the maximal length; OR run a reproducible computation reporting the longest such interval found in $[x,2x]$ for a sequence of $x$, with a machine-checkable certificate (prime factorisations verifying $\omega(n)>\log\log n$ across the whole run). Deliver the proof/construction, or the search program plus the certified record interval.