SOLVED (LEAN), on the site's label: the curator credits Stijn Cambie's observations, that $f$ attains each of its trivial bounds $u+2$ and $u^2$ infinitely often while $f(n)=(1+o(1))n$ for almost all $n$, as settling the natural readings of an estimate question whose intended precision the site calls unclear, and records Lean proofs of these statements outside this corpus; all of this is on the claim page (Cambie, 2025). The Lean proofs are not built here.