Finite-tower bounds for Skolem functions

We bound the eventual order types of Skolem functions below finite exponential towers. Writing $E_0(u)=u$, $E_{n+1}(u)=2^{E_n(u)}$, and ${\omega }_0=1$, ${\omega }_{k+1}={\omega }^{{\omega }_k}$, the argument gives $$\mathrm{\mid }{\text{Sk}}_{<E_n(x^m)}\mathrm{\mid }<{\omega }_{r_n},r_n=2+\frac{n(n+3)}{2}(n\ge 1,m\ge 2\text{ fixed})\mathrm{.}$$ For triple towers we obtain the sharper bound $\mathrm{\mid }{\text{Sk}}_{<E_3(x^m)}\mathrm{\mid }<{\omega }_{10}$ for every fixed $m\ge 1$. The proof combines comparisons of asymptotic expansions with finite recursive decompositions and ordinal estimates for ordered sums and products. The analytic part is developed in the classical field of logarithmic-exponential series. We prove the required discreteness, support and truncation statements in this setting. The external inputs are the series construction of van den Dries–Macintyre–Marker and the order and ordinal estimates recalled from Berarducci–Mamino. These bounds imply $\mathrm{\mid }\text{Sk}\mathrm{\mid }={\epsilon }_0$.