Is the number of divisors of $n$ in $(\sqrt n,\sqrt n+C n^{1/4})$ bounded by an absolute constant? (Erdős #887)

Is there an absolute constant $K$ (independent of everything) with the following property: for every $C>0$, if $n$ is sufficiently large in terms of $C$, then $n$ has at most $K$ divisors in the interval $(n^{1/2},\,n^{1/2}+C n^{1/4})$? The key demand is that the single constant $K$ must work simultaneously for all $C>0$; equivalently, the number of divisors of $n$ in a window of width proportional to $n^{1/4}$ about $\sqrt n$ should be bounded uniformly, no matter how large the proportionality constant $C$ is taken.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, otherwise a full written proof) that such an absolute constant $K$ exists — giving an explicit value and the argument that it bounds the divisor count in $(n^{1/2},\,n^{1/2}+C n^{1/4})$ for all large $n$ uniformly in $C$ — OR a proof that no such $K$ exists, e.g. by producing, for every $K$, arbitrarily large $n$ and some $C$ with more than $K$ divisors in the window. ADVANCES: (a) improve the Erdős–Rosenfeld $1+C^2$ bound toward an absolute constant for a nontrivial class of $n$, with proof; (b) extend Chan's bounded-divisor theorems [Ch14],[Ch15] to a strictly broader class of $n$ (e.g. weaken the near-square hypothesis or lower the constants $5$/$18$ stated in the background), with proof; or (c) computationally exhibit, via a reproducible search with an exhaustiveness certificate, an integer $n$ with strictly more than four divisors in $(n^{1/2},\,n^{1/2}+n^{1/4})$, improving the known lower bound on any admissible $K$. Deliver the proof file, the improved-bound proof, or the search code plus witnesses and certificate.