Surreal numbers as hyperseries

We first prove the result for \mathfrak{m} \in \mathbf{Mo}_{\omega}, by induction with respect to the simplicity relation \sqsubseteq. The \sqsubseteq-minimal element of \mathbf{Mo}_{\omega} is \omega, which satisfies (?) for \psi = \beta = 0 and \iota = 1. Consider \mathfrak{m} \in \mathbf{Mo}_{\omega} \setminus \{ \omega \} such that the result holds on \mathfrak{m}_{\sqsubset}^{\mathbf{Mo}_{\omega}}. By [vdH:hypno, Proposition 6.20], the monomial \mathfrak{m} is not L_{< \mathbf{On}}-atomic. So there is a maximal \lambda \in \omega^{\mathbf{On}} with \mathfrak{m} \in \mathbf{Mo}_{\lambda}, and we have \lambda \geqslant \omega by our hypothesis.

If there is no ordinal \gamma < \lambda such that E_{\gamma}^{\mathfrak{m}} \in \mathbf{Mo}_{\lambda \omega}, then we have \mathfrak{m} \in \mathbf{Mo}_{\lambda} \setminus L_{< \lambda} \mathbf{Mo}_{\lambda \omega}. So setting \alpha = \lambda, \beta = 0 and u = L_{\lambda} \mathfrak{m}, we are done. Otherwise, let \gamma < \lambda be such that \mathfrak{a} := E_{\gamma}^{\mathfrak{m}} \in \mathbf{Mo}_{\lambda \omega}. We cannot have \gamma = 0 by definition of \lambda. So there is a unique ordinal \eta and a unique natural number n \in \mathbb{N}^{>} such that \gamma = \gamma' + \omega^{\eta} n and \gamma' \gg \omega^{\eta}. Note that \lambda \geqslant \omega^{\eta + 1}. We must have \lambda = \omega^{\eta + 1}: otherwise, L_{\omega^{\eta + 1}} \mathfrak{m}= L_{\gamma' + \omega^{\eta + 1}} (\mathfrak{a}) + n where L_{\omega^{\eta + 1}} \mathfrak{m} and L_{\gamma' + \omega^{\eta + 1}} \mathfrak{a} are monomials. We deduce that \gamma' = 0 and \gamma = \omega^{\eta} n. Note that L_{\lambda} \mathfrak{a} \asymp L_{\lambda} \mathfrak{m}, \lambda < \lambda \omega, and \mathfrak{a} \in \mathbf{Mo}_{\lambda \omega}, so \mathfrak{a}=\mathfrak{d}_{\lambda \omega} (\mathfrak{m}). We deduce that \mathfrak{a} \sqsubset \mathfrak{m}. The induction hypothesis yields a hyperserial expansion \mathfrak{a}= \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^u)^{\iota}. Since \mathfrak{a} is log-atomic, we must have \psi = 0 and \iota = 1. If \mathfrak{a}= L_{\beta} \omega, then \beta \geq\!\!\!\geq \lambda_{/ \omega} = \omega^{\eta}, since \mathfrak{a} \in \mathbf{Mo}_{\lambda \omega}. Thus \mathfrak{m}= L_{\gamma} \mathfrak{a}= L_{\beta + \gamma} \omega is a hyperexponential expansion of type II. If \mathfrak{a}= L_{\beta} E_{\alpha}^u, then likewise \beta \geq\!\!\!\geq \omega^{\eta} and thus \mathfrak{m}= L_{\beta + \gamma} E_{\alpha}^u is a hyperexponential expansion of type I. This completes the inductive proof.

Now let \mathfrak{m} \in \mathbf{Mo}^{\neq} \setminus \mathbf{Mo}_{\omega} and set \varphi := \log \mathfrak{m}. If \varphi is tail-atomic, then there are \psi \in \mathbf{No}_{\succ}, \iota \in \{ - 1, 1 \} and \mathfrak{a} \in \mathbf{Mo}_{\omega} with \varphi = \psi \mathbin{+\!\!\!\!+} \iota \mathfrak{a}. Applying the previous arguments to \mathfrak{a}, we obtain elements \alpha \geqslant \omega, \beta, u with \mathfrak{a}= L_{\beta} E_{\alpha}^u and \beta \omega < \alpha, or an ordinal \beta with \mathfrak{a}= L_{\beta} \omega. Then \mathfrak{m}= \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^u)^{\iota} or \mathfrak{m}= \mathrm{e}^{\psi} (L_{\beta} \omega)^{\iota} is a hyperserial expansion. If \varphi is not tail-atomic, then we have \mathfrak{m}= E_1^{\varphi} is a hyperserial expansion of type I.

We first prove a). Assume that \mathfrak{a} is L_{< \omega^{\mu}}-atomic. Assume for contradiction that \beta'' \neq 0 and let \omega^{\eta} m denote the least non-zero term in the Cantor normal form of \beta''. Since \beta'' < \omega^{\mu_{\small{-}}}, we have \omega^{\eta + 1} < \omega^{\mu} so L_{\omega^{\eta + 1}} \mathfrak{a} is a monomial. But L_{\omega^{\eta + 1}} \mathfrak{a}= L_{\beta''_{\succ \omega^{\eta}}} E_{\alpha}^u - m where L_{\beta''_{\succ \omega^{\eta}}} E_{\alpha}^u is a monomial: a contradiction. So \beta'' = 0. If \alpha = 0 then we are done. Otherwise E_{\alpha}^u \not\in \mathbf{Mo}_{\alpha \omega}, so we must have \alpha \omega > \omega^{\mu}, whence \alpha \geqslant \omega^{\mu}. Conversely, assume that \alpha \geqslant \omega^{\mu} or \alpha = 0, and that \beta'' = 0. If \alpha \neq 0, then then for all \gamma < \omega^{\mu}, we have L_{\gamma} \mathfrak{a}= L_{\beta' + \gamma} E_{\alpha}^u where \beta' + \gamma < \alpha, so L_{\gamma} \mathfrak{a} is a monomial, whence \mathfrak{a} \in \mathbf{Mo}_{\omega^{\mu}}. If \alpha = 0, then for all \gamma < \omega^{\mu}, we have L_{\gamma} \mathfrak{a}= L_{\beta' + \gamma} \omega \in \mathbf{Mo}, whence \mathfrak{a} \in \mathbf{Mo}_{\omega^{\mu}}. This proves a).

Now assume that \alpha \geqslant \omega^{\mu}. So L_{\beta'} E_{\alpha}^u is L_{< \omega^{\mu}}-atomic by a). If \beta'' = 0 then we conclude that \mathfrak{a}= L_{\beta'} E_{\alpha}^u =\mathfrak{d}_{\omega^{\mu}} (\mathfrak{a}). If \beta'' \neq 0, then let \omega^{\eta} m denote the least non-zero term in its Cantor normal form. We have \omega^{\eta + 1} < \omega^{\mu} and L_{\omega^{\eta + 1}} \mathfrak{a}= L_{\omega^{\eta + 1}} L_{\beta'} E_{\alpha}^u - m \asymp L_{\omega^{\eta + 1}} L_{\beta'} E_{\alpha}^u, so L_{\beta'} E_{\alpha}^u =\mathfrak{d}_{\omega^{\mu}} (\mathfrak{a}).

Since L_{\gamma} \mathfrak{b} \in \mathbf{Mo}_{\alpha} \setminus \mathbf{Mo}_{\alpha \omega}, we must have \gamma \neq 0. By Lemma 5.4, we have a hyperserial expansion \mathfrak{b}= \mathrm{e}^{\psi} (L_{\beta} E_{\rho}^u)^{\iota}. Since \mathfrak{b} is log-atomic, we have \log \mathfrak{b}= \psi \mathbin{+\!\!\!\!+} \iota L_{\beta + 1} E_{\alpha}^u \in \mathbf{Mo}, whence \psi = 0 and \iota = 1. So \mathfrak{b}= L_{\beta} E_{\rho}^u. We have \mathfrak{b} \in \mathbf{Mo}_{\alpha \omega} so by Lemma 5.5(5.5), we have \beta \geq\!\!\!\geq \alpha. It follows that L_{\gamma} \mathfrak{b}= L_{\beta + \gamma} E_{\rho}^u is a hyperserial expansion. But then L_{\beta + \gamma} E_{\rho}^u \in \mathbf{Mo}_{\alpha} and Lemma 5.5(5.5) imply that \gamma \geq\!\!\!\geq \omega^{\mu_-}. The condition that \gamma < \alpha now gives \mu_- < \mu, whence \mu is a successor and \gamma = \omega^{\mu_-} n for a certain n \in \mathbb{N}^{>}, as claimed.

Consider a monomial \mathfrak{m} \neq 1 with

where \psi \in \mathbf{No}_{\succ}, \iota \in \{ - 1, 1 \}, \beta, \alpha \in \omega^{\mathbf{On}}, \mathfrak{a} \in \mathbf{Mo}_{\alpha}, \beta \omega < \alpha, and \ensuremath{\operatorname{supp}} \psi \succ L_{\beta + 1} \mathfrak{a}. Assume for contradiction that we can write \mathfrak{m}= \mathrm{e}^{\psi'} (L_{\beta'} E_{\alpha'} u')^{\iota'} as a hyperserial expansion of type I with \alpha' < \alpha. Note in particular that \alpha > 1, so L_{\beta + 1} \mathfrak{a} is log-atomic. We have

If \alpha' = 1, then \beta' = 0, \psi' = 0, \iota' = 1, and u' is not tail-atomic. But \psi \mathbin{+\!\!\!\!+} \iota L_{\beta + 1} \mathfrak{a}= u', where L_{\beta + 1} \mathfrak{a} \in \mathbf{Mo}_{\omega}, so u' is tail-atomic: a contradiction. Hence \alpha' > 1. Note that \iota L_{\beta + 1} \mathfrak{a} and \iota' L_{\beta' + 1} E_{\alpha'}^{u'} are both the least term of \log \mathfrak{m}. It follows that \psi = \psi', \iota = \iota', and

Since \beta' \omega < \alpha', we have

Now E_{\alpha'}^{u'} \not\in \mathbf{Mo}_{\alpha' \omega}, so \mathfrak{d}_{\alpha'} (L_{\beta} \mathfrak{a}) \neq \mathfrak{a} and thus \beta \omega \geqslant \alpha'. In particular \beta > \beta'. Taking hyperexponentials on both sides of Proof Proof, we may assume without loss of generality that \beta' = 0 or that the least exponents \eta and \eta' in the Cantor normal forms of \beta resp. \beta' differ. If \beta' = 0, then we decompose b = \gamma \dotplus \omega^{\eta} n where n \in \mathbb{N}^{>} and \gamma \gg \omega^{\eta}. Since L_{\beta} \mathfrak{a}= E_{\alpha'}^{u'} \in \mathbf{Mo}_{\alpha'} \setminus \mathbf{Mo}_{\alpha' \omega}, applying Lemma 5.5(5.5) twice (for \omega^{\mu} = \alpha' and \omega^{\mu} = \alpha' \omega) gives \omega^{\eta + 1} \geqslant \alpha' and \omega^{\eta + 1} \ngeqslant \alpha' \omega, whence \alpha' = \omega^{\eta + 1}. But then E_{\alpha'}^{u'} = L_{\omega^{\eta} n} \mathfrak{b}, where \mathfrak{b} := L_{\gamma} \mathfrak{a} \in \mathbf{Mo}_{\alpha'} \omega by Lemma 5.5(5.5). So E_{\alpha'}^{u'} \in L_{< \alpha'} \mathbf{Mo}_{\alpha' \omega}: a contradiction. Assume now that \beta' \neq 0. Lemma 5.5(5.5) yields both L_{\beta} \mathfrak{a} \in {\mathbf{Mo}_{\omega^{\eta + 1}} \setminus \mathbf{Mo}_{\omega^{\eta + 2}}} and L_{\beta'} E_{\alpha'}^{u'} \in \mathbf{Mo}_{\omega^{\eta' + 1}} \setminus \mathbf{Mo}_{\omega^{\eta' + 2}}, which contradicts Proof Proof.

Taking \mathfrak{a}= \omega \in \mathbf{No} and \alpha := \max (\alpha' \omega, \beta \omega^2), this proves that no two hyperserial expansions of distinct types I and II can be equal. Taking \mathfrak{a}= E_{\alpha}^u with \alpha > \alpha', this proves that no two hyperserial expansions \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^u)^{\iota}, \mathrm{e}^{\psi'} (L_{\beta'} E_{\alpha'}^{u'})^{\iota'} of type I with \alpha \neq \alpha' can be equal.

The two remaining cases are hyperserial expansions of type II and hyperserial expansions \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^u)^{\iota} and \mathrm{e}^{\psi'} (L_{\beta'} E_{\alpha'}^{u'})^{\iota'} of type I with \alpha = \alpha'. Consider a monomial \mathfrak{m} \in \mathbf{Mo}^{\neq} with the hyperserial expansions \mathfrak{m}= \mathrm{e}^{\psi} (L_{\gamma} \omega)^{\iota} = \mathrm{e}^{\psi'} (L_{\gamma'} \omega)^{\iota'} of type II. As above we have \psi = \psi', \iota = \iota', and L_{\gamma} \omega = L_{\gamma'} \omega. We deduce that \gamma = \gamma', so the expansions coincide.

Finally, consider a monomial \mathfrak{m} \neq 1 with two hyperserial expansions of type I

If \alpha = 1, then we have \psi = \psi' = 0 and \beta = \beta' = 0 and \iota = \iota' = 1, whence u = u', so we are done.

Assume now that \alpha > 1. Taking logarithms in (?), we see that \psi = \psi', \iota = \iota', and

We may assume without loss of generality that \beta \geqslant \beta'. Assume for contradiction that \beta > \beta'. Taking hyperexponentials on both sides of ?, we may assume without loss of generality that \beta' = 0 or that the least exponents \eta and \eta' in the Cantor normal forms of \beta resp. \beta' differ. On the one hand, Lemma 5.5(5.5) yields L_{\beta} E_{\alpha}^u \in \mathbf{Mo}_{\omega^{\eta + 1}} \setminus \mathbf{Mo}_{\omega^{\eta + 2}}. Note in particular that L_{\beta} E_{\alpha}^u \not\in \mathbf{Mo}_{\alpha}, since \beta \omega < \alpha. On the other hand, if \beta \neq 0, then Lemma 5.5(5.5) yields L_{\beta'} E_{\alpha}^{u'} \in \mathbf{Mo}_{\omega^{\eta'}} \setminus \mathbf{Mo}_{\omega^{\eta' + 1}}; if \beta' = 0, then L_{\beta'} E_{\alpha}^{u'} \in \mathbf{Mo}_{\alpha}. Thus ? is absurd: a contradiction. We conclude that \beta = \beta'. Finally E_{\alpha}^u = E_{\alpha}^{u'} yields u = u', so the expansions are identical.

Assume for contradiction that \mathfrak{n} \in \ensuremath{\operatorname{supp}} \psi \cap \ensuremath{\operatorname{supp}} u. In particular \mathfrak{n} \succ L_{\beta + 1} E_{\alpha}^u. Since u > 0, there is r \in \mathbb{R}^{>} with u \geqslant r\mathfrak{n}, so L_{\beta + 1} E_{\alpha}^u \succ \mathfrak{n}: a contradiction.

Let \mathfrak{l} \in \mathfrak{L} \setminus \{ - 1 \} and let P be a path in \mathfrak{l} \circ \omega. If there is an ordinal \gamma with \mathfrak{l}= \ell_{\gamma}, then the hyperserial expansion of \mathfrak{l} \circ \omega is L_{\gamma} \omega, so | P | = 1 if \gamma = 0 and | P | = 2 otherwise. If there is an ordinal \gamma with \mathfrak{l}= \ell_{\gamma}^{- 1}, then the hyperserial expansion of \mathfrak{l} \circ \omega is (L_{\gamma} \omega)^{- 1} and | P | = 2.

Assume now that \mathfrak{l} \not\in \ell_{\mathbf{On}}^{\pm 1}. If \log \mathfrak{l} \circ \omega is not tail-atomic, then hyperserial expansion of \mathfrak{l} \circ \omega is \mathfrak{l} \circ \omega = \mathrm{e}^{\log \mathfrak{l} \circ \omega}. If \log \mathfrak{l} \circ \omega is tail-atomic, then the hyperserial expansion of \mathfrak{l} \circ \omega is \mathfrak{l} \circ \omega = \mathrm{e}^{\psi \circ \omega} (\mathfrak{a} \circ \omega)^{\iota} for a certain log-atomic \mathfrak{a} \in \mathbb{L}. In both cases, P_{\nearrow 1} is a path in some monomial in L_{\mathbf{On}} \omega, whence | P_{\nearrow 1} | \leqslant 2 and | P | \leqslant 3, by the previous argument.

By Lemma 5.12, we have \mathfrak{m} \not\in (L_{\mathbf{On}} \omega)^{\pm 1}. If \mathfrak{m} has a hyperserial expansion of the form \mathfrak{m}= \mathrm{e}^{\psi} (L_{\gamma} \omega)^{\iota}, then P_{\nearrow 1} must be a path in \psi. So \psi is non-zero and thus \lambda = 1. It follows that P_{\nearrow 1} is a path in \log \mathfrak{m}= \psi \mathbin{+\!\!\!\!+} \iota (L_{\gamma} \omega)^{\iota}. Otherwise, let \mathfrak{m}= \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^u)^{\iota} be the hyperserial expansion of \mathfrak{m}. If P_{\nearrow 1} is a path in \psi, then it is a path in \log \mathfrak{m} as above. Otherwise, it is a path in u. Assume that \lambda = 1. If \alpha = 1, then we have \psi = 0 and \log \mathfrak{m}= \iota u so P_{\nearrow 1} is a path in \log \mathfrak{m}. If \alpha > 1, then \log \mathfrak{m}= \psi \mathbin{+\!\!\!\!+} \iota L_{\beta + 1} E_{\alpha}^u where L_{\beta + 1} E_{\alpha}^u is a hyperserial expansion, so P_{\nearrow 1} is a path in \log \mathfrak{m}. Assume now that \lambda > 1, so \psi = 0, \iota = 1, and \alpha \geqslant \omega. We must have \beta \geq\!\!\!\geq \lambda_{/ \omega} so there are \beta' \in \mathbf{On} and n \in \mathbb{N} with \beta' \gg \lambda_{/ \omega} and \beta = \beta' + \lambda_{/ \omega} n. We have L_{\lambda} \mathfrak{m}= L_{\beta' + \lambda} E_{\alpha}^u - n where L_{\beta' + \lambda} E_{\alpha}^u is a hyperserial expansion, so P_{\nearrow 1} is a path in L_{\lambda} \mathfrak{m}.

We prove this by induction on \alpha k, for any number a \in \mathbf{No}^{>, \succ}. We consider a \in \mathbf{No}^{>, \succ}, and a fixed path P in \sharp_{\alpha} (a) with | P | > 1.

Assume that \alpha = k = 1. We have \sharp_1 (a) = a_{\succ} and \mathfrak{d}_{\exp a} = \mathrm{e}^{a_{\succ}}. Assume that a_{\succ} = \psi \mathbin{+\!\!\!\!+} \iota \mathfrak{a} for certain \psi \in \mathbf{No}_{\succ}, \iota \in \{ - 1, 1 \}, and \mathfrak{a} \in \mathbf{Mo}_{\omega}. Let \mathfrak{a}= L_{\gamma} E_{\lambda}^u be the hyperserial expansion of \mathfrak{a}. If \lambda = \omega, then \gamma = 0 and the hyperserial expansion of \mathrm{e}^{\mathfrak{a}} is \mathrm{e}^{\mathfrak{a}} = E_{\omega}^{u + 1}. Therefore P_{\nearrow 1} is a subpath in \mathfrak{d}_{\exp a} = \mathrm{e}^{\psi} (E_{\omega}^{u + 1})^{\iota}. If \lambda > \omega, then the hyperserial expansion of \mathrm{e}^{\mathfrak{a}} is \mathrm{e}^{\mathfrak{a}} = L_{\gamma + 1} E_{\lambda}^u. Therefore P_{\nearrow 1} is a subpath in \mathfrak{d}_{\exp a} = \mathrm{e}^{\psi} (L_{\gamma + 1} E_{\lambda}^u)^{\iota}. Finally, if \mathrm{e}^{a_{\succ}} is not tail-atomic, then P_{\nearrow 1} is a subpath in \mathfrak{d}_{\exp a} = \left( E_1^{\smash{\epsilon a_{\succ}}} \right)^{\epsilon}, where \epsilon \in \{ - 1, 1 \} is the sign of a_{\succ}.

Now assume that \alpha = 1, k > 1, and that the result holds strictly below k. We have E_k a = E_{k - 1} (\exp a) where P_{\nearrow 1} is a subpath in \mathfrak{d}_{\exp a} by the previous argument. We have r\mathfrak{d}_{\exp a} \trianglelefteqslant \sharp_1 (\exp a) for a certain r \in \mathbb{R}^{\neq}, so Q := (r\mathfrak{d}_{\exp a}) \ast P_{\nearrow 1} is a path in \sharp_1 (\exp a). The induction hypothesis on k - 1 implies that Q_{\nearrow 1} = P_{\nearrow 1} is a subpath in \mathfrak{d}_{E_k a}.

Assume now that \alpha \geqslant \omega and that the result holds strictly below \alpha. Write v := \sharp_{\alpha} (a). By (?), there exist \eta \in \mathbf{On}, n < \omega, and \delta \in \mathbf{No} with \beta := \omega^{\eta} < \alpha and

Assume for contradiction that there is a \gamma \in \mathbf{On} with E_{\alpha}^v = L_{\gamma} \omega. We must have \gamma \geq\!\!\!\geq \alpha_{/ \omega}, so there are a number n \in \mathbb{N} and an ordinal \gamma' \geq\!\!\!\geq \alpha with \gamma = \gamma' + \alpha_{/ \omega} n. We have v = {L_{\gamma' + \alpha} \omega - n}. By Lemma 5.12, this contradicts the fact that | P | > 2. So by Lemma 5.4, there exist \beta \in \omega^{\mathbf{On}} and \gamma \in \mathbf{On} with \beta \geqslant \alpha, \gamma \omega < \beta, E_{\alpha}^v = L_{\gamma} E_{\beta}^u, and E_{\beta}^u \in \mathbf{Mo}_{\beta} \setminus L_{< \beta} \mathbf{Mo}_{\beta \omega}. Since E_{\alpha}^v \in \mathbf{Mo}_{\alpha}, we must have \gamma \geq\!\!\!\geq \alpha_{/ \omega} so there are a number n \in \mathbb{N} and an ordinal \gamma' \geq\!\!\!\geq \alpha with \gamma = \gamma' + \alpha_{/ \omega} n (note that n = 0 whenever \alpha_{/ \omega} = \alpha). Thus v + n = L_{\alpha} L_{\gamma' + \alpha_{/ \omega} n} E_{\beta}^u + n = L_{\gamma' + \alpha} E_{\beta}^u is a monomial with hyperserial expansion v + n = L_{\gamma' + \alpha} E_{\beta}^u. There is no path in n of length > 1, so P must be a path in L_{\gamma' + \alpha} E_{\beta}^u. We deduce that P_{\nearrow 1} is a path in u. Consequently, Q = (L_{\gamma} E_{\beta}^u) \ast P_{\nearrow 1} is a path in E_{\alpha}^v with | Q | = | P | > 1. Applying n times Lemma 5.14, we deduce that Q_{\nearrow 1} = P_{\nearrow 1} is a subpath in L_{\beta n} E_{\alpha}^v, hence in \sharp_{\beta} (L_{\beta n} E_{\alpha} a). Consider a path R in \sharp_{\beta} (L_{\beta n} E_{\alpha} a) with P_{\nearrow 1} = R_{\nearrow i} for a certain i > 0. Applying the induction hypothesis for L_{\beta n} E_{\alpha} a and \beta n in the roles of a and \alpha k, the path R_{\nearrow 1} is a subpath in \mathfrak{d}_{E_{\beta n} (L_{\beta n} E_{\alpha} a)} =\mathfrak{d}_{E_{\alpha} a}. Therefore P_{\nearrow 1} is a subpath in \mathfrak{d}_{E_{\alpha} a}. We deduce as in the case \alpha = 1 that P_{\nearrow 1} is a subpath in \mathfrak{d}_{E_{\alpha k} a}.

Let \mathfrak{m}= \mathrm{e}^{\varphi} (L_{\beta} E_{\alpha}^u)^{\iota} be a hyperserial expansion. The condition \ensuremath{\operatorname{supp}} \psi \succ \log \mathfrak{m} implies \varphi + \psi = \varphi \mathbin{+\!\!\!\!+} \psi, whence \mathrm{e}^{\psi} \mathfrak{m}= \mathrm{e}^{\psi \mathbin{+\!\!\!\!+} \varphi} (L_{\beta} E_{\alpha}^u)^{\iota} is also a hyperserial expansion. In particular P_{\nearrow 1} is a subpath in \mathrm{e}^{\psi} \mathfrak{m}.

Write \beta = \omega^{\eta_1} m_1 + \cdots + \omega^{\eta_k} m_k in Cantor normal form, with \eta_1 > \cdots > \eta_k and m_1, \ldots, m_k \in \mathbb{N}^{>} and let

for all i = 1, \ldots, k.

Assume that P shares a subpath with \varphi. In other words, there is a path R in \varphi which has a common subpath with P. The path R must be infinite, so by Lemma 5.15, it shares a subpath with E_{\alpha}^{\varphi} =\mathfrak{a}_1. Let us prove by induction on i = 1, \ldots, k that R shares a subpath with E_{\alpha}^{\varphi} =\mathfrak{a}_i. Assuming that this holds for i < k, we note that \mathfrak{a}_i is L_{< \omega^{\eta_{i - 1}} \omega}-atomic, hence L_{< \omega^{\eta_i}}-atomic. So P shares a subpath with \mathfrak{a}_{i + 1} by Lemma 5.14 and the induction hypothesis. We conclude by induction that P shares a subpath with \mathfrak{a}_k = L_{\beta} E_{\alpha}^{\varphi}.

Suppose conversely that P shares a subpath with L_{\beta} E_{\alpha}^{\varphi} =\mathfrak{a}_k. By induction on i = k - 1, \ldots, 1, it follows from Lemma 5.15 that P shares a subpath with \mathfrak{a}_i. Applying Lemma 5.14 to \mathfrak{a}_1 = E_{\alpha}^{\varphi}, we conclude that P shares a subpath with \varphi.

The condition \mathfrak{m} \in \mathcal{E}_{\omega} [\mathfrak{n}] yields \log \mathfrak{m} \prec \mathfrak{n}. We have \mathrm{e}^{\mathfrak{m}} \sqsubseteq \mathrm{e}^{\mathfrak{n}} by Lemma 5.23. The identity \mathrm{e}^{\mathbf{Mo}^{\succ}} = \mathbf{Smp}_{\mathcal{P}} implies that \mathrm{e}^{\mathfrak{m}} \sqsubseteq \mathrm{e}^{| r | \mathfrak{n}}, whence \mathrm{e}^{\ensuremath{\operatorname{sign}} (r) \mathfrak{m}} \sqsubseteq \mathrm{e}^{r\mathfrak{n}} by Lemma 5.21. Lemma 5.22 yields \mathrm{e}^{\varphi \mathbin{+\!\!\!\!+} \ensuremath{\operatorname{sign}} (r) \mathfrak{m}} \sqsubseteq \mathrm{e}^{\varphi \mathbin{+\!\!\!\!+} r\mathfrak{n}}. Since \mathrm{e}^0 = 1 \sqsubseteq \mathrm{e}^{\delta} \in \mathbf{No}^{>}, we may apply Lemma 5.22 to \varphi \mathbin{+\!\!\!\!+} r\mathfrak{n} and \varphi \mathbin{+\!\!\!\!+} r\mathfrak{n} \mathbin{+\!\!\!\!+} \delta to obtain \mathrm{e}^{\varphi \mathbin{+\!\!\!\!+} r\mathfrak{n}} \sqsubseteq \mathrm{e}^{\varphi \mathbin{+\!\!\!\!+} r\mathfrak{n} \mathbin{+\!\!\!\!+} \delta}. We conclude using the transitivity of \sqsubseteq.

By (?), we have

Since \varphi \sqsubseteq \psi, we have \varphi_L^{\mathbf{No}_{\succ, \alpha}} \subseteq \psi_L^{\mathbf{No}_{\succ, \alpha}} and \varphi_R^{\mathbf{No}_{\succ, \alpha}} \subseteq \psi_R^{\mathbf{No}_{\succ, \alpha}}, whence

Furthermore, we have L_{\alpha} E_{< \alpha} \varphi < \psi, so E_{< \alpha} \varphi < E_{\alpha}^{\psi}. We conclude that E_{\alpha}^{\varphi} \sqsubseteq E_{\alpha}^{\psi}.

Let \nu \in \mathbf{On} and \alpha := \omega^{\nu}. Assume for contradiction that b \in \mathbf{No}_{\succ, \alpha} and a \not\in \mathbf{No}_{\succ, \alpha}. Assume first that a \vartriangleleft b, so b = a \mathbin{+\!\!\!\!+} \delta. Then \ensuremath{\operatorname{supp}} b \succ \frac{1}{L_{< \alpha} E_{\alpha} b}. Let k \in \mathbb{N}^{>} be such that a \mathbin{+\!\!\!\!+} k\mathfrak{d}_{\delta} \geqslant b. Since \ensuremath{\operatorname{supp}} (a \mathbin{+\!\!\!\!+} k\mathfrak{d}_{\delta}) \subseteq \ensuremath{\operatorname{supp}} b, we deduce that \ensuremath{\operatorname{supp}} (a + k\mathfrak{d}_{\delta}) \succ \frac{1}{L_{< \alpha} E_{\alpha} (a + k\mathfrak{d}_{\delta})}, whence {a + k\mathfrak{d}_{\delta}} \in \mathbf{No}_{\succ, \alpha}. Modulo replacing b by a + k\mathfrak{d}_{\delta}, it follow that we may assume without loss of generality that \delta = k\mathfrak{p} for some k \in \mathbb{N}^{>} and some monomial \mathfrak{p}.

On the one hand, a is not \alpha-truncated, so there are \mathfrak{q} \in (\ensuremath{\operatorname{supp}} \varphi)_{\prec} and \gamma with 0 < \gamma < \alpha and a < L_{\alpha}^{\mathord{\uparrow} \gamma} (\mathfrak{q}^{- 1}). We may choose \gamma = \omega^{\eta} n for certain \eta < \nu and n \in \mathbb{N}^{>}, so a < L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} n} (\mathfrak{p}^{- 1}). On the other hand, a + k\mathfrak{p} is \alpha-truncated, so we have

We deduce that k\mathfrak{p}> L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} (n +\mathbb{N}^{>})} (\mathfrak{p}^{- 1}) - L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} n} (\mathfrak{p}^{- 1}). If \nu is a successor, then choosing {\eta = \nu_-}, we obtain k\mathfrak{p}> L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} n} (\mathfrak{p}^{- 1}) +\mathbb{N}^{>} - L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} n} (\mathfrak{p}^{- 1}), so k\mathfrak{p} \succ 1: a contradiction. Otherwise, k\mathfrak{p}> \ell_{[\omega^{\eta + 1}, \alpha)}^{- 1} \circ \mathfrak{p}^{- 1} by [BvdHK:hyp, (2.4)], where \ell_{[\omega^{\eta + 1}, \alpha)} := \prod_{\omega^{\eta + 1} \leqslant \gamma < \alpha} \ell_{\gamma}. Thus k^{- 1} \mathfrak{p}^{- 1} < {\ell_{[\omega^{\eta + 1}, \alpha)} \circ \mathfrak{p}^{- 1}}, whence k^{- 1} \ell_0 < \ell_{[\omega^{\eta + 1}, \alpha)}: a contradiction.

We now treat the general case. By a similar argument as above, we may assume without loss of generality that b = \varphi \mathbin{+\!\!\!\!+} s\mathfrak{n}. Assume that b \leqslant a. Since a is not \alpha-truncated, there exists a \gamma < \alpha with \mathfrak{m} \prec (L_{\gamma} E_{\alpha} a)^{- 1} \leqslant (L_{\gamma} E_{\alpha} b)^{- 1}, whence \mathfrak{m}^{- 1} \succ L_{\gamma} E_{\alpha} b. But b is \alpha-truncated, so \mathfrak{n}^{- 1} \prec L_{< \alpha} E_{\alpha} b. In particular \mathfrak{n}^{- 1} \prec L_{\gamma} E_{\alpha} b, so our hypothesis \mathfrak{m}^{- 1} < L_{\rho} \mathfrak{n}^{- 1} implies that \mathfrak{m}^{- 1} \prec L_{\rho} L_{\gamma} E_{\alpha} b \preccurlyeq L_{\gamma} E_{\alpha} b: a contradiction.

Assume now that b > a. As in the first part of the proof, there are \eta < \nu and n < n' < \omega with \varphi \mathbin{+\!\!\!\!+} s\mathfrak{n}> L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} n'} (\mathfrak{n}^{- 1}) and L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} n} (\mathfrak{m}^{- 1}) > \varphi \mathbin{+\!\!\!\!+} r\mathfrak{m}. Recall that \mathfrak{m}^{- 1} < E_{\rho} \mathfrak{n}^{- 1} for sufficiently large \rho < \alpha. Take \eta < \nu and n' < \omega such that

Then b - a > L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} (n + 1)} (\mathfrak{m}^{- 1}) - L_{\alpha}^{\mathord{\uparrow} \omega^{\eta} n} (\mathfrak{m}^{- 1}). If \nu is a successor, then choosing \eta = \nu_- yields b - a > 1, which contradicts the fact that \mathfrak{m} and \mathfrak{n} are infinitesimal. So \nu is a limit. Writing \mathfrak{q} := \max (\mathfrak{m}, \mathfrak{n}), we have b - a \asymp \mathfrak{q}. As in the first part of the proof, we obtain \mathfrak{q} \succcurlyeq {\ell_{[\omega^{\eta + 1}, \alpha)}^{- 1} \circ \mathfrak{m}^{- 1}}, so \mathfrak{q}^{- 1} \preccurlyeq \ell_{[\omega^{\eta + 1}, \alpha)} \circ \mathfrak{m}^{- 1} \prec \mathfrak{m}^{- 1}. In view of (?), we also obtain \mathfrak{q}^{- 1} \prec \mathfrak{n}^{- 1}, so \mathfrak{q}^{- 1} \prec \max (\mathfrak{m}, \mathfrak{n})^{- 1}: a contradiction.

Assume that L_{\alpha} u <\mathcal{E}_{\alpha} v. Let h \in \mathcal{E}_{\alpha'} and let h^{\ensuremath{\operatorname{inv}}} be its functional inverse in \mathcal{E}_{\alpha'}. We have h^{\ensuremath{\operatorname{inv}}} < E_{\alpha'} H_2 L_{\alpha'} by (?, ?), whence h > E_{\alpha'} H_{1 / 2} L_{\alpha'}. Furthermore, u < E_{\alpha} \mathcal{E}_{\alpha} v, so

We want to prove that E_{\alpha} u < (E_{\alpha'} h E_{\alpha}) v. By (Proof), it is enough to prove that there is a g \in \mathcal{E}_{\alpha} such that the inequality E_{\alpha} E_{\alpha} g \leqslant E_{\alpha'} h E_{\alpha} holds on \mathbf{No}^{>, \succ}.

Assume that \alpha = \alpha'. Setting g := H_{1 / 2} \in \mathcal{E}_{\alpha}, we have L_{\alpha} h E_{\alpha} > g, whence E_{\alpha} g \leqslant h E_{\alpha}, and E_{\alpha} E_{\alpha} g \leqslant E_{\alpha} h E_{\alpha}.

Assume that \alpha' > \alpha. We have E_{\alpha'} H_{1 / 2} > H_2 so E_{\alpha' 2} H_{1 / 2} > E_{\alpha'} H_2 > E_{\alpha} E_{\alpha'} by (?). Thus {E_{\alpha'} h > E_{\alpha' 2} H_{1 / 2} L_{\alpha'} > E_{\alpha}}. Consequently, E_{\alpha'} h E_{\alpha} > E_{\alpha} E_{\alpha}, as claimed.

We prove this by induction on n with a \lesssim_n c. Let P be an infinite path in a. Assume that a \lesssim_0 c. If a \trianglelefteqslant c, then we have a \trianglelefteqslant b so P is a path in b. Otherwise, there are \varphi, \delta \in \mathbf{No}, r \in \mathbb{R}^{\neq} and \mathfrak{m} \in \mathbf{Mo} with a = \varphi \mathbin{+\!\!\!\!+} \ensuremath{\operatorname{sign}} (r) \mathfrak{m} and c = \varphi \mathbin{+\!\!\!\!+} r\mathfrak{m} \mathbin{+\!\!\!\!+} \delta. Then b = \varphi \mathbin{+\!\!\!\!+} s\mathfrak{n} \mathbin{+\!\!\!\!+} t for certain t \in \mathbf{No}, s \in \mathbb{R}^{\neq} and \mathfrak{n} \in \mathbf{Mo} with s\mathfrak{n} \in [\ensuremath{\operatorname{sign}} (r) \mathfrak{m} \leftrightarrow r\mathfrak{m}]. We must have \mathfrak{n}=\mathfrak{m}. If P is a path in \varphi, then it is a path in b. Otherwise, it is a path in \ensuremath{\operatorname{sign}} (r) \mathfrak{m}, so P_{\nearrow 1} is a subpath in s\mathfrak{m}, hence in b.

We now assume that a \lesssim_n c where n > 0 and that the result holds for all a', b', c' \in \mathbf{No} and k < n with a' \lesssim_k c' and b' \in [a' \leftrightarrow c']. Assume first that (a, c) is in ?, and write

Then we can write b = \varphi \mathbin{+\!\!\!\!+} s\mathfrak{m} \mathbin{+\!\!\!\!+} t like in the case when n = 0. If P is a path in \varphi, then it is a path in b. So we may assume that P is a path in \ensuremath{\operatorname{sign}} (r) \mathrm{e}^{\psi} (E_{\alpha}^u)^{\iota}. Note that we have \mathfrak{m} \in [\mathrm{e}^{\psi} (E_{\alpha}^u)^{\iota} \leftrightarrow \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^v)^{\iota}]. Setting \mathfrak{n} := (\mathfrak{m} \mathrm{e}^{- \psi})^{\iota} \in [E_{\alpha}^u \leftrightarrow L_{\beta} E_{\alpha}^v], we observe that \ensuremath{\operatorname{supp}} \log \mathfrak{n} \prec \ensuremath{\operatorname{supp}} \psi, whence \mathrm{e}^{\psi} \mathfrak{n}^{\iota} is the hyperserial expansion of \mathfrak{m}. If P_{\nearrow 1} is a path in \psi, then it is a path in \mathfrak{m}.

Suppose that P_{\nearrow 1} is not a path in \psi. Assume first that \alpha = 1, so \psi = 0, \beta = 0, and P is a path in (E_1^u)^{\iota}. Then Lemma 5.14 implies that P_{\nearrow 1} is a subpath in \iota u, so P_{\nearrow 2} is a subpath in u. Otherwise, consider the hyperserial expansion E_{\alpha}^u = L_{\beta'} E_{\alpha'}^w, E_{\alpha'}^w \in \mathbf{Mo}_{\alpha'} \setminus L_{< \alpha'} \mathbf{Mo}_{\alpha' \omega} of E_{\alpha}^u. Since P_{\nearrow 1} is not a path in \psi, it must be a path in w. The number L_{\beta'} E_{\alpha'}^w is L_{< \alpha}-atomic, so we must have \alpha' \geqslant \alpha and \beta' \geq\!\!\!\geq \alpha_{/ \omega}. There are n \in \mathbb{N} and \beta'' \gg \alpha_{/ \omega} such that \beta' = \beta'' + \alpha_{/ \omega} n. Therefore u = L_{\beta'' + \alpha} E_{\alpha'}^w - n. It follows by Corollary 5.17 that P_{\nearrow 1} shares a subpath with u, whence so does P.

Let z := \sharp_{\alpha} (L_{\alpha} \mathfrak{n}). Recall that \mathfrak{n} \in [E_{\alpha}^u \leftrightarrow L_{\beta} E_{\alpha}^v], so L_{\alpha} \mathfrak{n} \in [u \leftrightarrow L_{\alpha} L_{\beta} E_{\alpha}^v]. Now (?) implies that L_{\beta} E_{\alpha}^v \in \mathcal{E}_{\alpha} [E_{\alpha}^v], so L_{\alpha} L_{\beta} E_{\alpha}^v \in L_{\alpha} \mathcal{E}_{\alpha} [E_{\alpha}^v] =\mathcal{L}_{\alpha} [v]. The function \sharp_{\alpha} = \pi_{\mathbf{Smp}_{\mathcal{L}_{\alpha}}} is non-decreasing, so

But u \lesssim_{n - 1} v, so the induction hypothesis yields that P_{\nearrow 2}, and thus P, shares a subpath with z. We deduce with Lemma 5.15 that P shares a subpath with \mathfrak{n}, hence with b.

Assume now that (a, c) is in ?, and write

Note that we also have \psi \lesssim_{n - 1} \psi' \mathbin{+\!\!\!\!+} \iota \log \mathfrak{a}. We may again assume that P_{\nearrow 1} is a path in \psi. Write b = \varphi \mathbin{+\!\!\!\!+} s' \mathfrak{q} \mathbin{+\!\!\!\!+} t', where s' \in \mathbb{R}^{\neq}, t' \in \mathbf{No}, and \mathfrak{q} \in [\mathrm{e}^{\psi} \leftrightarrow \mathrm{e}^{\psi'} \mathfrak{a}^{\iota}] \cap \mathbf{Mo}. Then \log \mathfrak{q} \in [\psi \leftrightarrow \psi' \mathbin{+\!\!\!\!+} \iota \log \mathfrak{a}] where \psi \lesssim_{n - 1} \psi' \mathbin{+\!\!\!\!+} \iota \log \mathfrak{a}. We deduce by induction that P shares a subpath with \log \mathfrak{q}. By Lemma 5.15, it follows that P shares a subpath with \mathfrak{q}, hence with b. This concludes the proof.

5.29. If \log E_{\alpha}^c \nprec \ensuremath{\operatorname{supp}} \psi, then we have \psi \neq 0, so \alpha > 1. Let \mathfrak{m} \in \ensuremath{\operatorname{supp}} \psi with \log E_{\alpha}^c \succcurlyeq \mathfrak{m}. Since \log E_{\alpha}^c and \mathfrak{m} are monomials, we have \mathfrak{m} \leqslant \log E_{\alpha}^c, whence \mathrm{e}^{\mathfrak{m}} \leqslant E_{\alpha}^c. Our assumption that \mathfrak{m} \in \ensuremath{\operatorname{supp}} \psi \succ \log L_{\beta} E_{\alpha}^b also implies \mathrm{e}^{\mathfrak{m}} \leqslant L_{\beta} E_{\alpha}^b. Hence \mathrm{e}^{\mathfrak{m}} \in [E_{\alpha}^c \leftrightarrow L_{\beta} E_{\alpha}^b]. Now P shares a subpath with E_{\alpha}^c, by Lemma 5.15. Since E_{\alpha}^c \lesssim L_{\beta} E_{\alpha}^b, Proposition 5.28 next implies that P shares a subpath with \mathrm{e}^{\mathfrak{m}}. Using Lemma 5.14, we conclude that P shares a subpath with \mathfrak{m}, and hence with \psi.

?. Let \mathfrak{m} \in \ensuremath{\operatorname{supp}} \varphi with \mathfrak{m} \preccurlyeq \mathrm{e}^{\psi} (E_{\alpha}^c)^{\iota}. It is enough to prove that P shares a subpath with \mathfrak{m}. Since \mathfrak{m}, \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^b)^{\iota}, and \mathrm{e}^{\psi} (E_{\alpha}^c)^{\iota} are monomials, we have \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^b)^{\iota} \leqslant \mathfrak{m} \leqslant \mathrm{e}^{\psi} (E_{\alpha}^c)^{\iota}. Let \mathfrak{n} := (\mathrm{e}^{- \psi} \mathfrak{m})^{\iota}, so that \mathfrak{n} \in [L_{\beta} E_{\alpha}^b \leftrightarrow E_{\alpha}^c]. In particular, we have \ensuremath{\operatorname{supp}} \psi \succ \log \mathfrak{n} \succ 1. Moreover E_{\alpha}^c \lesssim L_{\beta} E_{\alpha}^b, so using Lemma 5.15 and Proposition 5.28, we deduce in the same way as above that P shares a subpath with \mathfrak{n}. If \mathfrak{n} \not\in \mathbf{Mo}_{\omega}, then \mathfrak{m}= \mathrm{e}^{\psi \mathbin{+\!\!\!\!+} \iota \log \mathfrak{n}} is the hyperserial expansion of \mathfrak{m}, so P shares a subpath with \mathfrak{m}. If \mathfrak{n} \in \mathbf{Mo}_{\omega}, then the hyperserial expansion of \mathfrak{n} must be of the form \mathfrak{n}= E_{\beta'} E_{\alpha'}^u, since otherwise \log \mathfrak{n} would have at least two elements in its support. We deduce that P shares a subpath with u and that the hyperserial expansion of \mathfrak{m} is \mathrm{e}^{\psi} (E_{\beta'} E_{\alpha'}^u)^{\iota}. Therefore P shares a subpath with \mathfrak{m}.

?. We assume that a' is not \lambda-truncated whereas \log E_{\alpha}^c \prec \ensuremath{\operatorname{supp}} \psi and \mathrm{e}^{\psi} (E_{\alpha}^c)^{\iota} \prec \ensuremath{\operatorname{supp}} \varphi. If \lambda = 1, then we must have \mathrm{e}^{\psi} (E_{\alpha}^c)^{\iota} \preccurlyeq 1, which means that \psi < 0 or that \psi = 0 and \iota = - 1. But then \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^b)^{\iota} \preccurlyeq 1: a contradiction.

Assume that \lambda > 1. By Lemma 5.26, we may assume without loss of generality that \delta = 0. The assumption on a' and the fact that a \in \mathbf{No}^{>, \succ} imply that \varphi is non-zero. Write

So a = \varphi \mathbin{+\!\!\!\!+} r\mathfrak{q} and a' = \varphi \mathbin{+\!\!\!\!+} \ensuremath{\operatorname{sign}} (r) \mathfrak{p}. Note that \mathfrak{p} must be infinitesimal since a' is not \lambda-truncated. Thus \mathfrak{q} is also infinitesimal. By Lemma 5.26, we deduce that E_{< \lambda} \mathfrak{q}^{- 1} \prec \mathfrak{p}^{- 1}. We have \sharp_{\lambda} (a') \vartriangleleft a', so \sharp_{\lambda} (a') = \varphi, since a and \varphi \vartriangleleft a are both \lambda-truncated. Since a' is not \lambda-truncated, there is an ordinal \gamma < \lambda with \mathfrak{p} \prec (L_{\gamma} E_{\lambda}^{\varphi})^{- 1}. If \varphi \geqslant a, then \mathfrak{q} \succ (L_{< \lambda} E_{\lambda}^a)^{- 1}, because a is \lambda-truncated. Thus \mathfrak{q} \succ (L_{< \lambda} E_{\lambda}^{\varphi})^{- 1}. If \varphi < a, then \varphi + (L_{< \lambda} E_{\lambda}^{\varphi})^{- 1} \in \mathcal{L}_{\lambda} [\varphi] <\mathcal{L}_{\lambda} [a] \ni a = \varphi \mathbin{+\!\!\!\!+} r\mathfrak{q}, because \varphi and a are \lambda-truncated. Now r > 0, since \varphi < a. We again deduce that \mathfrak{q} \succ (L_{< \lambda} E_{\lambda}^{\varphi})^{- 1}.

In both cases, we have L_{\gamma} E_{\lambda}^{\varphi} \in [\mathfrak{p}^{- 1} \leftrightarrow \mathfrak{q}^{- 1}] where \mathfrak{p}^{- 1} \lesssim \mathfrak{q}^{- 1}, so P shares a subpath with L_{\gamma} E_{\lambda}^{\varphi}, by Proposition 5.28. It follows by Corollary 5.17 that P shares a subpath with \varphi.

Using backward induction on k, let us prove for k = i - 1, \ldots, 0 that

and that (Proof) and (Proof) also hold for k = - 1. Given j\leq i-1, we use the index notation (Proof)_i to refer to the equation (Proof) for k=i, and so on for the other conditions.

We first treat the case when k = i - 1. Note that c_i \neq 0 since it contains a subpath, so \varphi_i \in \mathbf{No}^{>, \succ} or \chi = 1. From our assumption that c_i = \varphi_i \mathbin{+\!\!\!\!+} \chi \ensuremath{\operatorname{sign}} (r_i) \mathrm{e}^{\psi_{i + 1}} \mathfrak{p}^{\iota_i} and the fact that \mathfrak{p} \in \mathcal{E}_{\omega} [E_{\alpha_i}^{u_{i + 1}}] if \psi_{i + 1} = 0, we deduce that c_i \in \mathcal{E}_{\omega} [u_i]. Hence L_{\alpha_{i - 1}} c_i <\mathcal{E}_{\alpha_{i - 1}} u_i and (Proof)_i - 1. Note that (Proof)_i - 1 and (Proof)_i - 1 follow immediately from the other assumptions on c_i. If \chi = 0 then c_i = \varphi_i \trianglelefteqslant u_i. If \chi = 1, then \mathfrak{p} \sqsubseteq L_{\beta_i} E_{\alpha_i}^{u_{i + 1}}, since L_{\beta_i} E_{\alpha_i}^{u_{i + 1}} \in \mathcal{E}_{\alpha_i} [E_{\alpha_i}^{u_{i + 1}}] and \mathfrak{p} \sqsubseteq E_{\alpha_i}^{u_{i + 1}} \sqsubseteq \mathcal{E}_{\alpha_i} [E_{\alpha_i}^{u_{i + 1}}]. Hence \mathfrak{p}^{\iota_i} \sqsubseteq (L_{\beta_i} E_{\alpha_i}^{u_{i + 1}})^{\iota_i} by Lemma 5.21 and \ensuremath{\operatorname{sign}} (r_i) \mathrm{e}^{\psi_{i + 1}} \mathfrak{p}^{\iota_i} \sqsubseteq r_i \mathrm{e}^{\psi_{i + 1}} (L_{\beta_i} E_{\alpha_i}^{u_{i + 1}})^{\iota_i} by Lemmas 5.19 and 5.22. Finally, c_i \sqsubseteq u_i by Lemma 5.20, so (Proof)_i - 1 holds in general. Recall that P is a subpath in c_i, but that it shares no subpath with \psi_i or \varphi_{i - 1}. In view of (Proof)_i - 1, we deduce (Proof)_i - 1 from Lemma 5.29(5.29) and (Proof)_i - 1 from Lemma 5.29(?). Combining (Proof)_i - 1, (Proof)_i - 1 and (Proof)_i - 1 with the relation c_i \lesssim u_i, we finally obtain (Proof)_i - 1.

Let k \in \{ 0, \ldots, i - 1 \} and assume that (Proof–Proof)_\ell hold for all \ell \geqslant k. We shall prove (Proof–Proof)_k - 1 if k > 0, as well as (Proof)_- 1 and (Proof)_- 1. Recall that

This concludes our inductive proof. The lemma follows from (Proof)_- 1 and (Proof)_- 1.

Let i \in \mathbb{N}. We have r_{P, i} \in \{ - 1, 1 \} because i is a good index for (P, a). We have \psi_{P, i + 1} \in \mathbf{No}_{\succ} and a_{P, i + 1} \in \mathbf{No}_{\succ, \alpha_i} by the definition of hyperserial expansions. If i > 0 and \varphi_i \neq 0, then we have \varphi_i \in \mathbf{No}^{>, \succ} because a_{P, i} \in \mathbf{No}^{>, \succ} by the definition of paths. Lemma 5.26 also yields \varphi_i \in \mathbf{No}_{\succ, \alpha_i}. This proves the conditions a) and b) for coding sequences. Assume that \alpha_i = 1. Then by the definition of hyperserial expansions, we have \psi_{P, i + 1} = 0 and u_{P, i + 1} = a_{P, i + 1} is not tail-atomic. Assume that \psi_{P, i + 2} = 0. Then \ensuremath{\operatorname{supp}} u_{P, i + 1} \succ 1 so \iota_{P, i + 2} = 1. We have u_{P, i + 1} = \varphi_{i + 1} \mathbin{+\!\!\!\!+} r_{P, i + 1} \mathfrak{a} where \mathfrak{a} := E_{\alpha_{P, i + 1}}^{u_{P, i + 2}} and u_{P, i + 1} is not tail-atomic. This implies that \mathfrak{a} is not log-atomic, so \alpha_{P, i + 1} = 1. Thus c) is valid.

Assume that \varphi_{i + 1} = \psi_{P, i + 2} = 0. Recall that a_{P, i + 1} = r_{P, i + 1} (E_{\alpha_{P, i + 1}}^{u_{P, i + 2}})^{\iota_{P, i + 1}} = u_{P, i + 1} \in \mathbf{No}^{>, \succ}, so r_{P, i + 1} = \iota_{P, i + 1} = 1. Since E_{\alpha_{P, i}}^{u_{P, i + 1}} \not\in \mathbf{Mo}_{\alpha_{P, i} \omega}, we have u_{P, i + 1} \not\in \mathbf{Mo}_{\alpha_{P, i} \omega}, whence \alpha_{P, i + 1} \leqslant \alpha_{P, i}. This proves d).

Assume now for contradiction that there is an i_0 \in \mathbb{N} with \varphi_{P, j} = \psi_{P, j + 1} = 0 for all j > i_0. By d), we have r_{P, j} = \iota_{P, j} = 1 for all j > i_0, and the sequence (\alpha_{P, j})_{j > i_0} is non-increasing, hence eventually constant. Let i_1 > i_0 with \alpha_{P, i_1} = \alpha_{P, j} for all j > i_1. For k \in \mathbb{N}, we have a_{P, i_1} = E_{\alpha_{P, i_1} k} a_{P, i_1 + k} so a_{P, i_1} \in \bigcap_{k \in \mathbb{N}} E_{\alpha_{P, i_1} k} \mathbf{Mo}_{\alpha_{P, i_1}} = \mathbf{Mo}_{\alpha_{P, i_1} \omega}. Therefore E_{\alpha_{P, i_1}}^{a_{P, i_1 + 1}} is L_{< \alpha_{P, i_1 + 1} \omega}-atomic: a contradiction. We deduce that e) holds as well.

Let us prove the lemma by induction on i. The result clearly holds for i = 0. Assuming that a_{; i} is well defined, let j > i be minimal such that \varphi_j \neq 0 or \psi_j \neq 0. Note that we have \alpha_i \geqslant \alpha_{i + 1} \geqslant \cdots \geqslant \alpha_j, so E_{\alpha_i} \circ E_{\alpha_{i + 1}} \circ \cdots \circ E_{\alpha_j} = E_{\gamma} where \gamma = \alpha_i + \alpha_{i + 1} + \cdots + {\nobreak} \alpha_j. Applying \Phi_{; i} to the inequality

we obtain

Now if \varphi_j \neq 0, then

wso the number z := \sigma_{; i} \frac{a_{; i} - \varphi_i}{\varepsilon_i} satisfies

Both in the cases when \sigma_{; i} = 1 and when \sigma_{; i} = - 1, it follows that the number ((a_{; i} - \varphi_i) / \varepsilon_i \mathrm{e}^{\psi_i})^{\iota_i} is bounded from below by the hyperexponential E_{\gamma} of a number. Thus a_{; j} = L_{\gamma} (((a_{; i} - \varphi_i) / (\varepsilon_i \mathrm{e}^{\psi_i}))^{\iota_i}) is well defined and so is each a_{; k} for i \leqslant k < j. If \varphi_j = 0, then we have \psi_j \neq 0 and

Hence

Both in the cases when \varepsilon_i = 1 and when \varepsilon_i = - 1, it follows that ((a_{; i} - \varphi_i) / \varepsilon_i \mathrm{e}^{\psi_i})^{\iota_i} is bounded from below by the hyperexponential E_{\gamma} of a number, so a_{; j} is well defined and so is each a_{; k} for i \leqslant k < j.

Let a \in \mathbf{Ad} \cup (L|R) and let i \in \mathbb{N}. We have a_{; i} \in \mathbf{No}^{>, \succ}. If \sigma_{; i} = 1, then \Phi_{i ;} is strictly increasing so we have

If \sigma_{; i} = - 1, then \Phi_{i ;} is strictly decreasing and likewise we obtain L_{i ;} < a < R_{i ;} \Longleftrightarrow \varphi_i \trianglelefteqslant a_{; i}.

We have \iota_i \log E_{\alpha_i} a_{; i + 1} = \iota_i \left( \log \frac{a_{; i} - \varphi_i}{\varepsilon_i \mathrm{e}^{\psi_i}} \right). If \sigma_{; i} = 1, then \Phi_{i ;} is strictly increasing so we have

Likewise, we have L_i^{[2]} < a < R_i^{[2]} \Longleftrightarrow \log E_{\alpha_i} a_{; i + 1} \prec \ensuremath{\operatorname{supp}} \psi_i if \sigma_{; i} = - 1.

Assume that \varphi_{i + 1} \neq 0 and \sigma_{; i + 1} = 1. If \varepsilon_{i + 1} = 1, then we have a_{; i + 1} > \varphi_{i + 1}. Hence

If \varepsilon_{i + 1} = - 1, then we have a_{; i + 1} > \varphi_{i + 1}, whence

Symmetric arguments apply when \varphi_{i + 1} \neq 0 and \sigma_{; i + 1} = - 1.

We deduce by definition of \mathbf{Ad} that \mathbf{Ad} = \bigcap_{i \in \mathbb{N}} (L_i |R_i) = (L|R).

For x, y \in \mathbf{No}^{\neq}, we write x \equiv y if x \asymp y and x and y have the same sign. Let us prove by induction on i \in \mathbb{N} that b_{; i} is defined and that a_{; i} - \varphi_i \equiv b_{; i} - \varphi_i. Since this implies that \varphi_i \trianglelefteqslant b_{; i}, that \log \frac{b_{; i} - \varphi_i}{\varepsilon_i \mathrm{e}^{\psi_i}} \prec \ensuremath{\operatorname{supp}} \psi_i, and that \varphi_i \vartriangleleft \sharp_{\alpha_{i - 1}} (b_{; i}) if i > 0, this will yield b \in \mathbf{Ad}.

The result follows from our hypothesis if i = 0. Assume now that a_{; i} - \varphi_i \equiv b_{; i} - \varphi_i and let us prove that a_{; i + 1} - \varphi_{i + 1} \equiv b_{; i + 1} - \varphi_{i + 1}. Let

We have c_i \equiv \left( \frac{a_{; i} - \varphi_i}{\varepsilon_i \mathrm{e}^{\psi_i}} \right)^{\iota_i} = E_{\alpha_i} a_{; i + 1} \in \mathbf{No}^{>, \succ}, so b_{; i + 1} = L_{\alpha_i} (c_i) is defined. Moreover c_i \in \mathcal{E}_{\alpha_i} [E_{\alpha_i} a_{; i + 1}] so b_{; i + 1} \in \mathcal{L}_{\alpha_i} [a_{; i + 1}]. Since \varphi_{i + 1} \vartriangleleft \sharp_{\alpha_i} (a_{; i + 1}) = \sharp_{\alpha_i} (b_{; i + 1}), we deduce that {b_{; i + 1} - \varphi_{i + 1}} \sim a_{; i + 1} - \varphi_{i + 1}, whence in particular b_{; i + 1} - \varphi_{i + 1} \equiv a_{; i + 1} - \varphi_{i + 1}. This concludes the proof.

For b \in \mathbf{Ad}_{\nearrow 1}, and c \in \mathcal{L}_{\alpha_0} [b], we have \varphi_1 \vartriangleleft \sharp_{\alpha_0} (b) = \sharp_{\alpha_0} (c) so c - \varphi_1 \sim b - \varphi_1. We conclude with the previous lemma.

Let j > i be minimal with \varphi_j \neq 0 or \psi_j \neq 0. We thus have a_{; j}, b_{; j} \in \mathcal{P} [\varphi_j \mathbin{+\!\!\!\!+} \varepsilon_j \mathrm{e}^{\psi_j}] so \log a_{; j} \prec b_{; j}. We have a_{; i} = E_{\alpha_i + \cdots + \alpha_{j - 1}} a_{; j} and b_{; i} = E_{\alpha_i + \cdots + \alpha_{j - 1}} b_{; j} where \alpha_i \geqslant \cdots \geqslant \alpha_j \geqslant 1. We deduce by induction using Lemma 5.27 that L_{\alpha_{i - 1}} a_{; i} <\mathcal{E}_{\alpha_{i - 1}} b_{; i}.

Recall that \sharp_1 (b) = b_{\succ}. By Corollary 6.8, we have \sharp_{\alpha_0} (b) \in \mathbf{Ad}_{\nearrow 1},. So we may assume without loss of generality that b = \sharp_{\alpha_0} (b).

We claim that E_{\alpha_0}^b \in \mathbf{Mo}_{\alpha_0} \setminus L_{< \alpha_0} \mathbf{Mo}_{\alpha_0 \omega}. Assume for contradiction that E_{\alpha_0}^b \in L_{< \alpha_0} \mathbf{Mo}_{\alpha_0 \omega} and write E_{\alpha_0}^b = L_{\gamma} \mathfrak{a} accordingly. Then Corollary 5.6 implies that \gamma = 0, in which case we define n := 0, or \alpha_0 = \omega^{\mu + 1} for some ordinal \mu and \gamma = (\alpha_0)_{/ \omega} n for some n \in \mathbb{N}^{>}. Therefore E_{\alpha_0}^{b + n} \in \mathbf{Mo}_{\alpha_0 \omega}, so {b + n} \in \mathbf{Mo}_{\alpha_0 \omega}. This implies that

Recall that \varphi_1 \vartriangleleft b. Assume that n = 0, so \varphi_1 = 0. Since b is \log-atomic, we also have \psi_1 = 0. Let j > 1 be minimal with \varphi_j \neq 0 or \psi_j \neq 0. We have \alpha_1 \geqslant \cdots \geqslant \alpha_{j - 1} and b_{1 ; j} = L_{\alpha_1 + \cdots + \alpha_{j - 1}} b \in \mathbf{Mo}_{\alpha_{j - 1} \omega}. In particular, the number b_{1 ; j} is log-atomic. If \varphi_j \neq 0, this contradicts the fact that \varphi_j \vartriangleleft b_{1 ; j}. If \psi_j \neq 0, then \ensuremath{\operatorname{supp}} \psi_j \succ \log ((b_{1 ; j} \mathrm{e}^{- \psi_j})^{\iota_j}) implies

But then \log b_{1 ; j} is not a monomial: a contradiction. Assume now that n > 0. So \varphi_1 = b + n and b = \varphi_1 \mathbin{+\!\!\!\!+} (- n). But then b_{1 ; 2} is not defined: a contradiction. We conclude that E_{\alpha_0}^b \not\in L_{< \alpha_0} \mathbf{Mo}_{\alpha_0 \omega}.

If \alpha_0 > 1, or if \alpha_0 = 1 and b is not tail-atomic, then our claim yields the result. Assume now that \alpha_0 = 1 and that b = \psi \mathbin{+\!\!\!\!+} \iota \mathfrak{b} is tail-atomic where \iota \in \{ - 1, 1 \}, \psi \in \mathbf{No}_{\succ}, and \mathrm{e}^{\mathfrak{b}} = L_{\beta} E_{\alpha}^u \in \mathbf{Mo}_{\omega} is a hyperserial expansion. Then the hyperserial expansion of \exp b is \exp b = \mathrm{e}^{\psi} (L_{\beta} E_{\alpha}^u)^{\iota}.

We next show that \psi \in \mathbf{Ad}_{\nearrow 1}. If \mathfrak{b} \not\in \mathrm{e}^{\psi_1} (E_{\alpha_1} \mathbf{Ad}_{\nearrow 2})^{\iota_1}, then \varphi_1 \vartriangleleft \psi, and we conclude with Lemma 6.7 that \psi \in \mathbf{Ad}_{\nearrow 1}. Assume for contradiction that \mathfrak{b} \in \mathrm{e}^{\psi_1} (E_{\alpha_1} \mathbf{Ad}_{\nearrow 2})^{\iota_1}. Since \mathfrak{b} is log-atomic, we must have \psi_1 = 0. By the definition of coding sequences, this implies that \iota_1 = 1 and \alpha_1 = 1. So b = \varphi_1 \mathbin{+\!\!\!\!+} \varepsilon_1 \exp (b_{1 ; 2}), whence \psi = \varphi_1, \iota = \varepsilon_1, and \mathfrak{b}= \exp (b_{1 ; 2}). In particular the number b_{1 ; 2} is \log-atomic, hence tail-atomic. Since b_{1 ; 2} \in \mathbf{Ad}_{\nearrow 2}, the claim in the second paragraph of the proof, applied to \Sigma_{\nearrow 1}, gives E_1^{b_{1 ; 2}} \not\in \mathbf{Mo}_{\omega}. But then also \mathfrak{b} \not\in \mathbf{Mo}_{\omega}: a contradiction.

By Lemma 5.16, it is enough to find such a path in E_{\alpha_0} a_{; 1}. Write \alpha_0 =: \omega^{\mu}. Assume first that \mu = 0, so \alpha_0 = 1 and \psi_0 = 0. If (a_{; 1})_{\succ} is not tail-atomic, then the hyperserial expansion of \exp (a_{; 1})_{\succ} is \exp (a_{; 1})_{\succ} = E_1^{\smash{(a_{; 1})_{\succ}}} and rE_1^{\smash{(a_{; 1})_{\succ}}} is the dominant term of \exp a_{; 1} for some r \in \mathbb{R}^{\neq}. Then the path P with | P | = 1 and \tau_{P, 0} := rE_1^{\smash{(a_{; 1})_{\succ}}} satisfies u_{P, | P |} = (a_{; 1})_{\succ} \in \mathbf{Ad}_{\nearrow 1}. If (a_{; 1})_{\succ} is tail-atomic, then there exist \psi \in \mathbf{Ad}_{\nearrow 1}, \iota \in \{ - 1, 1 \} and \mathfrak{a} \in \mathbf{Mo}_{\omega} such that the hyperserial expansion of \exp (a_{; 1})_{\succ} is \exp (a_{; 1})_{\succ} = \mathrm{e}^{\psi} \mathfrak{a}^{\iota}. Let r \mathrm{e}^{\psi} \mathfrak{a}^{\iota} be a term in \exp a_{; 1} with r \in \mathbb{R}^{\neq}. Then the path P with | P | = 1 and P (0) := r \mathrm{e}^{\psi} \mathfrak{a}^{\iota} satisfies \psi_{P, | P |} = \psi \in \mathbf{Ad}_{\nearrow 1} -\mathbb{N}.

Assume now that \mu > 0. In view of (?), we recall that there are an ordinal \lambda < \alpha_0 and a number \delta with

If \mu is a limit ordinal, then by Lemma 6.12, we have a hyperserial expansion \mathfrak{m} := L_{\lambda} E_{\alpha_0}^{\smash{\sharp_{\alpha_0} (a_{; 1})}}. Let \tau \in \ensuremath{\operatorname{term}} \sharp_{\alpha_0} (a_{; 1}) and set Q (0) =\mathfrak{m} and Q (1) := \tau, so that Q is a path in \mathfrak{m}. By Lemma 5.15, there is a subpath in E_{\alpha_0} a_{; 1}, hence also a path P in E_{\alpha_0} a_{; 1}, with \tau_{P, | P | - 1} =\mathfrak{m}. So u_{P, | P |} = \sharp_{\alpha_0} (a_{; 1}) \in \mathbf{Ad}_{\nearrow 1}. If \mu is a successor ordinal, then we may choose \lambda = \omega^{\mu_-} n for a certain n \in \mathbb{N}. By Lemma 6.12, we have a hyperserial expansion \mathfrak{m} := E_{\alpha_0}^{\smash{\sharp_{\alpha_0} (a_{; 1}) - n}}. As in the previous case, there is a path P in E_{\alpha_0} a_{; 1} with \tau_{P, | P |} =\mathfrak{m}, whence u_{P, | P |} = \sharp_{\alpha_0} (a_{; 1}) - n \in \mathbf{Ad}_{\nearrow 1} -\mathbb{N}.

This is immediate if k = 0. Assume that the result holds at k and pick a corresponding path P with u_{P, | P |} \in \mathbf{Ad}_{\nearrow k} -\mathbb{N} (resp. \psi_{P, | P |} \in \mathbf{Ad}_{\nearrow k} -\mathbb{N}). Note that the dominant term \tau of u_{P, | P |} - \varphi_k (resp. \psi_{P, | P |} - \varphi_k) lies in \varepsilon_k \mathrm{e}^{\psi_k} (E_{\alpha_k} \mathbf{Ad}_{\nearrow k + 1})^{\iota_k} by Lemma 6.7. Moreover \tau is a term of u_{P, | P |} (resp. \psi_{P, | P |}). By the previous lemma, there is a path Q in \tau with u_{Q, | Q |} \in \mathbf{Ad}_{\nearrow k + 1} -\mathbb{N} or \psi_{Q, | Q |} \in \mathbf{Ad}_{\nearrow k + 1} -\mathbb{N}, so (P (0), \ldots, P (| P | - 1), Q (0)) \ast Q satisfies the conditions.

Assume for contradiction that this is not the case. This means that the set \Delta of indices d \in \mathbb{N} such that \mathbf{Ad}_{\nearrow d} \neq \varphi_d + \varepsilon_d \mathrm{e}^{\psi_d} (E_{\alpha_d} \mathbf{Ad}_{\nearrow d + 1})^{\iota_d} is infinite. We write \Delta = \{ d_i : i \in \mathbb{N} \} where d_0 < d_1 < \cdots. Fix a \in \mathbf{Ad} and let d := d_i \in \Delta. Let u \in \mathbf{Ad}_{\nearrow d + 1} such that

let n \in \mathbb{N} and let P be any finite path with

We claim that we can extend P to a path Q with | Q | > | P |, u_{Q, | Q |} \in \mathbf{Ad}_{\nearrow d_{i + 3}} -\mathbb{N} and such that | P | is a bad index in Q. Indeed, in view of Definition 6.4 for \mathbf{Ad}_{\nearrow d}, the relation (Proof) translates into the following three possibilities:

Consider a b \in \mathbf{Ad}_{\nearrow d_1 - 1} and the path P_0 := \left( \tau_{a - \varphi_{d_0}} \right) in b. So P is a finite path with u_{P_0, | P_0 |} \in \mathbf{Ad}_{\nearrow d_1}. Thus there exists a path P_1 which extends P_0 with u_{P_1, | P_1 |} \in \mathbf{Ad}_{\nearrow d_3}, where | P_0 | is a bad index in P. Repeating this process iteratively for i = 2, 3, \ldots, we construct a path P_i that extends P_{i - 1} and such that u_{P_i, | P_i |} \in \mathbf{Ad}_{\nearrow d_{2 i + 1}} and such that | P_{i - 1} | is a bad index in P_i. At the limit, this yields an infinite path Q in a that extends each of the paths P_i. This path Q has a cofinal set of bad indices, which contradicts Theorem 1.1. We conclude that there is a k \in \mathbb{N} such that \Sigma_{\nearrow k} is nested.

Note that \mathcal{E}_{\alpha_0} [E_{\alpha_0} \mathbf{Ad}_{\nearrow 1}] = E_{\alpha_0} \mathcal{L}_{\alpha_0} [\mathbf{Ad}_{\nearrow 1}]. The result thus follows from Corollary 6.8 and the assumption that \Sigma is nested.

The proof is similar to the proof of Lemma 5.30. We have a_{; k} = \varphi_k \mathbin{+\!\!\!\!+} \varepsilon_k \mathrm{e}^{\psi_k} (E_{\alpha_k} a_{; k + 1})^{\iota_k} and we must have \ensuremath{\operatorname{supp}} \psi_k \succ \log \mathfrak{p} since c_k = \varphi_k \mathbin{+\!\!\!\!+} \varepsilon_k \mathrm{e}^{\psi_k} \mathfrak{p}^{\iota_k} \in \mathbf{Ad}_{\nearrow k}. If follows from the deconstruction lemmas in ? that c_k \sqsubseteq a_{; k}. This proves the result in the case when k = 0.

Now assume that k > 0. Setting c_{k - p} := \Phi_{k - p ; k} (c_k), let us prove by induction on p \leqslant k that

For p = k, the last relation yields the desired result.

If p = 0, then we have c_k \in \mathbf{Ad}_{\nearrow k} by assumption and we have shown above that c_k \sqsubseteq a_{; k}. We have \varphi_k \vartriangleleft \sharp_{\alpha_{k - 1}} (c_k) and \mathrm{e}^{\psi_k} \mathfrak{p}^{\iota_j} is a monomial, so (6.17) yields c_k = \sharp_{\alpha_{k - 1}} (c_k) \in \mathbf{No}_{\succ, \alpha_{k - 1}}. This deals with the case p = 0. In addition, we have c_k > 0 because k > 0 and c_k \in \mathbf{Ad}_{\nearrow k}. Let us show that

If \varphi_k \neq 0, then this follows from the facts that \varphi_k \vartriangleleft a_{; k} and \varphi_k \vartriangleleft c_k. If \varphi_k = 0 and \psi_k \neq 0, then \log (c_k / \varepsilon_k) \sim \psi_k \sim \log (a_{; k} / \varepsilon_k) \prec a_{; k}. If \varphi_k = \psi_k = 0, then a_{; k} = E_{\alpha_k} a_{; k + 1} and c_k =\mathfrak{p} \in \mathcal{E}_{\omega} [a_{; k}], so \log c_k \prec a_{; k}.

Assume now that 0 < p \leqslant k and that the induction hypothesis holds for all smaller p. We have

Since \Sigma is nested, we immediately obtain \varphi_{k - p} \vartriangleleft \sharp_{\alpha_{k - p - 1}} (c_{k - p}), whence c_{k - p} \in \mathbf{No}_{\succ, \alpha_{k - p - 1}} as above. Since c_{k - p - 1} \in \mathbf{Ad}_{\nearrow (k - p - 1)} and \Sigma is nested, we have c_{k - p} \in \mathbf{Ad}_{\nearrow (k - p)}. Using (?), (?), and the decomposition lemmas, we observe that the relation c_{k - p} \sqsubseteq a_{; k - p} is equivalent to

We have c_{k - p + 1} \sqsubseteq a_{; k - p + 1}, so c_{k - p + 1} \sqsubseteq \sharp_{\alpha_{k - p}} (a_{; k - p + 1}). Note that

So it is enough, in order to derive ?, to prove that E_{\alpha_{k - p}}^{\smash{c_{k - p + 1}}} \sqsubseteq E_{\alpha_{k - p}}^{\smash{\sharp_{\alpha_{k - p}} (a_{; k - p + 1})}}. Now

by Lemma 6.9, whence E_{\alpha_{k - p}}^{\smash{c_{k - p + 1}}} \sqsubseteq E_{\alpha_{k - p}}^{\smash{\sharp_{\alpha_{k - p}} (a_{; k - p + 1})}} by Lemma 5.25.

It is enough to prove the result for j = i + 1. Assume that \sigma_{i + 2 ; i + 1} = 1. Let a \in \mathbf{Ad} and set a' := (\Psi_{i + 1, H_2} (a))_{i + 1 ;}, so that

Note that

If \sigma_{; i + 1} = 1, then \varepsilon_{i + 1} \iota_{i + 1} = \sigma_{; i + 2} / \sigma_{; i + 1} = 1 and \Psi_{; i + 1} is strictly increasing. So we only need to prove that \mathcal{T}_{\alpha_i} [a_{; i + 1}] < a', which reduces to proving that \sharp_{\alpha_i} (a_{; i + 1}) < \sharp_{\alpha_i} (a'). Let \tau be the dominant term of E_{\alpha_{i + 1}} a_{; i + 2}. Our assumption that \Sigma is nested gives \varphi_i + \varepsilon_i \mathrm{e}^{\psi_i} (E_{\alpha_i} a')^{\iota_i} \in \mathbf{Ad}_{\nearrow i}, whence \varphi_{i + 1} \vartriangleleft \sharp_{\alpha_i} (a'). We deduce that \varphi_{i + 1} + \varepsilon_{i + 1} \mathrm{e}^{\psi_{i + 1}} (2 \tau)^{\iota_{i + 1}} \trianglelefteqslant \sharp_{\alpha_i} (a'). Lemma 5.26 implies that \varphi_{i + 1} + \varepsilon_{i + 1} \mathrm{e}^{\psi_{i + 1}} (2 \tau)^{\iota_{i + 1}} is \alpha_i-truncated.

and \varepsilon_{i + 1} \iota_{i + 1} = 1 implies that

is a strictly positive term. We deduce that \sharp_{\alpha_i} (a_{; i + 1}) - \varphi_{i + 1} < \sharp_{\alpha_i} (a') - \varphi_{i + 1}, whence \sharp_{\alpha_i} (a_{; i + 1}) < \sharp_{\alpha_i} (a'). The other cases when \sigma_{; i + 1} = - 1 or when \sigma_{i + 2 ; i + 1} = - 1 are proved similarly, using symmetric arguments.

By Proposition 4.1, the class \mathbf{Smp}_{\mathcal{G}} is a surreal substructure, so it is enough to prove the equality. We first prove that \mathbf{Smp}_{\mathcal{G}} \subseteq \mathbf{Ne}.

Assume for contradiction that there are an a \in \mathbf{Smp}_{\mathcal{G}} and a k \in \mathbb{N}, which we choose minimal, such that a_{; k} cannot be written as a_{; k} = \varphi_k \mathbin{+\!\!\!\!+} \varepsilon_k \mathfrak{m}_k where \mathfrak{m}_k = \mathrm{e}^{\psi_k} (E_{\alpha_k}^{a_{; k + 1}})^{\iota_k} is a hyperserial expansion. Set \mathfrak{m} := \mathfrak{d}_{a_{; k} - \varphi_k}, r := (a_{; k})_{\mathfrak{m}} and \delta := (a_{; k})_{\succ \mathfrak{m}}.

Our goal is to prove that there is a number m \in \{ k, k + 1 \} and \mathfrak{p} \in \mathbf{Mo}^{\succ} with

Assume that this is proved and set c_m := \varphi_m + \varepsilon_m \mathrm{e}^{\psi_m} \mathfrak{p}^{\iota_m}. The first condition and Lemma 6.16 yield c_m \in \mathbf{Ad}_{\nearrow m} and the relations \log \mathfrak{p} \prec \ensuremath{\operatorname{supp}} \psi_m and \mathrm{e}^{\psi_m} \mathfrak{p}^{\iota_m} \prec \ensuremath{\operatorname{supp}} \varphi_m. The second and third condition, together with Lemma 6.17, imply c := (c_m)_{m ;} \sqsubset a. The first condition also implies that c \in \mathcal{G} [a]: a contradiction. Proving the existence of m and \mathfrak{p} is therefore sufficient.

If \mathfrak{m} \neq \min \ensuremath{\operatorname{supp}} a_{; k} or \mathfrak{m}= \min \ensuremath{\operatorname{supp}} a_{; k} and r \not\in \{ - 1, 1 \}, then m := k and \mathfrak{p} := \mathfrak{d}_{E_{\alpha_k} a_{; k + 1}} satisfy (?). Assume now that \mathfrak{m}= \min \ensuremath{\operatorname{supp}} a_{; k} and that r \in \{ - 1, 1 \}, whence r = \varepsilon_k. If a_{; k + 1} \not\in \mathbf{No}_{\succ, \alpha_k} then m := k and \mathfrak{p} := E_{\alpha_k}^{\smash{\sharp_{\alpha_k} (a_{; k + 1})}} satisfy (?). Assume therefore that a_{; k + 1} \in \mathbf{No}_{\succ, \alpha_k}. This implies that there exist \gamma < \alpha_k and \mathfrak{a} \in \mathbf{Mo}_{\alpha_k \omega} with E_{\alpha_k}^{\smash{a_{; k + 1}}} = L_{\gamma} \mathfrak{a}. By the definition of coding sequences, there is a least index j > k with \varphi_j \neq 0 or \psi_j \neq 0, so

We have \mathfrak{a} \in \mathbf{Mo}_{\alpha_k \omega} and L_{\gamma} \mathfrak{a} \in \mathbf{Mo}_{\alpha_k} \setminus \mathbf{Mo}_{\alpha_k \omega}. So by Corollary 5.6, we must have \alpha_k = \omega^{\mu + 1} for a certain \mu \in \mathbf{On} and \gamma = (\alpha_k)_{/ \omega} n for a certain n \in \mathbb{N}^{>}. Note that a_{; k + 1} = L_{\alpha_k} \mathfrak{a}- n. Recall that \varphi_{k + 1} \vartriangleleft a_{; k + 1} and L_{\alpha_k} \mathfrak{a} \in \mathbf{Mo}^{\succ}, so \varphi_{k + 1} \in \{ L_{\alpha_k} \mathfrak{a}, 0 \}. The case \varphi_{k + 1} = L_{\alpha_k} \mathfrak{a} cannot occur for otherwise

would not lie in \mathbf{No}^{>, \succ}. So \varphi_{k + 1} = 0. Let m := k + 1 and

We have \mathfrak{p} \in \mathcal{E}_{\alpha_{k + 1}} [E_{\alpha_{k + 1}} a_{; k + 2}] and \mathfrak{p} \sqsubset E_{\alpha_{k + 1}} a_{; k + 2}, so m and \mathfrak{p} satisfy (?). We deduce that \mathbf{Smp}_{\mathcal{G}} is a subclass of \mathbf{Ne}.

Conversely, consider b \in \mathbf{Ne} and set c := \pi_{\mathcal{G}} [b]. So there are i_1, i_2 \in \mathbb{N} and (g, h) \in \mathcal{E}_{\alpha_{i_1}}' \times \mathcal{E}_{\alpha_{i_2}}' with \Psi_{i_1, g_1} (b) < c < \Psi_{i_2, g_2} (b). Let i := \max (i_1 + 1, i_2 + 1). By Lemma 6.18, there exist d_1, d_2 \in \left\{ 1 / 2, 2 \right\} with \Psi_{i_1, g_1} < \Psi_{i, H_{d_1}} and \Psi_{i_2, g_2} < \Psi_{i, H_{d_2}}, whence \Psi_{i, H_{d_1^{- 1}}} (b) < c < \Psi_{i, H_{d_2}} (b). Since \Phi_{; i} is strictly monotonous, we get c_{; i} - \varphi_i \asymp b_{; i} - \varphi_i. The numbers \varepsilon_i (c_{; i} - \varphi_i) and \varepsilon_i (b_{; i} - \varphi_i) are monomials, so c_{; i} - \varphi_i = b_{; i} - \varphi_i. Therefore b = c \in \mathbf{Smp}_{\mathcal{G}}.

By [BvdH19, Lemma 4.5] and since the function \Phi_{i ;} is strictly monotonous, it is enough to prove that \forall a, b \in \mathbf{Ne}, a \sqsubseteq b \Longleftarrow a_{; i} \sqsubseteq b_{; i}. By induction, we may also restrict to the case when i = 1. So assume that a_{; 1} \sqsubseteq b_{; 1}. Recall that L_{\alpha_0} a_{; 1} \prec \mathcal{E}_{\alpha_0} b_{; 1} by Lemma 6.9. Since a_{; 1}, b_{; 1} \in \mathbf{No}_{\succ, \alpha_0}, we deduce with Lemma 5.25 that E_{\alpha_0}^{\smash{a_{; 1}}} \sqsubseteq E_{\alpha_0}^{\smash{b_{; 1}}}. It follows using the decomposition lemmas that a \sqsubseteq b.

We have \mathbf{Ne} \subseteq (\mathbf{Ne}_{\nearrow 1})_{1 ;} by definition of \mathbf{Ne}. So we only need to prove that (\mathbf{Ne}_{\nearrow 1})_{1 ;} \subseteq \mathbf{Ne}. Consider b \in \mathbf{Ne}_{\nearrow 1}. Since \Sigma is nested, the number a := \varphi_0 + \varepsilon_0 \mathrm{e}^{\psi_0} (E_{\alpha_0} b) is \Sigma-admissible, so we need only justify that E_{\alpha_0} b \in \mathbf{Mo}_{\alpha_0} \setminus L_{< \alpha_0} \mathbf{Mo}_{\alpha_0 \omega}. Since a is \Sigma-admissible, we have \varphi_1 \vartriangleleft \sharp_{\alpha_0} (b). But b is \Sigma_{\nearrow 1}-nested, so b = \varphi_1 \mathbin{+\!\!\!\!+} \tau for a certain term \tau. We deduce that b = \sharp_{\alpha_0} (b) \in \mathbf{No}_{\succ, \alpha_0}, whence E_{\alpha_0} b \in \mathbf{Mo}_{\alpha_0}.

Assume for contradiction that E_{\alpha_0}^b \in L_{< \alpha_0} \mathbf{Mo}_{\alpha_0 \omega} and write E_{\alpha_0}^b = L_{\gamma} \mathfrak{a} where \mathfrak{a} \in \mathbf{Mo}_{\alpha_0 \omega} and \gamma < \alpha_0. Note that \gamma \neq 0: otherwise \varphi_i and \psi_i would be zero for all i \geqslant 1, thereby contradicting Definition 6.1(?). By Corollary 5.6, we must have \alpha_0 = \omega^{\mu + 1} for a certain ordinal \mu and \gamma = \omega^{\mu} n for a certain n \in \mathbb{N}^{>}. Consequently, b = L_{\alpha_0} \mathfrak{a}- n \in \mathbf{Mo} - n. If \varphi_1 \neq 0, then the condition \varphi_1 \vartriangleleft \sharp_{\alpha_0} (b) implies \varphi_1 = b, which leads to the contradiction that b_{1 ; 2} = 0 \not\in \mathbf{No}^{>, \succ}. If \varphi_1 = 0, then \mathbf{Ne}_{\nearrow 1} \subseteq \varepsilon_1 \mathbf{Mo}, whence n = 0: a contradiction.

Assume that \psi_1 < 0, or \psi_1 = 0 and \iota_1 = - 1. In particular, if a is \Sigma-admissible, then a_{; 1} - \varphi_1 \prec 1, so a_{; 1} - \varphi_1 \prec \ensuremath{\operatorname{supp}} \varphi_1'. For b \in \mathbf{No}^{>, \succ}, it follows that E_{\alpha_0} (b - n) is \Sigma^{[n]}-admissible if and only if E_{\alpha_0} b is \Sigma-admissible. Let \mathbf{Ad}_{\nearrow i}' be the class of \Sigma'_{\nearrow i}-admissible numbers, for each i \in \mathbb{N}. We have L_{\beta n} \mathbf{Ad} = \mathbf{Ad}' by the previous remarks, and \Sigma' is admissible. For i > 1, we have \Sigma'_{\nearrow i} = \Sigma_{\nearrow i}, so

Moreover, \mathbf{Ad}'_{\nearrow 1} = \mathbf{Ad}_{\nearrow 1} - n, so

So \Sigma' is nested. We deduce that L_{\beta n} \mathbf{Ne} = \mathbf{Ne}', that is, we have a strictly increasing bijection L_{\beta n} : \mathbf{Ne} \longrightarrow \mathbf{Ne}'. It is enough to prove that for a, b \in \mathbf{Ne} with a \sqsubseteq b, we have L_{\beta n} a \sqsubseteq L_{\beta n} b. Proceeding by induction on n, we may assume without loss of generality that n = 1. By [vdH:hypno, identity (6.3)], the function L_{\beta} has the following equation on \mathbf{Mo}_{\alpha_0}:

So it is enough to prove that L_{\beta} b < a. Note that L_{\beta} b = E_{\alpha_0}^{b_{; 1} - 1} and a = E_{\alpha_0}^{a_{; 1}} where b_{; 1} - \varphi_1, a_{; 1} - \varphi_1 \prec 1. So b_{; 1} - a_{; 1} \prec 1, whence b_{; 1} - 1 < a_{; 1}. This concludes the proof.

This is straightforward, by applying the rules \mathbf{E1}–\mathbf{E7} recursively (from the leaves to the root in the case of (?) and the other way around for (?)).

Given n \in \mathbb{N}, we say that an \ensuremath{\boldsymbol{\Sigma}}^{\sharp}-labeled tree T is n-settled if \lambda_{\nu} \not\in \textrm{?}_{\mathbf{No}} for all nodes \nu \in N_T of height < n. Let us show how to construct a sequence (T_n)_{n \in \mathbb{N}} of \ensuremath{\boldsymbol{\Sigma}}^{\sharp}-labeled tree expansions of a such that the following statements hold for each n \in \mathbb{N}:

• S1 T_n is an n-settled and of finite height;

• S2 v_n (\rho_{T_n}) = a for some (necessarily unique) evaluation v_n : N_{T_n} \longrightarrow \mathbf{No} of T_n;

• S3 If n > 0, then T_n refines T_{n - 1};

• S4 If T is a tree expansion of a with labels in \ensuremath{\boldsymbol{\Sigma}}, then T refines T_n.

We will write \lambda_n : N_{T_n} \longrightarrow \ensuremath{\boldsymbol{\Sigma}}^{\sharp} for the labeling of T_n.

We take T_0 such that N_{T_0} = \{ \rho_{T_0} \} and \lambda_{\rho_{T_0}} = \textrm{?}_a. Setting v_0 (\rho_{T_0}) := a, the conditions \mathbf{S1}–\mathbf{S4} are naturally satisfied.

Assume now that T_n has been constructed and let us show how to construct T_{n + 1}. Let S be the subset of N_{T_n} of nodes \nu of level n with v_n (\nu) \in \textrm{?}_{\mathbf{No}}. Given \nu \in S, let T_{\nu} be the standard expansion of v_n (\nu) and let v_{\nu} be the unique evaluation of T_{\nu}. We define T_{n + 1} to be the tree that is obtained from T_n when replacing each node \nu \in S by the tree T_{\nu}.

Since each tree T_{\nu} is of height at most 6, the height of T_{n + 1} is finite. Since T_{n + 1} is clearly (n + 1)-settled, this proves \mathbf{S1}. We define an evaluation v_{n + 1} : N_{T_{n + 1}} \longrightarrow \ensuremath{\boldsymbol{\Sigma}}^{\sharp} by setting v_{n + 1} (\sigma) = {\nobreak} v_n (\sigma) for any \sigma \in N_{T_n} and v_{n + 1} (\sigma) = v_{\nu} (\sigma) for any \nu \in S and \sigma \in N_{T_{\nu}} (note that v_{n + 1} is well defined since v_{\nu} (\rho_{T_{\nu}}) = (\lambda_n)_{\nu} = {\nobreak} v_n (\nu) for all \nu \in S). We have v_{n + 1} (\rho_{T_{n + 1}}) = v_n (\rho_{T_n}) = a, so \mathbf{S2} holds for v_{n + 1}. By construction, N_{T_{n + 1}} \supseteq N_{T_n} and the evaluations v_n and v_{n + 1} coincide on N_{T_n}; this proves \mathbf{S3}. Finally, let T be a tree expansion of a with labels in \ensuremath{\boldsymbol{\Sigma}} and let v be the unique evaluation of T with v (\rho_T) = a. Then T refines T_n, so v coincides with v_n on N_{T_n}. Let \nu \in S. Since T is a tree expansion of a, the subtree T' of T with root \nu refines T_{\nu}, whence N_T \supseteq N_{T_{\nu}}. Moreover, v (\nu) = v_{n + 1} (\nu), so v coincides with v_{\nu} on T_{\nu}. Altogether, this shows that T refines T_{n + 1}.

Having completed the construction of our sequence, we next define a \ensuremath{\boldsymbol{\Sigma}}-labeled tree T_{\infty} and a map v_{\infty} : N_{T_{\infty}} \longrightarrow \mathbf{No} by taking N_{T_{\infty}} = \bigcup_{n \in \mathbb{N}} N_{T_n} and by setting (\lambda_{\infty})_{\nu} := (\lambda_n)_{\nu} and v_{\infty} (\nu) = v_n (\nu) for any n \in \mathbb{N} and \nu \in N_{T_n} such that (\lambda_n)_{\nu} \not\in \textrm{?}_{\mathbf{No}}. By construction, we have v_{\infty} (\rho_{T_{\infty}}) = a and T_{\infty} refines T_n for every n \in \mathbb{N}.

We claim that T_{\infty} is a tree expansion of a. Indeed, consider a node \nu \in N_{T_{\infty}} of height n with \lambda_{\nu} = \sum. Then \nu \in N_{T_{n + 1}} and (\lambda_{n + 1})_{\nu} = \sum, since T_{n + 1} is (n + 1)-settled. Consequently, the subtree of T_{n + 1} with root \nu refines the standard expansion of v_{n + 1} (\nu). Since T_{\infty} refines T_{n + 1}, it follows that the subtree of T_{\infty} with root \nu also refines the standard expansion of v_{\infty} (\nu) = v_{n + 1} (\nu). This completes the proof of our claim.

It remains to show that T_{\infty} is the unique tree expansion of a with labels in \ensuremath{\boldsymbol{\Sigma}}. So let T be any tree expansion of a with labeling \lambda : N_T \longrightarrow \ensuremath{\boldsymbol{\Sigma}}. For every n \in \mathbb{N}, it follows from \mathbf{S4} that N_T \supseteq N_{T_n}. Moreover, since T_n is n-settled, \lambda coincides with both \lambda_n and \lambda_{\infty} on those nodes in N_{T_n} that are of height < n. Consequently, N_T \supseteq N_{T_{\infty}} and \lambda coincides with \lambda_{\infty} on N_{T_{\infty}}. Since every node in N_T has finite height, we conclude that T = T_{\infty}.