Fix a $\Sigma_1$-sound theory $\mathcal{T}$ containing basic (Robinson) arithmetic.
On the one hand, by diagonalizing over the provably total computable functions in $\mathcal{T}$, we can construct a computable function whose totality (well-definedness on all inputs) is not provable in $\mathcal{T}$.
On the other hand, for any computable function $f$, the well-definedness of $f$ on inputs up to any given $n \in \mathbb{N}$ is provable in $\mathcal{T}$. But the proof, in general, grows with $n$ almost as fast as $f$ itself.
It's therefore interesting to consider which functions $f$ are "barely unprovable" in $\mathcal{T}$: that is, within $\mathcal{T}$, the totality of $f$ is not provable, but its well-definedness on inputs up to $n \in \mathbb{N}$ has a proof that grows slowly (polynomially or even linearly) with $n$.
For example, if we're allowed to duplicate / reuse variables, then double exponential functions are barely unprovable in Robinson arithmetic. (Otherwise, only single exponential functions are.) Unlike provably total functions, barely-unprovable ones are not closed under composition. Situations where we want to consider single or double exponentials but not higher elemementary functions seem reasonably common, in some sense precisely because they are barely unprovable using basic arithmetic without induction: e.g. to talk about nodes or subtrees in a fixed-valence tree of height $n$ requires $O(n)$ symbols.
My question is simply whether this notion is discussed at all in the literature, and if so what are some typical or interesting applications (ideally with sources).
