The theorem I am referring to is Tait's sharpening of Gentzen's Cut Elimination Theorem in [1], which Schütte [2, p. 204, Theorem 22.8] also calls the ``second cut elimination theorem'' (here written in the Tait-style calculus, which derives finite sets--interpreted as disjunctions--of possibly infinitary formulae, also comp. [3, pp. 52f., p. 116]):
$$\text{If } \vdash^{\alpha}_{\beta+\omega^\rho} \Delta \text{ then }\vdash^{\varphi_\rho(\alpha)}_{\beta} \Delta,$$
where $\varphi_\rho (\alpha)$ refers to the Veblen function, comp [4], [6], and $\vdash^{\alpha}_{\beta} \Delta$ means that there is a derivation of $\Delta$ with height $\leq \alpha$ and cut-rank $< \beta$.
The proof proceeds by a nested induction, the main induction on $\rho$ (induction hypothesis: claim holds for all $\xi < \rho$), the side induction on $\alpha$ (ind. hyp.: claim holds for $\rho$ and all $\alpha_0 < \alpha$), and exploits the fact that for any $\sigma < \rho$, $\alpha_0 < \alpha$, and $n \in \mathbb{N}$,
$$\underbrace{\varphi_\sigma(\varphi_\sigma(...}_\text{n-fold}(\varphi_\rho(\alpha_0)+1)...)$$
is majorized by $\varphi_\rho(\alpha)$. This allows to finish the proof.
Now my question is this: I have seen it stated more than once (without argument) that the above result is optimal, in the sense that the 'cost' of eliminating cuts cannot be measured by functions that grow any slower than $\varphi$ (e.g. [5]). This seems to be a somewhat vague claim, and not at all obvious. Can this be made more precise, and can it be proven?
Extra question | On a more general note, I must admit that I do not have a very clear intuition of the Veblen functions. I understand their introduction in terms of enumerating fixed points of normal functions, but to be honest, beyond this purely abstract conceptual grasp, I can't really imagine what they 'look like'. Can anyone, actually? Honestly I am already struggling to put a clear intuition to $\varepsilon_0$ (although I can calculate with it quite well), of which I have read that ''it is easy to visualize'' and therefore ''plain'' that transfinite induction is valid for it [3, p.130]. Now I have no trouble ''visualizing'' hydras or various orderings on finite trees or ordinal notation systems for $\varepsilon_0$ (which convince me of its well-foundedness), but the order type itself? Either I'm (literally) overlooking something ''plain'' and obvious, or this is a massive overstatement. I can't 'see' $\varepsilon_0$, and I certainly can't 'see' what the effect of iterating $\varphi$ 'looks like'. Do you have any suggestions for sharpening my eyes?
[1] W. W. Tait. 1968, Normal derivability in classical logic. In: Jon Barwise, ed., The Syntax and Semantics of Infinitary Languages LNM 72. (Berlin: Springer, 1968), pp. 204-236.
[2] K. Schütte. 1977, Proof Theory, Berlin: Springer.
[3] W. Pohlers. 2009, Proof Theory: The First Step into Impredicativity, Berlin: Springer.
[4] https://plato.stanford.edu/entries/proof-theory/index.html#StroOrdiReprVeblBachHier
[5] https://plato.stanford.edu/entries/proof-theory/index.html#InfiProoForPredTheo