1 Introduction

A difference field is a field equipped with a distinguished automorphism. The concept has derived from the study of functional equations like \(f(x+1)-f(x)=g(x)\), which are called difference equations. A valued difference field is a valued field equipped with a distinguished automorphism which fixes the valuation ring setwise. These structures have attracted attention after their relevance in [8] as a tool for analyzing difference varieties.

The results of Ax&Kochen and Ershov (see [10]) on valued fields have been very influential on the algebraic theory of valued fields and lead to an asymptotic solution of Artin’s conjecture that over the \(p\)-adics every homogeneous polynomial of degree \(d\) with more than \(d^2\) variables has a nontrivial zero.Footnote 1 Hence it is very natural to ask whether one can obtain analogs of these results in the context of valued difference fields. Most notably, in [4], Belair, Macintyre and Scanlon provide axiomatization and relative quantifier elimination for the field of Witt vectors over the algebraic closure of \(\mathbb {F}_p\) equipped with the lifting of the Frobenius automorphism. One of the key ingredients of these results is the study of zeroes of difference polynomials in one variable. This is purely algebraic in nature and may be seen as a first step toward the study of difference varieties in terms of valuation theory. The success of [4] inspired further research, and more results in the same direction were proved in [1, 2] and [12]. It is worth mentioning that these results were used in [5] to show that valued difference fields are concrete examples of NTP2 theories. The main results of this paper are again axiomatization and relative quantifier elimination for valued difference fields (see Sect. 7) but in a much more general context than the results mentioned above. In Sect. 8 we apply these results to the transseries field considered as a valued difference field with the automorphism that sends each element \(f(x)\) to \(f(x+1)\).

Let \(K\) be a valued difference field with valuation \(v\), valuation ring \(\mathcal {O}\) whose maximal ideal is \(\mathfrak {m}\), value group \(\varGamma \) and distinguished automorphism \(\sigma \). Then \(\sigma \) induces an automorphism of the residue field \({{\varvec{k}}}:=\mathcal {O}/\mathfrak {m}\), denoted \(\bar{\sigma }\). Likewise \(\sigma \) induces an order-preserving automorphism of the value group, which we also denote by \(\sigma \):

$$\begin{aligned} \gamma \mapsto \sigma (\gamma ):= v(\sigma (a))\quad \text {where}\quad v(a)=\gamma . \end{aligned}$$

Up to this point model theoretic results on valued difference fields are obtained in restricted settings determined by the action of \(\sigma \) on the value group. For example, in [4], \(\sigma \) is assumed to induce the identity map on \(\varGamma \). In general the action of \(\sigma \) on \(\varGamma \) can be quite complicated (see Hahn difference fields in Sect. 2 and also Sect. 8). Our key improvement in this paper is omitting all assumptions about the action of \(\sigma \) on the value group except what is already implied by requiring that it fixes the valuation ring setwise. This is achieved via generalizing and unifying various techniques from the aforementioned results. The notion of regularity from the PhD thesis of the second author [11] (also used in [12] independently) turns out to be a very efficient tool for understanding the interaction between pseudoCauchy sequences and \(\sigma \)-polynomials (see Sect. 3).

For the main content of this paper we need the results of Sect. 3 only for \(\sigma \)-polynomials in one variable, but we also present straightforward generalizations to the multivariable setting at the end of Sect. 3. These results are very much in the spirit of tropical geometry, and we hope that they will find applications in the study of difference varieties. Indeed we provide a straightforward proof of Kapranov’s Theorem as a consequence (see Theorem 3.13). A tropical approach to difference geometry with the tools introduced here also seems within reach, but this is a separate goal to be pursued elaborately in further research.

Henselianity plays a crucial role in [10] and all similar results about the elementary theory of valued fields. There are various attempts for a suitable definition of \(\sigma \)-henselianity to fulfill that role in valued difference fields. The one we use (see Definition 4.5) was introduced in [1]. It was initially intended to deal with contractive valued difference fields,Footnote 2 but in Sect. 4 we show that this notion of \(\sigma \)-henselianity is suitable for the general setting as well. It is worth noting that \(\sigma \)-henselianity implies that the residue difference field is linear difference closed. That is, if \(K\) is a \(\sigma \)-henselian valued difference field as in Definition 4.5, then for all \(\alpha _0, \ldots , \alpha _n \in {{\varvec{k}}}\) with \(\alpha _i \ne 0\) for some \(i\), the equation

$$\begin{aligned} 1+\alpha _0x+\alpha _1\bar{\sigma }(x)+\cdots +\alpha _n\bar{\sigma }^n(x)=0 \end{aligned}$$

has a solution in \({{\varvec{k}}}\) (see Lemma 4.6). In particular our results in Sect. 7 do not apply when \(\bar{\sigma }\) is the identity on the residue field. Let us note that this restriction is present in each of [1, 4, 12].

In Sect. 8 we apply our results to transseries. Transseries, also referred to as LE-series, present themselves in real differential algebra as real closed differential fields (see [13]). Moreover there is a lot of additional structure on transseries: exponentiation, valuation, composition and integration. We will be considering a transseries field, \(\mathbb T\), as a valued field equipped with a right composition map. If \(g(x)\) is a positive, infinite transseries, then the map given by \(f(x) \mapsto f(g(x))\) is an automorphism of \(\mathbb T\) and it fixes the valuation ring setwise. As such \(\mathbb T\) becomes a valued difference field. One natural choice for \(g(x)\) as above is \(g(x)=x+1\). Let us note that in this case the automorphism is neither value-preserving, nor contractive, nor multiplicative; the cases considered in [1, 4, 12], respectively. Unfortunately, the residue field of the natural valuation on \(\mathbb T\) is really closed. In particular, the residue difference field is not linear difference closed. However, when \(g(x)=x+1\), we can pass to a coarsening of the natural valuation whose residue difference field is linear difference closed and then apply the results of Sect. 7. This trick can not be applied for an arbitrary \(g(x)\). In the particularly interesting case \(g(x)=e^x\), the linear difference equation

$$\begin{aligned} f(e^x)-f(x)=1 \end{aligned}$$

does not have a solution in \(\mathbb T\) and worse the reduced equation does not have a solution in the residue difference field of any coarsening.

We would like to thank Lou van den Dries and Joris van der Hoeven for the help they provided in issues concerning transseries. Part of this research was conducted at Nesin Mathematics Village, we are thankful for their hospitality.

2 Preliminaries

Throughout, \(\mathbb {N}=\{0,1,2,\ldots \}\), and \(m,n\) range over \(\mathbb {N}\). We let \(K^\times =K{\setminus } \{0\}\) be the multiplicative group of a field \(K\). Some of the basic concepts we use are introduced below. For the rest (difference fields, \(\sigma \)-polynomials and their Taylor expansions, valued fields, etc.) we follow the notations and conventions given in the preliminaries section of [2].

Ordered difference groups An ordered difference group is an ordered abelian group equipped with a distinguished order-preserving automorphism. We consider an ordered difference group in the obvious way as a structure for the language \(\{ 0, +, -, <, \sigma \}\), where the unary function symbol \(\sigma \) is interpreted as the distinguished automorphism. Let \(\varDelta \subseteq \varGamma \) be an extension of ordered difference groups, and \(\gamma \in \varGamma \). We define \(\varDelta \langle \gamma \rangle \) to be the smallest ordered difference subgroup of \(\varGamma \) containing \(\varDelta \) and \(\gamma \). For \({\varvec{i}}=(i_0, \ldots , i_n) \in \mathbb {Z}^{n+1}\) we put

$$\begin{aligned} {\varvec{\sigma }}^{{\varvec{i}}}(\gamma ):= \sum _{k=0}^n i_k \sigma ^k(\gamma ). \end{aligned}$$

Consider the polynomial ring \(\mathbb {Z}[\sigma ]\) where \(\sigma \) is taken as an indeterminate. We construe the ordered difference group \(\varGamma \) as a \(\mathbb {Z}[\sigma ]\)-module as follows: for

$$\begin{aligned} \tau =\sum _{k=0}^{n}i_k\sigma ^k \in \mathbb {Z}[\sigma ], \quad \gamma \in \varGamma , \end{aligned}$$

we set \(\tau (\gamma ):={\varvec{\sigma }}^{{\varvec{i}}}(\gamma )\) where \({\varvec{i}}=(i_0, \ldots , i_n) \in \mathbb {Z}^{n+1}\). We also consider each ordered difference subgroup of \(\varGamma \) as a \(\mathbb {Z}[\sigma ]\)-submodule of \(\varGamma \).

Valued difference fields A valued difference field is a valued field \(\mathcal {K}=(K, \varGamma , {{\varvec{k}}}; v,\pi )\) where \(K\) is not just a field, but a difference field whose difference operator \(\sigma \) satisfies \(\sigma (\mathcal {O}_v)= \mathcal {O}_v\). It follows that \(\sigma \) induces an automorphism of the residue field:

$$\begin{aligned} \pi (a) \mapsto \pi (\sigma (a)):\ {{\varvec{k}}}\rightarrow {{\varvec{k}}}, \quad a \in \mathcal {O}. \end{aligned}$$

We denote this automorphism by \(\bar{\sigma }\), and \({{\varvec{k}}}\) equipped with \(\bar{\sigma }\) is called the residue difference field of \(\mathcal {K}\). Likewise \(\sigma \) induces an order-preserving automorphism of the value group \(\varGamma \), which we also denote by \(\sigma \). Furthermore

$$\begin{aligned} v({\varvec{\sigma }}(y)^{{\varvec{i}}})={\varvec{\sigma }}^{{\varvec{i}}}(\gamma ) \end{aligned}$$

for all \(y\in K^{\times }\) with \(v(y)=\gamma \) and \({\varvec{\sigma }}(y)^{{\varvec{i}}}=y^{i_0}\cdots \sigma ^n(y)^{i_n}\). Hence \(v:K^{\times } \rightarrow \varGamma \) is a morphism of \(\mathbb {Z}[\sigma ]\)-modules.

Let \(\mathcal {K}\) be a valued difference field. The difference operator \(\sigma \) of \(K\) is also referred to as the difference operator of \(\mathcal {K}\). By an extension of \(\mathcal {K}\) we shall mean a valued difference field \(\mathcal {K}'=(K',\ldots )\) that extends \(\mathcal {K}\) as a valued field and whose difference operator extends the difference operator of \(\mathcal {K}'\). In this situation we also say that \(\mathcal {K}\) is a valued difference subfield of \(\mathcal {K}'\), and we indicate this by \(\mathcal {K} \le \mathcal {K}'\). Such an extension is called immediate if it is immediate as an extension of valued fields. In dealing with a valued difference field \(\mathcal {K}\) as above \(v\) also denotes the valuation of any extension of \(\mathcal {K}\) that gets mentioned (unless specified otherwise), and any difference subfield \(E\) of \(K\) is construed as a valued difference subfield of \(\mathcal {K}\) in the obvious way. Whenever we say \(\mathcal {K}\) is a valued difference field, it should be understood that \(\mathcal {K}=(K, \varGamma , {{\varvec{k}}}; v, \pi )\); thus fixing the notations for the underlying field, value group, residue field and valuation. Likewise \(\mathcal {K}'\) will always be \((K', \varGamma ', {{\varvec{k}}}'; v',\pi ')\). In case \(\mathcal {K} \le \mathcal {K}'\) we write \(v\), \(\sigma \), \(\pi \) for \(v'\), \(\sigma '\) and \(\pi '\), respectively.

Let \(\mathcal {K}^h= (K^h, \varGamma , {{\varvec{k}}};\dots )\) be the henselization of the underlying valued field of \(\mathcal {K}\). By the universal property of “henselization” the operator \(\sigma \) extends uniquely to an automorphism \(\sigma ^h\) of the field \(K^h\) such that \(\mathcal {K}^h\) with \(\sigma ^h\) is a valued difference field. Accordingly we shall view \(\mathcal {K}^h\) as a valued difference field, making it thereby an immediate extension of the valued difference field \(\mathcal {K}\).

Given an extension \(\mathcal {K} \le \mathcal {K}'\) of valued difference fields and \(a \in K'\) we define \(\mathcal {K} \langle a \rangle \) to be the smallest valued difference subfield of \(\mathcal {K}'\) extending \(\mathcal {K}\) and containing \(a\) in its underlying difference field; thus the underlying difference field of \(\mathcal {K} \langle a \rangle \) is \(K \langle a \rangle \).

Hahn difference fields Let \({{\varvec{k}}}\) be a field and \(\varGamma \) an ordered abelian group. This gives the Hahn field \({{\varvec{k}}}((t^{\varGamma }))\) whose elements are the formal sums \(a=\sum _{\gamma \in \varGamma } a_\gamma t^{\gamma }\) with \(a_\gamma \in {{\varvec{k}}}\) for all \(\gamma \), with well-ordered support \(\{\gamma :\ a_\gamma \ne 0\} \subseteq \varGamma \). With \(a\) as above we define the valuation \(v: {{\varvec{k}}}((t^{\varGamma }))^{\times } \rightarrow \varGamma \) by \(v(a):=\min \{\gamma : a_\gamma \ne 0\}\), and the surjective ring morphism \(\pi :\ \mathcal {O}_v \rightarrow {{\varvec{k}}}\) by \(\pi (a):=a_0\). In this way we obtain the (maximal) valued field \(\mathcal {K}=({{\varvec{k}}}((t^\varGamma )), \varGamma , {{\varvec{k}}};v,\pi )\) which we also just refer to as the Hahn field \({{\varvec{k}}}((t^\varGamma ))\).

Suppose that the field \({{\varvec{k}}}\) is equipped with an automorphism \(\bar{\sigma }\) and that the ordered group \(\varGamma \) is equipped with an order-preserving automorphism \(\sigma \). Then

$$\begin{aligned} \sum _{\gamma } a_\gamma t^{\gamma } \mapsto \sum _{\gamma } \bar{\sigma }(a_\gamma ) t^{\sigma (\gamma )} \end{aligned}$$

is an automorphism, to be denoted by \(\sigma \), of the field \({{\varvec{k}}}((t^\varGamma ))\), with \(\sigma (\mathcal {O}_v)=\mathcal {O}_v\). We consider the three-sorted structure \(({{\varvec{k}}}((t^\varGamma )), \varGamma , {{\varvec{k}}};\ v,\pi )\), with the field \({{\varvec{k}}}((t^\varGamma ))\) equipped with the automorphism \(\sigma \) as above, as a valued difference field, and also refer to it as the Hahn difference field \({{\varvec{k}}}((t^\varGamma ))\).

PseudoCauchy sequences A well-indexed sequence is a sequence \(\{a_\rho \}\) indexed by the elements \(\rho \) of some nonempty well-ordered set without largest element; throughout “eventually” means “for all sufficiently large \(\rho \)” in the context of a well-indexed sequence. Let \(\mathcal {K}\) be a valued field and \(\{a_\rho \}\) a well-indexed sequence from \(K\).

Definition 2.1

The sequence \(\{a_\rho \}\) is a pseudoCauchy sequence (pc-sequence) if for some index \(\rho _0 \),

$$\begin{aligned} \rho '' > \rho ' > \rho \ge \rho _0\ \Longrightarrow \ v(a_{\rho ''}-a_{\rho '}) > v(a_{\rho '}-a_\rho ). \end{aligned}$$

For \(a\) in some valued field extension of \(\mathcal {K}\) we say that \(a\) is a pseudolimit of \(\{a_\rho \}\) if \(\{v(a-a_\rho )\}\) is eventually increasing, denoted \(a_\rho \leadsto a\).

For \(\rho _0\) as above, and put

$$\begin{aligned} \gamma _\rho :=v(a_{\rho '}-a_\rho ) \end{aligned}$$

for \(\rho '>\rho \ge \rho _0\); this depends only on \(\rho \). Then \(\{\gamma _\rho \}_{\rho \ge \rho _0}\) is strictly increasing. The width of \(\{a_\rho \}\) is the set

$$\begin{aligned} \{\gamma \in \varGamma \cup \{\infty \}:\gamma >\gamma _\rho \ \quad \text{ for } \text{ all }\ \quad \rho \ge \rho _0\}. \end{aligned}$$

Its significance is that if \(a,b\in K\) and \(a_\rho \leadsto a\), then \(a_\rho \leadsto b\) if and only if \(v(a-b)\) is in the width of \(\{a_\rho \}\). A useful observation about pc-sequences is that if \(\{a_\rho \}\) is a pc-sequence in an expansion of a valued field (e.g., in a valued difference field), then \(\{a_\rho \}\) has a pseudolimit in an elementary extension of that expansion.

3 Regularity and pseudoconvergence

Let \(\mathcal {K}\) be a valued difference field. For a \(\sigma \)-polynomial \(F(x)=\sum _{{\varvec{i}}}a_{{\varvec{i}}}{\varvec{\sigma }}(x)^{{\varvec{i}}}\) over \(K\) and \(\gamma \in \varGamma \) define \(F_v(\gamma ) :=\min _{{\varvec{i}}}\{v(a_{{\varvec{i}}})+{\varvec{\sigma }}^{{\varvec{i}}}(\gamma )\}\). Thus \(F\) induces a map

$$\begin{aligned} F_v:&\varGamma \rightarrow \varGamma \\&\gamma \mapsto F_v(\gamma ) \end{aligned}$$

which is strictly increasing whenever \(F(x)\) is nonzero and the constant term of \(F\) is equal to zero (since \(\sigma \) is an order- preserving automorphism of \(\varGamma \)). In general \(F_v\) is strictly increasing on an initial segment of \(\varGamma \) and constant on the complement of this initial segment. Note that if \(F\) is a \(\sigma \)-monomial then for all \(a \in K\) we have \(vF(a)=F_v(\gamma )\), where \(v(a)=\gamma \). This obviously does not hold for \(\sigma \)-polynomials.

Definition 3.1

Let \(F(x)\) be a \(\sigma \)-polynomial over \(K\). An element \(a \in K\) is regular for \(F\) if

$$\begin{aligned} v(F(a))=F_v(\gamma ), \end{aligned}$$

where \(\gamma =v(a)\); otherwise \(a\) is irregular for \(F\). We say that \(a \in K\) is regular over a subfield \(E\) of \(K\) if \(a\) is regular for all \(\sigma \)-polynomials with coefficients from \(E\).

Every element \(a \in K\) is regular for all \(\sigma \)-monomials over \(K\), and 0 is regular for \(F(x)\) if and only if \(F(0)=0\). Note that \(a\) is irregular for \(F(x)\) if and only if \(vF(a)>F_v(v(a))\).

Lemma 3.2

Let \(a, b \in K\) be such that \(v(b-a)>v(a)\) and \(F(x)\) a \(\sigma \)-polynomial over \(K\). Then \(a\) is regular for \(F(x)\) if and only if \(b\) is regular for \(F(x)\).

Proof

Suppose that \(a\) is regular for \(F(x)=\sum _{\varvec{i}}a_{\varvec{i}}{\varvec{\sigma }}(x)^{\varvec{i}}\) and \(v(a)=\gamma \). Pick \({\varvec{j}}\) with \(v(a_{\varvec{j}})+{\varvec{\sigma }}^{\varvec{j}}(\gamma )=F_v(\gamma )=vF(a)\) and let

$$\begin{aligned} G(x)=\frac{F(ax)}{a_{\varvec{j}}{\varvec{\sigma }}(a)^{\varvec{j}}}=\sum _{\varvec{i}}\frac{a_{\varvec{i}}{\varvec{\sigma }}(a)^{\varvec{i}}}{a_{\varvec{j}}{\varvec{\sigma }}(a)^{\varvec{j}}}{\varvec{\sigma }}(x)^{\varvec{i}}. \end{aligned}$$

Then \(G(x)\) has coefficients from the valuation ring, and since \(a\) is regular for \(F(x)\), \(vG(1)=0\). Therefore we obtain \(\overline{G}(1) \ne 0 \in {{\varvec{k}}}\) where \(\overline{G}(x)\) is the reduced \(\bar{\sigma }\)-polynomial over \({{\varvec{k}}}\). Set \(c=b/a\). Then \(\bar{c}=1\) and \(vG(c)=0\) since \(\overline{G}(\bar{c})=\overline{G}(1) \ne 0\). This leads to

$$\begin{aligned} vF(b)=v(a_{\varvec{j}})+{\varvec{\sigma }}^{\varvec{j}}(\gamma )=F_v(\gamma ) \end{aligned}$$

and so \(b\) is also regular for \(F(x)\).\(\square \)

If \(\{a_\rho \}\) is a pc-sequence in a valued field \(K\) and \(a_\rho \leadsto a\) with \(a\in K\) then for an ordinary nonconstant polynomial \(f(x) \in K[x]\) we have \(f(a_\rho ) \leadsto f(a)\) (see [9]). For certain valued difference fields, as in  [1], the same is true for nonconstant \(\sigma \)-polynomials but that is not the case in general. In the context of a value-preserving automorphism this issue was resolved in [4] via the notion of equivalent pc-sequences under the assumption that the automorphism is not of finite order over the residue field. We will also need this assumption, which we explicitly state as an axiom.

Axiom 1. For each integer \(d>0\) there is \(y\in {{\varvec{k}}}\) with \(\bar{\sigma }^d(y)\ne y\).

Also, the focus of the current paper is valued difference fields with residue characteristic zero, and so we assume this throughout the rest even though some results are valid without this assumption.

Definition 3.3

Two pc-sequences \(\{a_\rho \},\{b_\rho \}\) in a valued field are equivalent if for all \(a\) in all valued field extensions, \(a_\rho \leadsto a \Leftrightarrow b_\rho \leadsto a.\)

This is an equivalence relation on the set of pc-sequences with given index set and in a given valued field, and:

Lemma 3.4

Two pc-sequences \(\{a_\rho \}\) and \(\{b_\rho \}\) in a valued field are equivalent if and only if they have the same width and a common pseudolimit in some valued field extension.

We shall prove that given a pc-sequence \(\{a_\rho \}\) from a valued difference field \(\mathcal {K}\) which satisfies Axiom 1, and a \(\sigma \)-polynomial \(F(x)\) over \(\mathcal {K}\) there is an equivalent pc-sequence \(\{b_\rho \}\) such that \(\{F(b_\rho )\}\) is also a pc-sequence. Construction of \(b_\rho \), even when assuming specific behavior of \(\sigma \) as in [4], is quite complicated. Appropriately using regular elements this can be achieved in straightforward manner. First we state a well-known fact which will allow us to use Axiom 1 effectively.

Lemma 3.5

Let \(k \subseteq k'\) be a field extension, and \(g(x_0,\ldots ,x_n)\) a nonzero polynomial over \(k'\). Then there is a nonzero polynomial \(f(x_0,\ldots ,x_n)\) over \(k\) such that whenever \(y_0,\ldots ,y_n\in k\) and \(f(y_0,\ldots ,y_n)\ne 0\), then \(g(y_0,\ldots ,y_n) \ne 0\).

The existence of regular elements as described below will be the key tool for constructing an equivalent pc-sequence as in the above discussion.

Lemma 3.6

Suppose that \(\mathcal {K} \le \mathcal {K}'\) is an extension of valued fields, and \(\mathcal {K}\) satisfies Axiom 1. Let \(F\) be a \(\sigma \)-polynomial over \(K'\), and \(\gamma \in \varGamma \). Then there exists \(a \in K\) such that \(v(a)=\gamma \) and \(a\) is regular for \(F\).

Proof

Let \(F=\sum a_{\varvec{i}}\sigma ^{\varvec{i}}(x)\) and take \(b \in K\) with \(v(b)=\gamma \). Set

$$\begin{aligned} G(x):=\frac{F(bx)}{a_{\varvec{j}}{\varvec{\sigma }}(b)^{\varvec{j}}}=\sum _{{\varvec{i}}} \frac{a_{\varvec{i}}{\varvec{\sigma }}(b)^{\varvec{i}}}{a_{\varvec{j}}{\varvec{\sigma }}(b)^{\varvec{j}}}{\varvec{\sigma }}(x)^{{\varvec{i}}} \end{aligned}$$

where \({\varvec{j}}\) is such that \(F_v(\gamma )=v(a_{\varvec{j}})+{\varvec{\sigma }}^{\varvec{j}}(\gamma )\). So the coefficients of \(G(X)\) are in the valuation ring of \(K'\), with one coefficient equal to 1. So the reduced \(\bar{\sigma }\)-polynomial \(\overline{G}(x)\) over \({{\varvec{k}}}'\) is nonzero.

By Lemma 3.5 there is a nonzero \(\bar{\sigma }\)-polynomial \(h(x)\) over \({{\varvec{k}}}\) such that for all \(\alpha \in {{\varvec{k}}}\), \(\overline{G}(\alpha ) \ne 0\) whenever \(h(\alpha )\ne 0\). Since \(\bar{\sigma }\) is not of finite order as an automorphism of \({{\varvec{k}}}\), there exists a nonzero element \(\alpha \in {{\varvec{k}}}\) such that \(h(\alpha ) \ne 0\) (see [6], p. 201) and hence \(\overline{G}(\alpha ) \ne 0\). So we can take \(c \in K\) with \(v(c)=0\) and \(\bar{c}=\alpha \). Then \(v(G(c))= 0\), \(v(bc)=v(b)=\gamma \) and

$$\begin{aligned} v(F(bc))=v(a_{{\varvec{j}}}\sigma (b)^{{\varvec{j}}})=F_v(\gamma ). \end{aligned}$$

That is, \(a=bc \in K\) is regular for \(F\).\(\square \)

Remark 3.7

Under the same hypothesis of above lemma, given a finite set \(\Sigma \) of \(\sigma \)-polynomials over \(\mathcal {K}'\) and \(\gamma \in \varGamma \), we can find \(a\in K\) of valuation \(\gamma \) which is regular for every \(\sigma \)-polynomial in \(\Sigma \).

Theorem 3.8

Suppose \(\mathcal {K}\) satisfies Axiom 1, \(\{a_\rho \}\) is a pc-sequence from \(K\) and \(a_\rho \leadsto a\) in an extension. Let \(\Sigma \) be a finite set of \(\sigma \)-polynomials \(F(x)\) over \(K\). Then there is a pc-sequence \(\{b_\rho \}\) from \(K\), equivalent to \(\{a_\rho \},\) such that \(F(b_\rho ) \leadsto F(a)\) for each nonconstant \(F\) in \(\Sigma .\)

Proof

First, let us assume that \(\Sigma \) consists of a single nonconstant \(\sigma \)-polynomial \(F(x)\) over \(K\). Put \(\gamma _\rho :=v(a_\rho -a) \in \varGamma \); then \(\{\gamma _\rho \}\) is an eventually strictly increasing sequence. Also set

$$\begin{aligned} G(x):=F(a+x)-F(a)=\sum _{|{\varvec{i}}| \ge 1}F_{{\varvec{i}}}(a){\varvec{\sigma }}(x)^{{\varvec{i}}}. \end{aligned}$$

Note that \(G(x)\) is a nonzero \(\sigma \)-polynomial which has constant term zero and its coefficients are in \(K\langle a\rangle \).

For all \(\rho \) we choose, using Lemma 3.6, \(c_\rho \in K\) of valuation \(\gamma _\rho \) such that \(c_\rho \) is regular for \(G(x)\). Now, define \(b_\rho :=a_{\rho +1}+c_\rho \). Then \(v(a-b_\rho )=v(a-a_{\rho +1}-c_\rho )=\gamma _\rho \) eventually, so \(b_\rho \leadsto a\). Moreover

$$\begin{aligned} v(b_{\rho +1}-b_\rho )=v(a_{\rho +2} + c_{\rho +1} - a_{\rho +1} - c_\rho )=\gamma _\rho \end{aligned}$$

eventually, and hence \(\{b_\rho \}\) is equivalent to \(\{a_\rho \}\). Since \(c_\rho \) is regular for \(G(x)\) and

$$\begin{aligned} v(b_\rho -a-c_\rho )=v(a_{\rho +1}+c_\rho -a-c_\rho )=\gamma _{\rho +1}>v(c_\rho ) \end{aligned}$$

eventually, by Lemma 3.2, \(b_\rho -a\) is regular for \(G(x)\) eventually. Then

$$\begin{aligned} v\big (F(b_\rho )-F(a)\big )=vG(b_\rho -a)=G_v(\gamma _\rho ) \end{aligned}$$

eventually. Since \(G(x)\) has constant term equal to zero, \(G_v\) is a strictly increasing function, and hence \(F(b_\rho ) \leadsto F(a)\). The general case can be obtained using Remark 3.7.

\(\square \)

Corollary 3.9

The same result, where \(a\) is removed and one only asks that \(\{G(b_\rho )\}\) is a pc-sequence.

Proof

Put in an \(a\) from an elementary extension.\(\square \)

Using the above results it is easy to obtain the following theorem which will be crucial at later stages. See [4] for a detailed treatment.

Theorem 3.10

Let \(\mathcal {K}\) be a valued difference field satisfying Axiom 1. Let \(\{a_\rho \}\) be a pc-sequence from \(K\) and let \(a\) in some extension of \(\mathcal {K}\) be such that \(a_\rho \leadsto a\). Let \(G(x)\) be a \(\sigma \)-polynomial over \(K\) such that

  1. (i)

    \(G(a_\rho ) \leadsto 0\),

  2. (ii)

    \(G_{({\varvec{l}})}(b_\rho ) \not \leadsto 0\) whenever \(|{\varvec{l}}|\ge 1\) and \(\{b_\rho \}\) is a pc-sequence in \(K\) equivalent to \(\{a_\rho \}\).

Let \(\Sigma \) be a finite set of \(\sigma \)-polynomials \(H(x)\) over \(K\). Then there is a pc-sequence \(\{b_\rho \}\) in \(K\), equivalent to \(\{a_\rho \}\), such that \(G(b_\rho ) \leadsto 0\), and \(H(b_\rho ) \leadsto H(a)\) for every nonconstant \(H\) in \(\Sigma \).

The multivariable case and Kapranov’s theorem For our model theoretic treatment of valued difference fields we only need to deal with \(\sigma \)-polynomials in one variable. However we will provide generalizations of some of the results of this section to the multivariable case with the hope that they can be useful for other applications. A particular goal would be to establish a basis for tropical difference geometry.

Let \(F(x_1, x_2, \ldots , x_n)=\sum _{{\varvec{i}}} M_{{\varvec{i}}}\) be a multivariable \(\sigma \)-polynomial, where \(M_{{\varvec{i}}}\)’s are its monomials. Then each monomial \(M_{{\varvec{i}}}\) induces a function

$$\begin{aligned}&{M_{{\varvec{i}}}}_v:\varGamma ^n \rightarrow \varGamma \\&(\gamma _1,\ldots ,\gamma _n) \mapsto v(M_{{\varvec{i}}}(x_1,\ldots ,x_n)) \end{aligned}$$

where \(v(x_i)=\gamma _i\). We set \(F_v(\gamma _1,\ldots ,\gamma _n):=\min _{{\varvec{i}}}\{{M_{{\varvec{i}}}}_v (\gamma _1,\ldots ,\gamma _n)\}\). Note that when \(F\) is an ordinary multivariable polynomial, \(F_v\) is precisely the tropicalization of \(F\). We define a regular tuple for \(F\) to be an n-tuple \(a \in K^n\) such that \(F_v(v(a))=v(F(a))\).

We see \(\varGamma ^n\) as a group with componentwise addition and equipped with the natural partial ordering obtained from the ordering on \(\varGamma \). We say that \(\gamma , \theta \in \varGamma ^n\) are comparable if \(\gamma \le \theta \) or \(\theta \le \gamma \). We also extend all structure on \(K\) to \(K^n\) componentwise, and we use the same notations that we use for elements of \(\varGamma \) and \(K\) for n-tuples. So for \(a=(a_1,\ldots a_n) ,b=(b_1,\ldots ,b_n) \in K^n\) we have:

$$\begin{aligned} v(a)&=(v(a_1),\ldots ,v(a_n));\\ v(a)&<v(b) \Leftrightarrow v(a_i)<v(b_i) \quad \text { for } \quad i=1,\ldots ,n; \\ ab&=(a_1b_1,\ldots , a_nb_n);\\ a+b&=(a_1+b_1,\ldots ,a_n+b_n). \end{aligned}$$

It is easy to see that for \(a,b \in K^n\), we have \(v(ab)=v(a) + v(b)\) and

$$\begin{aligned} v(a+b)\ge \min \{v(a),v(b)\} \end{aligned}$$

whenever \(v(a)\) and \(v(b)\) are comparable. In particular, if \(v(a)<v(b)\), then \(v(a+b)=v(a)\). A pc-sequence from \(K^n\) is a sequence such that each of its coordinates is a pc-sequence in \(K\) and it pseudoconvergences to an n-tuple if each of its coordinates pseudoconverge to the corresponding coordinate of that n-tuple. Two pc-sequences from \(K^n\) are equivalent if the corresponding pc-sequences from each coordinate are equivalent.

Then it is straightforward to check that all the previous results of this section are valid in the multivariable context. In particular, we note the following consequence of the proof of the Lemma 3.6:

Lemma 3.11

Let \(a\ne 0 \in K^n\) and \(F(x)\) be a nonzero multivariable \(\sigma \)-polynomial. Then \(a\) is regular for \(F(x)\) if and only if \((1,\ldots ,1)\) is not a zero of reduced polynomial \(\overline{F(ax)/d}\) over \({\varvec{k}}\) for some \(d \in K^n\) of valuation \(F_v(v(a))\). More generally, for all \(b \in K^n\) such that \(v(b)=(0,\ldots ,0)\), the element \(ab\) is irregular for \(F\) if and only if \(ab\) is a root of \(F\) or \((\bar{b}_1,\ldots ,\bar{b}_n)\) is a root of \(\overline{F(ax)/d}\).

Now let us explain how these tools relate to tropical geometry. Let \(F(x)=\sum _{{\varvec{i}}} M_{{\varvec{i}}}\) be a multivariable \(\sigma \)-polynomial, with monomials \(M_{{\varvec{i}}}\), over a nontrivially valued field \(\mathcal {K}=(K,\varGamma , {{\varvec{k}}};v)\). A tropical zero of \(F\) is an element \(\gamma \in \varGamma ^n\), such that \(F_v(\gamma )\) is equal to \({M_{{\varvec{i}}}}_v(\gamma )={M_{{\varvec{j}}}}_v(\gamma )\) for some \({\varvec{i}}\ne {\varvec{j}}\). Note that if \(F\) is an ordinary polynomial in one variable, then it has finitely many tropical zeroes. The same assertion is false for multivariable polynomials and \(\sigma \)-polynomials even in one variable (e.g., if \(\sigma \) is the identity on \(\varGamma \) then \(F(x)=\sigma (x) - x\) has infinitely many tropical zeroes). This difference is actually the reason why pseudoconvergence is preserved under ordinary polynomials in one variable but not under \(\sigma \)-polynomials. So it is no surprise that the tools we introduced to deal with pseudoconvergence are actually closely related to tropical geometry.

If \(a \in K^n\) is a zero of \(F\) then \(v(a)\) is a tropical zero of \(F\). One of the essential results in tropical geometry is Kapranov’s Theorem (see Theorem 2.1.1. [7]) which asserts the converse when \(K\) is algebraically closed; namely that if \(\gamma \) is a tropical zero of \(F\) then there is \(a \in K^n\) with \(v(a)=\gamma \) and \(F(a)=0\). Using the lemma below we provide an alternative proof of this fact.

Lemma 3.12

Let \(F\) be an ordinary one variable polynomial over a nontrivially valued field \((K,\varGamma , v)\), \(\gamma \in \varGamma \) be a tropical zero of \(F\) and \(b \in K\) of valuation \(\gamma \). Consider the polynomial \(G(x):=\sum _{i \ge 1} F_{i}(b)x^i\). Then \(G_v(\gamma )=F_v(\gamma )\).

Proof

Since it enough to show that \(F_v(\gamma )\) and \(G_v(\gamma )\) agree over an extension of \((K,v)\) we can suppose that \(K\) is algebraically closed. Since the residue field is infinite, by the Lemma 3.6, we can choose \(\epsilon \in K^n\) of valuation \(\gamma \) which is regular for \(G\). Then \(v(\epsilon +b)\ge \gamma \) and \(F(\epsilon +b)-F(b)=G(\epsilon )\). Since

$$ \begin{aligned} vF(\epsilon +b)\ge F_v(\gamma ) \quad \& \quad vF(b)\ge F_v(\gamma ) \end{aligned}$$

we have \(v(G(\epsilon ))\ge F_v(\gamma )\).

The reduced polynomial \(\overline{F(bx)/d}\) with \(v(d)=F_v(\gamma )\), as in Corollary 3.11, is nonzero, and since \({{\varvec{k}}}\) is algebraically closed we can pick a root of it which provides an irregular element for \(F\) of the form \(by\) with \(v(y)=0\). On the other hand, as above, there exists regular elements for \(F\) for an arbitrary value in \(\varGamma \). Now if \(b\) is irregular for \(F\) then choose \(c \in K\) of valuation \(\gamma \) regular for \(F\), and if \(b\) is regular for \(F\) then choose \(c\) irregular for \(F\) of valuation \(\gamma \). Then \(v(c-b)=\gamma \) by 3.11 and \(v(F(c)-F(b))=\min \{F(c),F(b)\}=F_v(\gamma )\). Hence we have \(F_v(\gamma )=v(G(c-b))\ge G_v(\gamma )\).\(\square \)

Theorem 3.13

(Kapranov’s theorem) If \(F(x)\) is a nonzero multivariable polynomial over an algebraically closed valued field \((K,\varGamma ,v)\) and \(\gamma \in \varGamma ^n\) is a tropical zero of \(F\) then there is a root of \(F\) of valuation \(\gamma \).

Proof

Let \(a:=(a_1,\ldots , a_{n-1},a_n) \in K^n\) be of valuation \(\gamma \). Since \(\gamma \) is a tropical zero of \(F\) we can w.l.o.g. suppose that \(a\) is irregular for \(F(x)\): In fact if not, repeating the proof above, by 3.11 we can consider the polynomial \(\overline{F(ax)/d}\) over \({{\varvec{k}}}\); since \({{\varvec{k}}}\) is algebraically closed we can take a root of it which provides an irregular element for \(F(x)\) of the form \(ab\) with \(v(b)=(0,\ldots ,0)\). Remark in this case that by 3.11 \(a_n\) is irregular for the one variable polynomial \(F^a:=F(a_1,\ldots , a_{n-1}, y)\): the fact that \((1,\ldots ,1)\) is a root of \(\overline{F(ax)/d}\) implies \(1\) is a root of \(\overline{F^a(a_ny)/d}\). Now it is enough to find a zero of \(F^a\) of valuation \(v(a_n)\).

Set \(b_0:=a_n\) and \(\theta :=v(b_0)\). We will first find \(b_1 \in K\) of valuation \(\theta \) such that \(v(b_1-b_0)>\theta \) and \(F^a(b_1)>F^a(b_0)\). Set

$$\begin{aligned} G(x):= \sum _{i \ge 1} F^a_{(i)}(b_0)x^i. \end{aligned}$$

By divisibility of the value group \(\varGamma \) we can pick \(\delta \) such that \(G_v(\delta )=v(F^a(b_0))\). By Lemma 3.12 we have \(G_v(\theta )=F^a_v(\theta )\) and since \(b_0\) is irregular for \(F^a\) we get \(v(F^a(b_0))>F^a_v(\theta )\). Putting these together with the fact that \(G_v\) is strictly increasing we conclude that \(\delta > \theta \). Let \(\epsilon \) be such that \(v(\epsilon )=\delta \). Set \(b_1=b_0 + \epsilon u\) where \(u\) is a new variable. Then \(G(\epsilon u)+ F^a(b_0)= F^a(b_1)\). Since \(G_v(\delta )=v(F^a(b_0))\) the polynomial

$$\begin{aligned} H(u):=\frac{G(\epsilon u)}{F^a(b_0)} \end{aligned}$$

has coefficients from the valuation ring of \(K\), and the reduced polynomial \(\overline{H}(u)\) over the residue field is nonzero and has constant term zero. Now, in order to have \(F^a(b_1)>F^a(b_0)\), we pick a \(c \in K\) of valuation zero such that \(\bar{c} \in {{\varvec{k}}}\) is a zero of the polynomial \(\overline{H} + 1\) and set \(b_1=b_0 + \epsilon c\).

Proceeding inductively we can construct a pc-sequence \(\{b_k\}_{k \in \mathbb {N}}\) with \(F^a(b_{k+1})>F^a(b_{k})\) if \(F^a(b_k)\ne 0\) for all \(k\in \mathbb {N}\). Since \(\{b_k\}\) is of algebraic type, \(\{b_k\} \leadsto b_{\omega }\) for some \(b_{\omega } \in K\). Since \(\{F^a(b_k)\} \leadsto 0\) and \(\{F^a(b_k)\} \leadsto F^a(b_{\omega })\) we have \(F^a(b_{\omega })>F^a(b_k)\) for all \(k \in \mathbb {N}\). Then again either \(F^a(b_{\omega })=0\) or we can continue extending our sequence as before. Hence we can construct a pc-sequence of arbitrary length \(\{b_\rho \}\) if during the process we do not get a zero \(F^a\). We must obtain a zero of \(F^a\) considering the cardinality of \(K\).\(\square \)

4 Approximating zeroes of \(\sigma \)-polynomials

Let \(\mathcal {K}\) be a valued difference field of residue characteristic zero as usual. Let \(G(x)\) be a \(\sigma \)-polynomial over \(K\) of order \(\le n\) and \(a\in K\). Let \({\varvec{i}}\) range over tuples \((i_0,\ldots ,i_n)\in \mathbb {N}^{n+1}\), and likewise with \({\varvec{j}}=(j_0,\ldots ,j_n)\), \({\varvec{l}}=(l_0, \ldots ,l_n)\). Much of this section is parallel with the corresponding sections of [4] and [2]. There are some points which require close inspection, in which case we present proofs in full detail even though they look identical to what is already known from [4] and [2]; otherwise we just point out the necessary references.

Definition 4.1

We say \((G,a)\) is in \(\sigma \)-hensel configuration if \(G\notin K\) and there is \({\varvec{i}}\) with \(|{\varvec{i}}|=1\) and \(\gamma \in \varGamma \) such that

  1. (i)

    \(v(G(a))=v(G_{({\varvec{i}})}(a))+{\varvec{\sigma }}^{{\varvec{i}}}\gamma \le v(G_{({\varvec{j}})}(a)) +{\varvec{\sigma }}^{{\varvec{j}}}\gamma \) whenever \(|{\varvec{j}}|=1\),

  2. (ii)

    \(v(G_{({\varvec{j}})}(a))+{\varvec{\sigma }}^{{\varvec{j}}}\gamma < v(G_{({\varvec{j}}+{\varvec{l}})}(a)) +{\varvec{\sigma }}^{{\varvec{j}}+{\varvec{l}}}\gamma \) whenever \({\varvec{j}}, {\varvec{l}}\ne 0\) and \(G_{({\varvec{j}})} \ne 0\).

If \((G,a)\) is in \(\sigma \)-hensel configuration then \(G_{({\varvec{j}})}(a) \ne 0\) whenever \({\varvec{j}}\ne 0\) and \(G_{({\varvec{j}})} \ne 0\), so \(G(a)\ne 0\), and therefore \(\gamma \) as above satisfies

$$\begin{aligned} v(G(a))=\min _{|{\varvec{j}}|=1} v(G_{({\varvec{j}})}(a))+{\varvec{\sigma }}^{{\varvec{j}}}\gamma , \end{aligned}$$

so is unique, and we set \(\gamma (G,a):=\gamma \). If \((G,a)\) is not in \(\sigma \)-hensel configuration we set \(\gamma (G,a):=\infty \).

Remark 4.2

Suppose \(G\) is nonconstant, \(G(a)\ne 0\), \(v(G(a))>0\) and \(v(G_{({\varvec{i}})}(a))=0\) for all \({\varvec{i}}\ne 0\) with \(G_{({\varvec{i}})} \ne 0\). Then \((G,a)\) is in \(\sigma \)-hensel configuration with \(\gamma (G,a)>0\).

The definition of \(\sigma \)-hensel configuration above is identical with the corresponding definition in [1] and [4]. In order to obtain Lemma 4.3 we need to impose the following condition on the residue difference field.

Axiom \(2_n\). If \(\alpha _0,\ldots ,\alpha _n \in {{\varvec{k}}}\) are not all \(0\) then the equation

$$\begin{aligned} 1+\alpha _0x + \cdots + \alpha _m\bar{\sigma }^n(x)=0 \end{aligned}$$

has a solution in \({{\varvec{k}}}\).

We say that a difference field satisfies Axiom 2 if it satisfies Axiom \(2_n\) for all n, such a difference field will be called linear difference closed. This axiom is very similar to Kaplansky’s condition on residue fields in the study of valued fields of positive residue characteristic. One just replaces the Frobenius with \(\bar{\sigma }\), see [1] for a detailed study of the connection. It is shown in [1] that Axiom 2 can not be avoided if one wants to obtain Theorem 5.8. Nonetheless it is conceivable that AKE-type results can be obtained without having Theorem 5.8 and hence without requiring the residue difference field to be linear difference closed. Presently we avoid this discussion and assume throughout the rest of the paper that all valued difference fields under consideration satisfy Axiom 2. Note that Axiom 2 implies Axiom 1. The next lemma is identical to Lemma 4.4 from [1], and one can see that its proof remains valid in our context when the details are made explicit.

Lemma 4.3

Suppose that \(\mathcal {K}\) satisfies Axiom \(2\), and \((G,a)\) is in \(\sigma \)-hensel configuration. Then there is \(b \in K\) such that

  1. (1)

    \(v(b-a) \ge \gamma (G,a), \quad v(G(b))>v(G(a))\),

  2. (2)

    either \(G(b)=0\), or \((G,b)\) is in \(\sigma \)-hensel configuration.

For any such \(b\) we have \(v(b-a) = \gamma (G,a)\) and \(\gamma (G,b)>\gamma (G,a)\).

Proof

Let \(\gamma =\gamma (G,a)\), pick \(\epsilon \in K\) with \(v(\epsilon )=\gamma \). Let \(b=a+\epsilon u\) where \(u \in K\) is to be determined later; we only impose \(v(u)\ge 0\) for now. Consider

$$\begin{aligned} G(b)=G(a) + \sum \limits _{|{\varvec{i}}| \ge 1}G_{({\varvec{i}})}(a) \cdot {\varvec{\sigma }}(b-a)^{{\varvec{i}}}. \end{aligned}$$

Therefore \(G(b)=G(a) \cdot (1+ \sum \limits _{|{\varvec{i}}| \ge 1} c_{{\varvec{i}}} \cdot {\varvec{\sigma }}(u)^{{\varvec{i}}})\), where

$$\begin{aligned} c_{{\varvec{i}}}=\frac{G_{({\varvec{i}})}(a) \cdot {\varvec{\sigma }}(\epsilon )^{{\varvec{i}}}}{G(a)}. \end{aligned}$$

From \(v(\epsilon )=\gamma \) we obtain \(\min _{|{\varvec{i}}|=1} v(c_{{\varvec{i}}}) =0\) and \(v(c_{{\varvec{j}}})>0\) for \(|{\varvec{j}}|>1\). Then imposing \(v(G(b)) > v(G(a))\) forces \(\bar{u}\) to be a solution of the equation

$$\begin{aligned} 1+\sum \limits _{|{\varvec{i}}|=1}\bar{c_{{\varvec{i}}}} \cdot \bar{{\varvec{\sigma }}}(x)^{{\varvec{i}}}=0. \end{aligned}$$

By Axiom \(2\) we can take \(u\) with this property, and then \(v(u)=0\), so \(v(b-a)=\gamma (G,a)\) and \(v(G(b))>v(G(a))\).

Assume that \(G(b) \ne 0\). It remains to show that then \((G,b)\) is in \(\sigma \)-hensel configuration with \(\gamma (G,b)>\gamma \). Let \({\varvec{j}}\ne 0\), \(G_{({\varvec{j}})} \ne 0\) and consider

$$\begin{aligned} G_{({\varvec{j}})}(b)=G_{({\varvec{j}})}(a) + \sum \limits _{{\varvec{l}}\ne 0} G_{({\varvec{j}})({\varvec{l}})}(a) \cdot {\varvec{\sigma }}(b-a)^{{\varvec{l}}}. \end{aligned}$$

Note that \(G_{({\varvec{j}})}(a) \ne 0\). Since \({\text {char}}{{{\varvec{k}}}}=0\), \(v(G_{({\varvec{j}})({\varvec{l}})}(a))=v(G_{({\varvec{j}}+{\varvec{l}})}(a))\). Therefore, for all \({\varvec{l}}\ne 0\),

$$\begin{aligned} v\big (G_{({\varvec{j}})({\varvec{l}})}(a) \cdot {\varvec{\sigma }}(b-a)^{{\varvec{l}}}\big )>v(G_{({\varvec{j}})}(a)), \end{aligned}$$

hence \(v(G_{({\varvec{j}})}(b))=v(G_{({\varvec{j}})}(a))\). If \(|{\varvec{i}}|=1\), then \(\theta \mapsto {\varvec{\sigma }}^{{\varvec{i}}}(\theta )\) is an automorphism of \(\varGamma \). Since \(G(b)\ne 0\), it follows that we can pick \(\gamma _1 \in \varGamma \) such that

$$\begin{aligned} G(b)=\min _{|{\varvec{i}}|=1} v(G_{({\varvec{i}})}(b)) + {\varvec{\sigma }}^{{\varvec{i}}}\gamma _1. \end{aligned}$$

Note that \(\gamma _1 > \gamma \) because \(v(G(b))>v(G(a))\) and \(v(G_{({\varvec{i}})}(b))=v(G_{({\varvec{i}})}(a))\) for \({\varvec{i}}\ne 0\). Also for \({\varvec{i}},{\varvec{j}}\ne 0\) and \(\theta \in \varGamma \) with \(\theta >0\) we have \({\varvec{\sigma }}^{{\varvec{i}}}\theta <{\varvec{\sigma }}^{{\varvec{i}}+{\varvec{j}}}\theta \), since \(\sigma \) is order- preserving. Now the inequality

$$\begin{aligned} v(G_{({\varvec{i}})}(a)) + {\varvec{\sigma }}^{{\varvec{i}}}\gamma < v(G_{({\varvec{i}}+{\varvec{j}})}(a)) + {\varvec{\sigma }}^{{\varvec{i}}+{\varvec{j}}}\gamma \end{aligned}$$

together with \(\gamma _1>\gamma \) leads toFootnote 3

$$\begin{aligned} v(G_{({\varvec{i}})}(a)) + {\varvec{\sigma }}^{{\varvec{i}}}\gamma _1 < v(G_{({\varvec{i}}+{\varvec{j}})}(a)) + {\varvec{\sigma }}^{{\varvec{i}}+{\varvec{j}}}\gamma _1. \end{aligned}$$

Hence \((G,b)\) is in \(\sigma \)-hensel configuration with \(\gamma _1=\gamma (G,b)\).\(\square \)

Using the above lemma it is straightforward to obtain the following (see [2] for a proof).

Lemma 4.4

Suppose \(\mathcal {K}\) satisfies Axiom \(2\) and \(G(x)\) is \(\sigma \)-henselian at \(a\). Suppose also that there is no \(b\in K\) with \(G(b)=0\) and \(v(a-b) = v(G(a))\). Then there is a pc-sequence \(\{a_\rho \}\) in \(K\) with the following properties:

  1. (1)

    \(a_0=a\) and \(\{a_\rho \}\) has no pseudolimit in \(K\);

  2. (2)

    \(\{v(G(a_\rho ))\}\) is strictly increasing, and thus \(G(a_\rho ) \leadsto 0\);

  3. (3)

    \(v(a_{\rho '} -a_\rho )=v\big (G(a_\rho )\big )\) whenever \(\rho <\rho '\);

  4. (4)

    for any extension \(\mathcal {K}'=(K',\ldots )\) of \(\mathcal {K}\) and \(b,c\in K'\) such that \(a_\rho \leadsto b\), \(G(c)=0\) and \(v(b-c)\ge v(G(b))\), we have \(a_\rho \leadsto c\).

Definition 4.5

A valued difference field \(\mathcal {K}\) is \(\sigma \)-henselian if for all \((G,a)\) in \(\sigma \)-hensel configuration there is \(b \in K\) such that \(v(b-a)=\gamma (G,a)\) and \(G(b)=0\).

Lemma 4.6

If \(\mathcal {K}\) is \(\sigma \)-henselian, then \(\mathcal {K}\) satisfies Axiom \(2\).

Proof

Assume that \(\mathcal {K}\) is \(\sigma \)-henselian and let \(\alpha _0, \ldots , \alpha _n \in {{\varvec{k}}}\), not all zero. Let

$$\begin{aligned} G(x)=1+ a_0x + \cdots + a_n\sigma ^n(x) \qquad (\text {all }a_i\in K), \end{aligned}$$

where \(a_i=0\) if \(\alpha _i=0\), and \(v(a_i)=0\) with \(\bar{a}_i=\alpha _i\) if \(\alpha _i \ne 0\), for \(i=0, \ldots , n\). It is easy to see that \((G,0)\) is in \(\sigma \)-hensel configuration with \(\gamma (G,a)=0\). This gives \(a \in K\) such that \(v(a)=0\) and \(G(a)=0\). Then \(\bar{a}\) is a solution of

$$\begin{aligned} 1+\alpha _0x + \cdots + \alpha _n \bar{\sigma }^n(x)=0. \end{aligned}$$

\(\square \)

Definition 4.7

We say \(\{a_\rho \}\) is of \(\sigma \)-algebraic type over \(K\) if \(G(b_\rho ) \leadsto 0\) for some \(\sigma \)-polynomial \(G(x)\) over \(K\) and an equivalent pc-sequence \(\{b_\rho \}\) in \(K\).

If \(\{a_\rho \}\) is of \(\sigma \)-algebraic type over \(K\) then a minimal \(\sigma \)-polynomial of \(\{a_\rho \}\) over \(K\) is a \(\sigma \)-polynomial \(G(x)\) over \(K\) with the following properties:

  1. (i)

    \( G(b_\rho ) \leadsto 0\) for some pc-sequence \(\{b_\rho \}\) in \(K\), equivalent to \(\{a_\rho \}\);

  2. (ii)

    whenever \(H(x)\) is a \(\sigma \)-polynomial over \(K\) of lower complexityFootnote 4 than \(G\) and \(\{b_\rho \}\) is a pc-sequence in \(K\) equivalent to \(\{a_\rho \}\).

If \(\{a_\rho \}\) is of \(\sigma \)-algebraic type over \(K\) then \(\{a_\rho \}\) clearly has a minimal \(\sigma \)-polynomial over \(K\).

Lemma 4.8

Suppose \(\mathcal {K}\) satisfies Axiom 2. Let \(\{a_\rho \}\) from \(K\) be a pc-sequence of \(\sigma \)-algebraic type over \(K\) with minimal \(\sigma \)-polynomial \(G(x)\) over \(K\), and with pseudolimit \(a\) in some extension. Let \(\Sigma \) be a finite set of \(\sigma \)-polynomials \(H(x)\) over \(K\). Then there is a pc-sequence \(\{b_\rho \}\) in \(K\), equivalent to \(\{a_\rho \}\), such that, with \(\gamma _\rho :=v(a-a_\rho )\):

  1. (1)

    \(G(b_\rho ) \leadsto 0\) and eventually \(v(a-b_\rho )=\gamma _\rho \);

  2. (2)

    if \(H\in \Sigma \) and \(H \notin K\), then \(H(b_\rho ) \leadsto H(a)\);

  3. (3)

    Eventually \((G, b_\rho )\) is in \(\sigma \)-hensel configuration with \(\gamma (G,b_\rho )=\gamma _\rho \);

  4. (4)

    If \(G(a)\ne 0\), then \((G,a)\) is in \(\sigma \)-hensel configuration, and \(\gamma (G,a) > \gamma _\rho \), eventually.

Proof

Let \(G\) have order \(n\). We can assume that \(\Sigma \) includes all \(G_{({\varvec{i}})}\). In the rest of the proof \({\varvec{i}},{\varvec{j}},{\varvec{l}}\) range over \(\mathbb {N}^{n+1}\). Since Axiom 2 implies Axiom 1, Theorem 3.10 and its proof yield an equivalent pc-sequence \(\{b_\rho \}\) in \(K\) such that (1) and (2) hold. Choosing regular elements like in the proof of Theorem 3.8 yields in addition that there is \({\varvec{i}}\in \mathbb {N}^{n+1}\) such that, for cofinally many \(\rho \),

$$\begin{aligned} v\big (G(b_\rho )-G(a)\big )= v\big (G_{({\varvec{i}})}(a)\big ) +\sigma ^{{\varvec{i}}}\gamma _\rho \le v\big (G_{({\varvec{j}})}(a)\big )+\sigma ^{{\varvec{j}}}\gamma _\rho , \end{aligned}$$

for each \({\varvec{j}}\ne {\varvec{i}}\). Hence we can w.l.o.g. suppose that the above formula holds eventually for all \(\rho \) (if needed we can pass to an cofinal subsequence of \(\{b_\rho \}\) which is necessarily equivalent to it). Now \(\left\{ v\big (G(b_\rho )\big )\right\} \) is strictly increasing, eventually, so \(v\big (G(a)\big ) > v\big (G(b_\rho )\big )\) eventually, and so for \({\varvec{j}}\ne {\varvec{i}}\):

$$\begin{aligned} v\big (G(b_\rho )\big )= v\big (G_{({\varvec{i}})}(a)\big ) +\sigma ^{{\varvec{i}}}\gamma _\rho \le v\big (G_{({\varvec{j}})}(a)\big )+\sigma ^{{\varvec{j}}}\gamma _\rho , \quad \text {eventually}. \end{aligned}$$

We claim that \(|{\varvec{i}}|=1\). Let \(|{\varvec{j}}|=1\) with \(G_{({\varvec{j}})}\ne 0\), and let \({\varvec{k}}>{\varvec{j}}\); our claim will then follow by deriving

$$\begin{aligned} v\big (G_{({\varvec{j}})}(a)\big ) + \sigma ^{{\varvec{j}}}\gamma _\rho < v\big (G_{({\varvec{k}})}(a)\big ) + \sigma ^{{\varvec{k}}}\gamma _\rho , \quad \text {eventually}. \end{aligned}$$

The proof of Theorem 3.8 with \(G_{({\varvec{j}})}\) in the role of \(G\) shows that we can arrange that our sequence \(\{b_\rho \}\) also satisfies

$$\begin{aligned} v\big (G_{({\varvec{j}})}(b_\rho )-G_{({\varvec{j}})}(a)\big ) \le v\big (G_{({\varvec{j}})({\varvec{l}})}(a)\big ) +\sigma ^{{\varvec{l}}}\gamma _\rho , \quad \text {eventually} \end{aligned}$$

for all \({\varvec{l}}\) with \(|{\varvec{l}}|\ge 1\). Since \(v\big (G_{({\varvec{j}})}(b_\rho )\big )=v\big (G_{({\varvec{j}})}(a)\big )\) eventually, this yields

$$\begin{aligned} v\big (G_{({\varvec{j}})}(a)\big )\le v\big (G_{({\varvec{j}})({\varvec{l}})}(a)\big ) +\sigma ^{{\varvec{l}}}\gamma _\rho , \quad \text {eventually} \end{aligned}$$

for all \({\varvec{l}}\) with \(|{\varvec{l}}|\ge 1\), hence for all such \({\varvec{l}}\),

$$\begin{aligned} v\big (G_{({\varvec{j}})}(a)\big )\le v{{{\varvec{j}}+ {\varvec{l}}}\atopwithdelims (){\varvec{i}}} +v\big (G_{({\varvec{j}}+ {\varvec{l}})}(a)\big )+\sigma ^{{\varvec{l}}}\gamma _\rho , \quad \text {eventually} \end{aligned}$$

For \({\varvec{l}}\) with \({\varvec{j}}+{\varvec{l}}={\varvec{k}}\), this yields

$$\begin{aligned} v\big (G_{({\varvec{j}})}(a))\le v{{{\varvec{k}}\atopwithdelims (){\varvec{j}}}} +v\big (G_{({\varvec{k}})}(a)\big )+\sigma ^{{\varvec{k}}-{\varvec{j}}}\gamma _\rho , \quad \text {eventually}. \end{aligned}$$

Since \({\text {char}}({{\varvec{k}}})=0\),

$$\begin{aligned}&v\big (G_{({\varvec{j}})}(a))\le v\big (G_{({\varvec{k}})}(a)\big )+\sigma ^{{\varvec{k}}-{\varvec{j}}}\gamma _\rho , \quad \text {eventually, hence}\\&v\big (G_{({\varvec{j}})}(a)\big )+\sigma ^{{\varvec{j}}}\gamma _\rho <v(G_{({\varvec{k}})}(a))+ \sigma ^{{\varvec{k}}}\gamma _\rho , \quad \text {eventually}. \end{aligned}$$

Thus \(|{\varvec{i}}|=1\) as claimed. Then we obtain (3) and (4) by the above inequalities together with the fact that \(G\) is a minimal \(\sigma \)-polynomial of \(\{b_\rho \}\).\(\square \)

5 Immediate extensions

Throughout this section \(\mathcal {K}=(K,\varGamma ,{{\varvec{k}}}; v,\pi )\) is a valued difference field satisfying Axiom 2. Note that immediate extensions of \(\mathcal {K}\) also satisfy Axiom 2. We let \(K\) stand for \(\mathcal {K}\) when the meaning is clear from the context. The results of this section contain precisely the same conclusions as in the results of the corresponding sections of [2, 4] and [1]. Having proved Lemmas 4.3 and 4.8 for the general context of this paper, proofs in [2, 4] and [1] remain intact. Therefore we present the results without proof.

Definition 5.1

A pc-sequence \(\{a_\rho \}\) from \(K\) is said to be of \(\sigma \)-transcendental type over \(K\) if it is not of \(\sigma \)-algebraic type over \(K\), that is, for each \(\sigma \)-polynomial \(G(x)\) over \(K\) and each equivalent pc-sequence \(\{b_\rho \}\) from \(K\).

In particular, such a pc-sequence cannot have a pseudolimit in \(K\). For the proofs of next two lemmas see [4] or [1].

Lemma 5.2

Let \(\{a_\rho \}\) from \(K\) be a pc-sequence of \(\sigma \)-transcendental type over \(K\). Then \(\mathcal {K}\) has an immediate extension \((K\langle a \rangle , \varGamma ,{{\varvec{k}}}; v_a, \pi _a)\) such that:

  1. (1)

    \(a\) is \(\sigma \)-transcendental over \(K\) and \(a_\rho \leadsto a\);

  2. (2)

    for any extension \((K_1,\varGamma _1,{{\varvec{k}}}_1;v_1,\pi _1)\) of \(\mathcal {K}\) and any \(b\in K_1\) with \(a_\rho \leadsto b\) there is a unique embedding

    $$\begin{aligned} (K\langle a \rangle , \varGamma ,{{\varvec{k}}}; v_a, \pi _a)\ \longrightarrow \ (K_1,\varGamma _1,{{\varvec{k}}}_1;v_1,\pi _1) \end{aligned}$$

    over \(\mathcal {K}\) that sends \(a\) to \(b\).

Lemma 5.3

Let \(\{a_\rho \}\) from \(K\) be a pc-sequence of \(\sigma \)-algebraic type over \(K\), with no pseudolimit in \(K\). Let \(G(x)\) be a minimal \(\sigma \)-polynomial of \(\{a_\rho \}\) over \(K\). Then \(\mathcal {K}\) has an immediate extension \((K\langle a \rangle , \varGamma ,{{\varvec{k}}}; v_a, \pi _a)\) such that

  1. (1)

    \(G(a)=0\) and \(a_\rho \leadsto a\);

  2. (2)

    for any extension \((K_1, \varGamma _1,{{\varvec{k}}}_1; v_1, \pi _1)\) of \(\mathcal {K}\) and any \(b\in K_1\) with \(G(b)=0\) and \(a_\rho \leadsto b\) there is a unique embedding

    $$\begin{aligned} (K\langle a \rangle , \varGamma ,{{\varvec{k}}}; v_a, \pi _a) \longrightarrow \ (K_1, \varGamma _1,{{\varvec{k}}}_1; v_1, \pi _1) \end{aligned}$$

    over \(\mathcal {K}\) that sends \(a\) to \(b\).

We note the following consequences of Lemmas 5.2 and 5.3:

Corollary 5.4

Let \(a\) from some extension of \(\mathcal {K}\) be \(\sigma \)-algebraic over \(K\) and let \(\{a_\rho \}\) be a pc-sequence in \(K\) such that \(a_\rho \leadsto a\). Then \(\{a_\rho \}\) is of \(\sigma \)-algebraic type over \(K\).

Corollary 5.5

Suppose \(\mathcal {K}\) is finitely ramified. Then \(\mathcal {K}\) as a valued field has a proper immediate extension if and only if \(\mathcal {K}\) as a valued difference field has a proper immediate extension.

We say that \(\mathcal {K}\) is \(\sigma \)-algebraically maximal if it has no proper immediate \(\sigma \)-algebraic extension, and we say it is maximal if it has no proper immediate extension. Corollary 5.4 and Lemmas 5.3 and 4.4 yield:

Corollary 5.6

  1. (1)

    \(\mathcal {K}\) is \(\sigma \)-algebraically maximal if and only if each pc-sequence in \(K\) of \(\sigma \)-algebraic type over \(K\) has a pseudolimit in \(K\);

  2. (2)

    if \(\mathcal {K}\) satisfies Axiom \(2\) and is \(\sigma \)-algebraically maximal, then \(\mathcal {K}\) is \(\sigma \)-henselian.

It is clear that \(\mathcal {K}\) has \(\sigma \)-algebraically maximal immediate \(\sigma \)-algebraic extensions, and also maximal immediate extensions. Using the next lemma we will show that if \(\mathcal {K}\) satisfies Axiom 2 both kinds of extensions are unique up to isomorphism.

Lemma 5.7

Suppose \(\mathcal {K}\) satisfies Axiom 1 and \(\mathcal {K}'\) satisfies Axiom 2. Let \(\mathcal {K}'\) be \(\sigma \)-algebraically maximal extension of \(\mathcal {K}\) and \(\{a_\rho \}\)  from \(K\) be a pc-sequence of \(\sigma \)-algebraic type over \(K\), with no pseudolimit in \(K\), and with minimal \(\sigma \)-polynomial \(G(x)\) over \(K\). Then there exists \(b\in K'\) such that \(a_\rho \leadsto b\) and \(G(b)=0\).

Proof

Lemma 5.3 provides a pseudolimit \(a\in K'\) of \(\{a_\rho \}\). Take a pc-sequence \(\{b_\rho \}\) in \(K\) equivalent to \(\{a_\rho \}\) with the properties listed in Lemma 4.8. Since \(\mathcal {K}'\) satisfies Axiom 2, it is \(\sigma \)-henselian and hence there is \(b\in K'\) such that

$$\begin{aligned} v(a-b)=\gamma (G,a)\quad \text {and}\quad G(b)=0. \end{aligned}$$

Note that \(a_\rho \leadsto b\) since \(\gamma (G,a) > v(a-a_\rho )=\gamma _\rho \) eventually.\(\square \)

Together with Lemmas 5.2 and  5.3 this yields:

Theorem 5.8

Suppose \(\mathcal {K}\) satisfies Axiom \(2\). Then all its maximal immediate extensions are isomorphic over \(\mathcal {K}\), and all its \(\sigma \)-algebraically maximal immediate \(\sigma \)-algebraic extensions are isomorphic over \(\mathcal {K}\).

It is worth mentioning that the above result fails if Axiom 2 is not assumed (see [1]). A minor variant of these results will be needed in proving our model theoretic conclusions, and its proof is straightforward. Let \(|X|\) denote the cardinality of a set \(X\), and let \(\kappa \) be a cardinal.

Lemma 5.9

Suppose \(\mathcal {E}=(E, \varGamma _E, \ldots )\le \mathcal {K}\) satisfies Axiom 1 and \(\mathcal {K}\) is \(\sigma \)-henselian, and \(\kappa \)-saturated with \(\kappa >|\varGamma _E|\). Let \(\{a_\rho \}\) from \(E\) be a pc-sequence of \(\sigma \)-algebraic type over \(E\), with no pseudolimit in \(E\), and with minimal \(\sigma \)-polynomial \(G(x)\) over \(E\). Then there exists \(b\in K\) such that \(a_\rho \leadsto b\) and \(G(b)=0\).

In combination with Lemmas 5.2 and 5.3 this yields:

Corollary 5.10

If \(\mathcal {E}=(E, \varGamma _E, \ldots )\le \mathcal {K}\) satisfies Axiom \(2\), and \(\mathcal {K}\) is \(\sigma \)-henselian, and \(\kappa \)-saturated with \(\kappa >|\varGamma _E|\), then any maximal immediate extension of \(\mathcal {E}\) can be embedded in \(\mathcal {K}\) over \(\mathcal {E}\).

6 The embedding theorem

Theorem 6.2, the main result of the paper, will give us a criterion for elementary equivalence between \(\sigma \)-henselian valued difference fields of residue characteristic zero and also a relative quantifier elimination result. We now present the notion of rv-structure for a valued field which will be needed for relative quantifier elimination. This notion was introduced in [3] building up on the notion of additive multiplicative congruences.

RV-structure Let \(\mathcal {K}\) be a valued field. The rv-sort for \(K\) is the imaginary sort \( RV =K^{\times }/1 + \mathfrak {m}\), which is a multiplicative group. The associated canonical surjection is denoted by \(rv\), and we extend it to \(K\) by setting \(rv(0) :=\infty \). The subgroup \(\mathcal {O}^{\times }/1 + \mathfrak {m}\) of \( RV \) is exactly \({{\varvec{k}}}^{\times }\). Two elements \(a, b \in K\) are equivalent modulo \(1 + \mathfrak {m}\) if and only if \(v(a-b)>v(a)=v(b)\) and so the map

$$\begin{aligned} v_{rv} :&RV \rightarrow \varGamma \\&a(1+\mathfrak {m}) \mapsto v(a) \end{aligned}$$

is well-defined. There is also a partial addition on the rv-sort. For \(a,b \in K\) with \(v(a+b)=\min \{v(a),v(b)\}\), define

$$\begin{aligned} rv(a)+rv(b):=rv(a+b). \end{aligned}$$

It is clear that this partial addition is well-defined and we can extend this addition to all of \( RV \) by setting \(rv(a)+rv(b):=\infty \) whenever \(v(a+b) \ne \min \{v(a),v(b)\}\). We denote this map by \(\bigoplus \).

If \(\mathcal {K}\) is a valued difference field its distinguished automorphism \(\sigma \) fixes \(\mathfrak {m}\) setwise, and so the map \(\sigma _{rv} : x(1 + \mathfrak {m}) \rightarrow rv(\sigma (x))\) is also well-defined. Moreover the induced maps \(\sigma _{rv}:\varGamma \rightarrow \varGamma \) and \(\sigma :\varGamma \rightarrow \varGamma \) are the same. We consider the rv-sort of \(\mathcal {K}\) as first-order structure in the language \(\mathcal {L}_{rv}:=\{.,^{-1},\oplus , 1, v_{rv}, \sigma _{rv}\}\) and refer to it as the difference rv-structure of \(\mathcal {K}\). Replacing the addition, multiplication and the difference operator on \(K\) by the corresponding operations on the rv-sort, we may consider a \(\sigma \)-polynomial \(F(x)\) over \(K\) as a function on the rv-sort, also denoted \(F(x)\). It is worth noting that the value group and residue field are interpretable in the rv-structure both for valued fields and valued difference fields (see Proposition 9.3 of [12]).

The main result In this subsection we consider \(4\)-sorted structures

$$\begin{aligned} \mathcal {K}=\big (K, \varGamma , {{\varvec{k}}}, RV ; v, rv, v_{rv}, \pi ) \end{aligned}$$

where \(\big (K, \varGamma , {{\varvec{k}}}; v, \pi \big )\) is a valued difference field and \( RV \) is its rv-sort. Such a structure will be called an rv-valued difference field. Any subfield \(E\) of \(K\) is viewed as a valued subfield of \(\mathcal {K}\) with valuation ring \(\mathcal {O}_E:=\mathcal {O}\cap E\).

A good substructure of \(\mathcal {K}=(K, \varGamma , {{\varvec{k}}}, RV ; v, rv, v_{rv}, \pi )\) is a quadruple \(\mathcal {E}=(E, \varGamma _{\mathcal {E}}, {{\varvec{k}}}_{\mathcal {E}}, RV _{\mathcal {E}})\) such that

  1. (1)

    \(E\) is a difference subfield of \(K\),

  2. (2)

    \(\varGamma _{\mathcal {E}}\) is an ordered abelian subgroup of \(\varGamma \) with \(v(E^\times )\subseteq \varGamma _{\mathcal {E}}\),

  3. (3)

    \({{\varvec{k}}}_{\mathcal {E}}\) is a difference subfield of \({{\varvec{k}}}\) with \(\pi (\mathcal {O}_E)\subseteq {{\varvec{k}}}_{\mathcal {E}}\),

  4. (4)

    \( RV _{\mathcal {E}}\) is a subgroup of \( RV \) with \(rv(E) \subseteq RV _{\mathcal {E}}\).

For good substructures \(\mathcal {E}_1=(E_1, \varGamma _1, {{\varvec{k}}}_1, RV _1)\) and \(\mathcal {E}_2=(E_2, \varGamma _2, {{\varvec{k}}}_2, RV _2)\) of \(\mathcal {K}\), we define \(\mathcal {E}_1\subseteq \mathcal {E}_2\) to mean that \(E_1 \subseteq E_2,\ \varGamma _1 \subseteq \varGamma _2,\ {{\varvec{k}}}_1 \subseteq {{\varvec{k}}}_2\) and \( RV _1 \subseteq RV _2\).

Throughout this subsection

$$\begin{aligned} \mathcal {K}=(K, \varGamma , {{\varvec{k}}}, RV ; v, rv, v_{rv}, \pi ), \qquad \mathcal {K}'=(K', \varGamma ', {{\varvec{k}}}', RV '; v', rv', v'_{rv}, \pi ') \end{aligned}$$

are rv-valued difference fields, with valuation rings \(\mathcal {O}\) and \(\mathcal {O}'\), and

$$\begin{aligned} \mathcal {E}=(E,\varGamma _{\mathcal {E}}, {{\varvec{k}}}_{\mathcal {E}}, RV _{\mathcal {E}}), \qquad \mathcal {E'}=(E',\varGamma _{\mathcal {E}'}, {{\varvec{k}}}_{\mathcal {E}'}, RV _{\mathcal {E}'}) \end{aligned}$$

are good substructures of \(\mathcal {K}\), \(\mathcal {K'}\), respectively. To avoid too complicated notation we let \(\sigma \) denote the difference operator of each of \(K, K', E, E'\), and put \(\mathcal {O}_{E'}:= \mathcal {O}'\cap E'\).

A good map \(\mathbf {f}: \mathcal {E} \rightarrow \mathcal {E'}\) is a quadruple \(\mathbf {f}=(f, f_{{\text {v}}}, f_{{\text {r}}}, f_{rv})\) consisting of a difference field isomorphism \(f:E \rightarrow E'\), an ordered group isomorphism \(f_{{\text {v}}}:\varGamma _{\mathcal {E}} \rightarrow \varGamma _{\mathcal {E}'}\), a difference field isomorphism \(f_{{\text {r}}}: {{\varvec{k}}}_{\mathcal {E}} \rightarrow {{\varvec{k}}}_{\mathcal {E}'}\) and a group isomorphism \(f_{rv}: RV _{\mathcal {E}} \rightarrow RV _{\mathcal {E}'}\) such that

  1. (i)

    \(f_{{\text {v}}}(v(a))=v'(f(a))\) for all \(a \in E^\times \), and \(f_{{\text {v}}}\) is elementary as a partial map between \(\varGamma \) and \(\varGamma '\);

  2. (ii)

    \(f_{{\text {r}}}(\pi (a))=\pi '(f(a))\) for all \(a \in E\), and \(f_{{\text {r}}}\) is elementary as a partial map between \({{\varvec{k}}}\) and \({{\varvec{k}}}'\);

  3. (iii)

    \(f_{rv}(rv(a))=rv'(f(a))\) for all \(a \in E^{\times }\), and \(f_{rv}\) is elementary as a partial map between \( RV _{\mathcal {E}}\) and \( RV _{\mathcal {E}'}\).

Let \(\mathbf {f}: \mathcal {E} \rightarrow \mathcal {E'}\) be a good map as above. Then the field part \(f: E \rightarrow E'\) of \(\mathbf {f}\) is a valued difference field isomorphism. Moreover \(f_{{\text {v}}}\), \(f_{{\text {r}}}\) and \(f_{rv}\) agree on \(v(E^\times )\), \(\pi (\mathcal {O}_E)\) and \(rv(E)\) with the corresponding maps induced by \(f\). We say that a good map \(\mathbf {g}= (g, g_{{\text {v}}}, g_{{\text {r}}}, g_{rv}) : \mathcal {F} \rightarrow \mathcal {F'}\) extends \(\mathbf {f}\) if \(\mathcal {E}\subseteq \mathcal {F}\), \(\mathcal {E'}\subseteq \mathcal {F'}\), and \(g\), \(g_{{\text {v}}}\), \(g_{{\text {r}}}\), \(g_{rv}\) extend \(f\), \(f_{{\text {v}}}\), \(f_{{\text {r}}}\), \(g_{rv}\), respectively. The domain of \(\mathbf {f}\) is \(\mathcal {E}\).

We say that \(\mathcal {E}\) satisfies Axiom 1 (respectively, Axiom 2) if the valued difference subfield \((E, v(E^\times ),\pi (\mathcal {O}_E);\dots )\) of \(\mathcal {K}\) does. Likewise we say that \(\mathcal {E}\) is \(\sigma \)-henselian if this valued difference subfield of \(\mathcal {K}\) is.

Regular elements will also play a role in the main theorem, for value group extensions. The same technique has been used in [12] with a different name.Footnote 5 The next result is the analog of Lemma 8.8 from [12], whose proof can be generalized to our context easily using Lemma 3.6.

Lemma 6.1

Let \(\mathcal {K}\) be a \(\kappa ^{+}\)-saturated valued difference field which satisfies Axiom 1. Suppose that \(\mathcal {E}\) is a good substructure of \(\mathcal {K}\) with \({{\varvec{k}}}_{\mathcal {E}} < \kappa \). Let \(\gamma \in \varGamma \), \(\gamma \notin v(E^{\times })\). Then

  1. (i)

    there is \(a \in K\) with \(v(a)=\gamma \) which is regular over \(E\);

  2. (ii)

    The value group of \(E\langle a \rangle \) is \(v(E^\times )\langle \gamma \rangle \), and its residue field is the same as the residue field of \(E\);

  3. (iii)

    if \(b\in K\) is regular over \(E\) with \(v(a)=\gamma '\) and the ordered difference groups \(v(E^\times )\langle \gamma \rangle \) and \(v(E^\times )\langle \gamma ' \rangle \) are isomorphic via the map sending \(\gamma \) to \(\gamma '\) then there is a valued difference field isomorphism between \(E\langle a \rangle \) and \(E\langle b \rangle \) sending \(a\) to \(b\).

Theorem 6.2

Suppose \({\text {char}}({{\varvec{k}}})=0\), \(\mathcal {K}\), \(\mathcal {K}'\) satisfy Axiom \(2\) and are \(\sigma \)-henselian. Then any good map \(\mathcal {E} \rightarrow \mathcal {E}'\) is a partial elementary map between \(\mathcal {K}\) and \(\mathcal {K}'\).

Proof

The theorem holds trivially for \(\varGamma =\{0\}\), so assume that \(\varGamma \ne \{0\}\). Let \(\mathbf {f}=(f, f_{{\text {v}}}, f_{{\text {r}}}, f_{rv}): \mathcal {E} \rightarrow \mathcal {E}'\) be a good map. By passing to suitable elementary extensions of \(\mathcal {K}\) and \(\mathcal {K}'\) we may assume that \(\mathcal {K}\) and \(\mathcal {K}'\) are \(\kappa \)-saturated, where \(\kappa \) is an uncountable cardinal such that \(|{{\varvec{k}}}_{\mathcal {E}}|,\ |\varGamma _{\mathcal {E}}| < \kappa \). We say that a good substructure \(\mathcal {E}_1=(E_1,{{\varvec{k}}}_1, \varGamma _1, RV _1)\) of \(\mathcal {K}\) small if \(|{{\varvec{k}}}_1|,\ |\varGamma _1|<\kappa \). We shall prove that the good maps with small domain form a back-and-forth system between \(\mathcal {K}\) and \(\mathcal {K}'\), which suffices to obtain the theorem. In other words we shall prove that under the present assumptions on \(\mathcal {E}\), \(\mathcal {E}'\) and \(\mathbf {f}\), there is for each \(a \in K\) a good map \(\mathbf {g}\) extending \(\mathbf {f}\) such that \(\mathbf {g}\) has small domain \(\mathcal {F}=(F,\ldots )\) with \(a\in F\). We achieve this by appropriately iterating Corollary 5.10, and the extension procedures described below which correspond to extending the residue field and value group. We will use results from [2] to extend the residue field which have been used in different contexts in [1] and [12].

  1. (1)

    Given \(\alpha \in {{\varvec{k}}}\), arranging that \(\alpha \in {{\varvec{k}}}_{\mathcal {E}}\). By saturation and the definition of “good map” this can be achieved without changing \(f\), \(f_{{\text {v}}}\), \(f_{rv}\), \(E\), \(\varGamma _{\mathcal {E}}\), \( RV _{\mathcal {E}}\) by extending \(f_{{\text {r}}}\) to a partial elementary map between \({{\varvec{k}}}\) and \({{\varvec{k}}}'\) with \(\alpha \) in its domain. In the same way we obtain the next two results.

  2. (2)

    Given \(\gamma \in \varGamma \), arranging that \(\gamma \in \varGamma _{\mathcal {E}}\).

  3. (3)

    Given \(r\in RV \), arranging that \(r \in RV _{\mathcal {E}}\).

  4. (4)

    Arranging \({{\varvec{k}}}_{\mathcal {E}}=\pi (\mathcal {O}_E)\). Suppose \(\alpha \in {{\varvec{k}}}_{\mathcal {E}},\ \alpha \notin \pi (\mathcal {O}_E)\); set \(\alpha ':= f_{{\text {r}}}(\alpha )\).

If \(\alpha \) is \(\bar{\sigma }\)-transcendental over \(\pi (\mathcal {O}_E)\), we pick \(a\in \mathcal {O}\) and \(a'\in \mathcal {O}'\) such that \(\bar{a}=\alpha \) and \(\bar{a'}=\alpha '\), and then Lemma 2.5 from [2] yields a good map \(\mathbf {g}=(g, f_{{\text {v}}}, f_{{\text {r}}}, f_{rv})\) with small domain \((E \langle a \rangle , \varGamma _{\mathcal {E}}, {{\varvec{k}}}_{\mathcal {E}}, RV _{\mathcal {E}})\) such that \(\mathbf {g}\) extends \(\mathbf {f}\) and \(g(a)=a'\).

Next, assume that \(\alpha \) is \(\bar{\sigma }\)-algebraic over \(\pi (\mathcal {O}_E)\). Let \(G(x)\) be a \(\sigma \)-polynomial over \(\mathcal {O}_E\) such that \(\bar{G}(x)\) is a minimal \(\bar{\sigma }\)-polynomial of \(\alpha \) over \(\pi (\mathcal {O}_E)\) and has the same complexity as \(G(x)\). Pick \(a\in \mathcal {O}\) such that \(\bar{a}=\alpha \). Then \(G\) is \(\sigma \)-henselian at \(a\). So we have \(b \in \mathcal {O}\) such that \(G(b)=0\) and \(\bar{b}=\bar{a}=\alpha \). Likewise we obtain \(b'\in \mathcal {O}'\) such that \(f(G)(b')=0\) and \(\bar{b'}=\alpha '\), where \(f(G)\) is the difference polynomial over \(E'\) that corresponds to \(G\) under \(f\). By Lemma 2.6 of [2] we obtain a good map extending \(\mathbf {f}\) with small domain \((E \langle b \rangle , \varGamma _{\mathcal {E}}, {{\varvec{k}}}_{\mathcal {E}}, RV _{\mathcal {E}})\) and sending \(b\) to \(b'\).

Iterating (4) we may assume that \({{\varvec{k}}}_{\mathcal {E}}=\pi (\mathcal {O}_E)\). We refer from now on to \({{\varvec{k}}}_{\mathcal {E}}\) as the residue difference field of \(E\). Since \(\mathcal {K}\) satisfies Axiom 2, appropriately iterating (1) and (4), we may assume in addition that \(\mathcal {E}\) satisfies Axiom 2, and consequently Axiom 1.

  1. (5)

    Arranging \(\varGamma _{\mathcal {E}}=v(E^\times )\).

Suppose \(\gamma \in \varGamma _{\mathcal {E}}\), \(\gamma \notin v(E^\times )\). By Lemma 6.1 we can take \(b \in K\) such that \(v(b)=\gamma \) and \(b\) is regular over \(K\). By (3) we may assume \(r=rv(b) \in RV _{\mathcal {E}}\). Let \(r'=f_{rv}(r) \in \mathcal {K}'\) and pick \(b' \in \mathcal {K}'\) with \(rv(b')=r'\). Then \(b'\) is regular over \(E'\) and we can extend \(\mathbf {f}\) by mapping \(b\) to \(b'\), again by Lemma 6.1.

Iterating (5) we assume in the rest of the proof that \(\varGamma _{\mathcal {E}}=v(E^\times )\). This condition is actually preserved in the earlier extension procedures (4). We refer from now on to \(\varGamma _{\mathcal {E}}\) as the value group of \(E\). Note also that in the extension procedure (5) the residue difference field does not change.

Now let \(a \in K\) be given. We want to extend \(\mathbf {f}\) to a good map whose domain is small and contains \(a\). By our previous remarks \({{\varvec{k}}}_{\mathcal {E}}=\pi (\mathcal {O}_E)\), \(\varGamma _{\mathcal {E}}=v(E^\times )\), and \(\mathcal {E}\) satisfies Axiom 2. Appropriately iterating and alternating the above extension procedures we can arrange in addition that \(E\langle a \rangle \) is an immediate extension of \(E\). Let \(\mathcal {E} \langle a \rangle \) be the valued difference subfield of \(\mathcal {K}\) that has \(E\langle a \rangle \) as underlying difference field. By Corollary 5.10, \(\mathcal {E} \langle a \rangle \) has a maximal immediate valued difference field extension \(\mathcal {E}_1\le \mathcal {K}\). Then \(\mathcal {E}_1\) is a maximal immediate extension of \(\mathcal {E}\) as well. Applying Corollary 5.10 to \(\mathcal {E}'\) and using Theorem 5.8 we can extend \(\mathbf {f}\) to a good map with domain \(\mathcal {E}_1\), construed here as a good substructure of \(\mathcal {K}\) in the obvious way. Of course, \(a\) is in the underlying difference field of \(\mathcal {E}_1\).\(\square \)

7 Equivalence and relative quantifier elimination

Here we state the model theoretic consequences of the Theorem 6.2. All these consequences are obtained by standard model theoretic considerations which has been done in detail repeatedly in the context of valued difference fields, see [1, 2, 4, 12]. We use the symbols \(\equiv \) and \(\preceq \) for the relations of elementary equivalence and being an elementary submodel, in the setting of many-sorted structures. In this section

$$\begin{aligned} \mathcal {K}=(K, \varGamma , {{\varvec{k}}}, RV ; \ldots ), \qquad \mathcal {K}'=(K', \varGamma ', {{\varvec{k}}}', RV '; \ldots ) \end{aligned}$$

are rv-valued difference fields of residue characteristic \(0\) that satisfy Axiom \(2\) and are \(\sigma \)-henselian. We consider them as \(\mathcal {L}\)-structures where \(\mathcal {L}\) is the 4-sorted language described in the previous section. Note that \(\varGamma \) and \({{\varvec{k}}}\) are interpretable in \( RV \), hence:

Theorem 7.1

\(\mathcal {K} \equiv \mathcal {K}'\) if and only if \( RV \equiv RV '\).

The Hahn difference field \({{\varvec{k}}}((t^\varGamma ))\) can be expanded to an rv-valued difference field in the natural way and, by the above result, it is elementarily equivalent to \(\mathcal {K}\).

Theorem 7.2

Let \(\mathcal {E}=(E, \varGamma _E, {{\varvec{k}}}_E, RV _E;\dots )\) be a \(\sigma \)-henselian rv-valued difference subfield of \(\mathcal {K}\) such that \( RV _E\preceq RV \). Then \(\mathcal {E} \preceq \mathcal {K}\).

Theorem 7.3

Let \(\mathcal {T}\) be the \(\mathcal {L}\)-theory of \(\sigma \)-henselian valued difference fields with residue characteristic 0. Then every \(\mathcal {L}\)-formula \(\phi \) is equivalent (modulo \(\mathcal {T}\)) to an \(\mathcal {L}\)-formula \(\psi \) in which all occurences of field variables are free.

Cross section and angular component maps Let \(\mathcal {K}=(K, \varGamma , {{\varvec{k}}};v,\pi )\) be a valued field. A cross-sectional map is a group homomorphism \(c:\varGamma \rightarrow K^{\times }\) such that \(v(c(\gamma ))=\gamma \), for all \(\gamma \in \varGamma \). An angular component map is a multiplicative group homomorphism \(ac: K^{\times } \rightarrow {{\varvec{k}}}^{\times }\) which agrees with the residue class map \(\pi \) on \(\mathcal {O}{\setminus } \mathfrak {m}\). We can extend an angular component map to \(K\) by setting \(ac(0)=0\). In the presence of a cross section the rv-sort is interpretable in \(\mathcal {K}=(K, \varGamma , {{\varvec{k}}}; v,\pi , c)\) by taking \(rv:K^{\times } \rightarrow k^{\times } \times \varGamma \) with \(rv(a)=(\pi (a/c(v(a))), v(a))\). Similarly, when \(K\) is equipped with an angular component map the rv-sort is interpretable in \(\mathcal {K}=(K,\varGamma ,{{\varvec{k}}};v,\pi ,ac)\) via \(rv(a)=(ac(a),v(a))\). Evert valued field has elementary extension which admits cross section and an angular component map.

If \(\mathcal {K}\) is a valued difference field we ask that cross-sectional and angular component maps are compatible with the distinguished automorphism \(\sigma \). Therefore it seems quite unlikely that an arbitrary valued difference field admits a cross section or an angular component map in an elementary extensionsFootnote 6. However many natural examples of valued difference fields can be equipped with cross section and angular component maps, and so it is worthwhile stating the consequences of the above results in the presence of a cross-sectional or an angular component mapFootnote 7.

Theorem 7.4

Let \(\mathcal {K}, \mathcal {K'}\) be \(\sigma \)-henselian valued difference fields with residue characteristic zero which are either both equipped with a cross section or both equipped with an angular component map. Then \(\mathcal {K}\equiv \mathcal {K}'\) if and only if \({{\varvec{k}}}\equiv {{\varvec{k}}}'\) and \(\varGamma \equiv \varGamma '\).

Theorem 7.5

Let \(\mathcal {L}_c\) and \(\mathcal {L}_{ac}\) be the expansions of the 3-sorted language of valued difference fields with a cross section and with an angular component map, respectively. Let \(\mathcal {T}_c\) and \(\mathcal {T}_{ac}\) be the theories of \(\sigma \)-henselian valued difference fields with residue characteristic 0 in the language \(\mathcal {L}_c\) and \(\mathcal {L}_{ac}\), respectively. Then every \(\mathcal {L}_c\)-formula \(\phi \) is equivalent (modulo \(\mathcal {T}_c\)) to an \(\mathcal {L}_c\)-formula \(\psi \) in which all occurrences of field variables are free, and every \(\mathcal {L}_{ac}\)-formula \(\phi \) is equivalent (modulo \(\mathcal {T}_{ac}\)) to an \(\mathcal {L}_{ac}\)-formula \(\psi \) in which all occurrences of field variables are free.

8 Applications to transseries

We refer the reader to [13] for all definitions, conventions and basic facts regarding transseries. Let \(\mathbb {T}\) be a field of transseries (grid based or well based) in \(x\). Monomials of \(\mathbb {T}\) (with coefficient 1) form an ordered multiplicative group. Let \(\varGamma \) be this group monomials, seen as an additive group and equipped with the reverse of the ordering on monomials. Then we define the valuation of an element \(f(x) \in \mathbb {T}\) as the minimum (in the sense of the reversed ordering) of the support of \(f(x)\). So we have

$$\begin{aligned} v(e^x)<<v(x)<<v(log(x))<<v(1)=0<v(x^{-1})<<v(e^{-x}) \end{aligned}$$

where \(\gamma <<\gamma '\) is a shorthand for \(n\gamma <\gamma '\) for all \(n>0\). Note that the residue field of \(\mathbb T\) is isomorphic to the field of constants of \(\mathbb T\) which is really closed. Clearly \(\mathbb T\) admits a cross-sectional map; simply send \(\gamma \in \varGamma \) to the monomial with coefficient \(1\) and valuation \(\gamma \).

Let \(g(x)\) be an infinite positive element of \(\mathbb T\). Then we obtain an automorphism of \(\mathbb T\) via sending \(f(x)\) to \(f(g(x))\) which is obtained from \(f(x)\) by uniformly substituting \(x\) by \(g(x)\). By proposition 5.10 of [13] such automorphisms are asymptotic which, in terms of the valuation, means that they fix the valuation ring of \(\mathbb T\) setwise. Now let \(\sigma \) be the automorphism of \(\mathbb T\) given by right composition with \(g(x)=x+1\), and consider \(\mathbb T\) as a valued difference field equipped with a cross section \((\mathbb T, \varGamma , {{\varvec{k}}}; v, \pi , c)\) with distinguished automorphism \(\sigma \). Note that \(\bar{\sigma }\) is the identity, and hence the equation

$$\begin{aligned} \bar{\sigma }(x)-x+1=0 \end{aligned}$$

has no solution in \({{\varvec{k}}}\). On the contrary the action of \(\sigma \) on the value group is rather complex;

$$\begin{aligned} v(\sigma (e^x))=v(e^x), \quad v(\sigma (e^{x\mathrm{log}x}))=v(e^{x\mathrm{log}x})+v(x), \quad v(\sigma (e^{x^2})=v(e^{x^2})+v(e^x) \end{aligned}$$

and as such does not fit in any of contexts studied in [1, 4] and [12].

We now introduce a coarsening of \(v\), whose residue difference field will be linear difference closed. Let

$$\begin{aligned} \varDelta :=\{\gamma \in \varGamma : v(e^x)<<\gamma <<v(e^{-x})\}. \end{aligned}$$

Then \(\varDelta \) is a convex subgroup of \(\varGamma \), and moreover if \(v(f(x)) \in \varDelta \) then so is \(v(\sigma (f(x))\). Therefore we obtain a valued difference field equipped with a cross section

$$\begin{aligned} \mathbb {T}_\varDelta :=(\mathbb T, \varGamma _w, {{\varvec{k}}}_w;w,\pi _w, c_w) \end{aligned}$$

where \(w: \mathbb {T}^{\times } \rightarrow \varGamma _w=\varGamma /\varDelta \) is the coarsening of \(v\) by \(\varDelta \). Let \(K_w\) be the difference subfield of \(\mathbb T\) which consists of elements \(f(x)\) whose support is contained in \(\varDelta \). Then \(K_w\) is isomorphic to \({{\varvec{k}}}_w\) via the restriction of the residue class map \(\pi _w\). In order to show that \(K_w\) is linear difference closed we will use the differential operator \(\partial \) on \(\mathbb T\), as introduced in Chapter 5 of [13], which has a functional inverse \(\int \) and is compatible with composition and exponentiation. Next we list a few conclusions from Proposition 5.11 of [13] and its proof.

Lemma 8.1

For all \(f(x) \in K_w\) we have:

  1. (i)

    \(\partial f(x) \in K_w\);

  2. (ii)

    \(f(x+1)=f(x)+\partial f(x)+ \partial ^2f(x)/2!+\partial ^3f(x)/3!+\cdots \);

  3. (iii)

    \(v(\partial \mathrm{log}f(x))>0\).

Hence \(\sigma (f(x))=e^{\partial }f(x)\) where \(e^\partial \) is seen as an operator in \(K_w[[\partial ]]\). Now let \(h_0,\ldots , h_n \in K_w\), with \(h_i \ne 0\) for some \(i\), and consider the linear difference equation

$$\begin{aligned} h_0+h_1\sigma (f(x))+\cdots +h_n\sigma ^n(f(x))=1 \end{aligned}$$

We represent this equation as an (infinite order) linear differential equation:

$$\begin{aligned} Lf(x)=1 \end{aligned}$$

where \(L=h_0+h_1e^\partial +\cdots +h_ne^{n\partial } \in K_w[[\partial ]]\) is nonzero. A formal inverse \(L^{-1}\) of \(L\) can be found in the ring \(K_w[[\partial ]][\int ]\). Note that it is possible to have the constant term of \(L\) equal to zero and then one would need the inverse of \(\partial \) (which is \(\int \)) to find \(L^{-1}\). See flat discrete summation in [14] for a specific example worked out in detail. By part (iii) of Lemma 8.1, the formal operator \(L^{-1}\) indeed acts on \(K_w\) and so we can find a solution to the equation \(Lf(x)=1\) by choosing \(f(x)=L^{-1}(1) \in K_w\). Therefore \(K_w\) is linear difference closed.

Remark 8.2

The fact that \(K_w\) is linear difference closed is actually implicit in Chapter 7 of [13]. One can generalize the Newton polygon method for finite-order linear differential operators to linear differential operators like \(L\) above and indeed obtain much more than what we proved.

Theorem 8.3

\(\mathbb {T}_\varDelta \) is \(\sigma \)-henselian.

Proof

Since \(\sigma (f(x))=f(x+1)\), exponentiality of \(f\) and \(\sigma (f)\) is the same, exercise 5.13 of [13]. Also, \(\mathbb T\) is the union of Hahn fields

$$\begin{aligned} \mathbb {L}_0 \subseteq \mathbb {L}_1 \subseteq \mathbb {L}_2 \cdots \end{aligned}$$

where \(\mathbb {L}_{i+1}\) is obtained from \(\mathbb {L}_i\) by taking exponentials (see [13] page 98). Therefore \(\sigma \) is an automorphism of each \(\mathbb {L}_i\), and \(\mathbb {T}\) is the directed union of the valued difference subfields \(\mathbb {L}_i\). Since \(K_w \subseteq \mathbb {L}_0\), the residue difference field of \(\mathbb {L}_i\) is \({{\varvec{k}}}_w\) and by the above discussion \(\mathbb {L}_i\) satisfies Axiom 2 for all \(i\). Now, since each \(\mathbb {L}_i\) is maximal, we can use Corrollary 5.6 to conclude that they are \(\sigma \)-henselian. Note that \(\sigma \)-henselianity is a universal–existential first-order property and such properties are preserved in unions of chains. Therefore \(\mathbb {T}\) is \(\sigma \)-henselian.\(\square \)

Thus the results of the previous section are applicable, in particular:

Corollary 8.4

\(\mathbb {T}_\varDelta \) is elementarily equivalent to the Hahn difference field \({{\varvec{k}}}_w((t^{\varGamma _w}))\) (equipped with its natural cross section).

In this section we considered the particular automorphism \(\sigma (f(x))=f(x+1)\) but indeed one can carry out the arguments above for any \(\sigma \) which is given by right composition with \(g(x)\) where \(g(x)\) is an infinite positive transseries of exponential and logarithmic depth zero. For that general case one still considers the coarsening above, and the only difference would be to explicitly follow Remark 8.2 instead of the discussion which precedes it.