An everywhere-total functional has a computable use bound

For fixed $n$, effectively search for length $m$ and time $t$ such that every binary string $\sigma$ of length $m$ makes ${\mathrm{\Gamma }}^{\sigma }(n)$ halt by $t$ without querying outside $m$.

Suppose the search never succeeds. Call a string $\sigma$ of length $m$ bad if the computation with that finite oracle never halts without a query outside $m$. At every length $m$ there is a bad string: otherwise each of the finitely many length-$m$ strings would halt within $m$, and the maximum of their finite running times would make the search succeed. Every prefix of a bad string is bad, since a halting run using only queries below the prefix length would be the same on every extension. Thus the bad strings form a binary tree with nodes at every level. The empty string has bad extensions at arbitrarily large lengths. Whenever a bad string has bad extensions at arbitrarily large lengths, at least one of its two children does too; otherwise the two finite height bounds would bound all its extensions. Recursively take the child labelled $0$ if it has this property, and otherwise the child labelled $1$. This fixed rule yields an infinite path $X$ of bad strings without any choice principle. If ${\mathrm{\Gamma }}^X(n)$ halted, its finite query witness would be contained below some $m$; then the length-$m$ prefix of $X$ would not be bad, a contradiction. This violates everywhere-totality.

Therefore the search halts; let $b(n)$ be its first successful length. The finite exhaustive test makes $b$ computable, and its defining property forces every oracle computation on $n$ to use only positions below $b(n)$.