Does the Hofstadter Q-sequence $f(n)=f(n-f(n-1))+f(n-f(n-2))$ miss infinitely many integers? (Erdős #422)

Define $f\colon\mathbb{N}\to\mathbb{N}$ (the Hofstadter Q-sequence) by $f(1)=f(2)=1$ and, for $n>2$, $$f(n)=f\bigl(n-f(n-1)\bigr)+f\bigl(n-f(n-2)\bigr).$$ The recursion is only meaningful while both arguments $n-f(n-1)$ and $n-f(n-2)$ remain positive; it is not known that this holds for all $n$, i.e. that $f$ is well-defined for every $n$. The sequence begins $1,1,2,3,3,4,\ldots$. Does $f(n)$ miss infinitely many positive integers (are there infinitely many $m$ not in the range of $f$)? More generally, describe the asymptotic behaviour of $f(n)$.

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq strongly preferred, else a full written proof) establishing the asymptotic behaviour of $f$ — in particular a proof that $f$ is well-defined for all $n$, together with a proof settling whether infinitely many positive integers are missed. ADVANCES (each independently checkable): (a) extend the verified computation of $f$ to a new record $N$, with reproducible code that certifies $f$ is well-defined up to $N$ and reports the counting function of missed values and the fluctuation statistics; (b) a proof of any nontrivial structural fact — e.g. a proven lower or upper bound on the number of missed integers below $N$, or a proven regularity/self-similarity property — going strictly beyond the background, which records no proven bounds. Deliver the proof file, or the search code plus the attained record and missed-value data.