Finite-tower bounds for Skolem functions

RESUMO

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 \[ |\Sk_{<E_n(x^m)}|<\omega_{r_n},\qquad r_n=2+\frac{n(n+3)}2\quad(n\ge1,\ m\ge2\text{ fixed}). \] For triple towers we obtain the sharper bound $|\Sk_{<E_3(x^m)}|<\omega_{10}$ for every fixed $m\ge1$. 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 $|\Sk|=\varepsilon_0$.