Least spread $f(n)$ of a factorization of $n!$ into distinct integers (Erdős #393)

Let $f(n)$ be the least $m\geq 1$ for which the factorial $n!$ can be written as a product of distinct increasing integers whose spread is $m$: $$n!=a_1 a_2\cdots a_t,\qquad a_1<a_2<\cdots<a_t=a_1+m$$ (the factors all lie in the interval $[a_1,\,a_1+m]$). In particular $f(n)=1$ means $n!$ is the product of two consecutive integers, $n!=a_1(a_1+1)$. Determine the behaviour of $f(n)$ as $n\to\infty$ (its growth rate, and whether small values recur).

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, otherwise a full written proof) determining the asymptotic behaviour of $f(n)$ — for example an unconditional proof that $f(n)\to\infty$ (removing the abc hypothesis of [Lu02]), or a determination of the true order of growth of $f(n)$, or a proof settling whether $f(n)=1$ for infinitely many $n$. ADVANCES: improve the Bui–Pratt–Zaharescu bound $F_m(N)\ll_m N^{33/34}$ to a strictly smaller exponent, with proof; OR prove an unconditional lower bound such as $f(n)\to\infty$ along a density-1 set of $n$, or under a hypothesis strictly weaker than abc; OR compute $f(n)$ exactly over a substantially extended range with a reproducible search and optimality certificate, reporting the observed growth and any $n$ with $f(n)=1$. Deliver the proof file, the improved-exponent proof, or the search code plus the extended table and certificate.