Unbounded minimal $T$-proof lengths and $T$-provably total functions

Question

Let $T$ be a sound, r.e. theory containing elementary arithmetic. Fix a $T$-proof predicate $\mathrm{Proof}_T(x,y)$. Let $\phi(x)$ be such that, for all $n$, $T\vdash\phi(n)$; $\forall x\,\phi(x)$ is true but $T$ does not prove it. Define $f(n)$ as the minimal length of the $T$-proof of $\phi(n)$ (i.e. $f(n)$ is the minimal $m$ such that $\mathrm{Proof}_T(m,\ulcorner\phi(n)\urcorner)$). Suppose $f$ is unbounded. Must $f$ dominate all $T$-provably total functions?

Answer 1

No, such an $f$ can grow extremely slowly.

Let $\varphi$ be a formula such that for each $n$, we have $T\vdash\varphi(n)\leftrightarrow $ "there is no $T$-proof of $\varphi(n)$ of length $<n$." The existence of such a formula follows from (the proof of) the diagonal lemma. As long as $T$ is consistent, no $n$ can have $\varphi(n)$ be $T$-provable in length $<n$ (since then $T$ could verify such a proof, which - combined with the above $T$-provable equivalence and the hypothesized proof - would yield a contradiction in $T$). But this means that $T$ does prove $\varphi(n)$ for each $n$ by brute-force-search (which is roughly exponential in length).