What is the exact proof that Busy Beaver function grows asymptotically faster than any computable function?

Question

I have seen the following formulation of the proof:

If there is a computable function $\forall n\ge n_0:f(n) \ge BB(n)$ then $f(n)$ can be used as an upper bound for $BB(n)$, thus making it computable, which is a contradiction.

However, this is only possible if you know such $f(n)$ exactly. Suppose there is a set $S$ of all computable functions $f(n)$ such that $\forall n\ge n_0:f(n) \ge BB(n)$. The question is, how can one prove $S=\varnothing$?

Notice that so far just an existence of $f(n)\in S$ does not allow to compute $BB(n)$ - you need to also have a procedure that verifies if $f(n)\in S$ in a finite time. Considering that $BB(n)$ is undecidable, no such procedure exists, of course. It seems pretty similar to games where it is known that a winning strategy exists, but finding such a strategy is uncomputable.

None of that seems to be sufficient to prove $S=\varnothing$. Is there something I am missing?

Answer 1

Scott Aaronson's survey paper on the Busy Beaver function includes this proposition, which I think is responsive to your question:

Proposition 3: Let $f : \mathbb{N} \to \mathbb{N}$ be any computable function. Then there exists an $n_f$ such that $BB(n)>f(n)$ for all $n\ge n_f$.

Proof: Let $M_f$ be a Turing machine that computes $f(n)$, for any $n$ encoded on $M_f$'s input tape. Suppose $M_f$ has $c$ states. Then for all $n$, there exists a Turing machine $M_{f,n}$ with $c + O (\log n)$ states that, given an all-$0$ input tape, first writes $n$ onto the input tape, then simulates $M_f$ in order to compute $f(n)$, and finally executes an empty loop for (say) $f(n)^2$ steps. Hence $$BB (c + O (\log n)) > f (n)$$ for all $n$ from which the proposition follows.