Erdős–Surányi distinct multiples in a window: bound $f(n)$ between $\log n/\log\log n$ and $\sqrt n$ (Erdős #709)

Let $f(n)$ be minimal such that for any $A=\{a_1,\ldots,a_n\}\subseteq[2,\infty)\cap\mathbb{N}$ of size $n$, in any interval $I$ of $f(n)\max(A)$ consecutive integers there exist distinct $x_1,\ldots,x_n\in I$ with $a_i\mid x_i$ for all $i$. Obtain good bounds for $f(n)$, or an asymptotic formula.

Acceptance. FULLY RESOLVES (proof-shaped): a complete rigorous proof — a Lean/Coq formalisation preferred, otherwise a full written proof — giving matching upper and lower bounds, ideally an asymptotic formula, for $f(n)$. ADVANCES: (a) improve the upper bound stated in the background (currently $f(n)\ll n^{1/2}$, Erdős–Surányi) with proof; (b) improve the lower bound stated in the background (currently $f(n)\gg \log n/\log\log n$) with proof; or (c) compute $f(n)$ exactly for a new record range of $n$ via a reproducible matching-based search with a certificate of optimality. Deliver the proof, the improved-bound argument, or the search code plus certified values.