!newop an
!newop id
!newop dom
!newop st
!newop sign
!newtuple X
!newtuple Y
!renewtuple Z
!newtuple w
!newtuple x
!newtuple y
!newtuple z
!renewtuple a
!renewtuple b
!renewtuple c
!newtuple s
!renewtuple k

\newcommand{\Ran}{\R_{\an}}
\newcommand{\Lan}{L_{\an}}
\newcommand{\Tan}{T_{\an}}
\newcommand{\RanD}{\R_{\an}^D}
\newcommand{\LanD}{L_{\an}^D}
\newcommand{\TanD}{T_{\an}^D}
\providecommand{\alphabar}{\overline{\alpha}}
\providecommand{\etabar}{\overline{\eta}}
\renewcommand{\int}{\"int}

\title{Model completeness and o-minimality of $\Ran$}
\maketitle

Notes on the Denef - van den Dries quantifier elimination for $\Ran$ and its 
consequences, written for a pair of seminars in Muenster, January 2018.

These notes are based in large part on some lecture notes by Alex Wilkie on 
the topic, currently available at:
\url{http://www.logique.jussieu.fr/modnet/Publications/Introductory\%20Notes\%20and\%20surveys/Wilkie.pdf}

A reader who has stumbled upon these notes and has not read Wilkie's notes 
should stop reading now and seek out Wilkie's notes instead. In these notes I 
attempt to spell out the odd thing left implicit in Wilkie's notes, but 
essentially these notes cover a proper subset of the material covered in 
Wilkie's notes, skip over many details handled nicely there, and indubitably 
add errors and imprecisions of their own.

## Analytic functions

# Formal power series

For $R$ a ring,
\[ R[[X]] := \{ \sum_{i (- \N} a_iX^i : a_i (- R \} \]
\[ R[[\X]] = R[[X_1,...,X_n]] = (...((R[[X_1]])[[X_2]])...)[[X_n]] \]

If $F (- R[[\X]]$, we can write
\[ F = \sum_{\nu (- \N^n} a_\nu \X^\nu \]
where $\X^\nu := X_1^{\nu_1}...X_n^{\nu_n}$.

$|\nu| := \max_i \nu_i$.

$F(0) :=$ constant term of $F = a_0$

For $R$ a ring, $R^* := \{ x (- R : \exists y (- R\. xy=1 \} =$ multiplicative 
group of units.
Lemma:
    For $F (- R[[\X]]$, $F (- R[[\X]]^*$ iff $F(0) (- R^*$.
    .
Proof:
    By induction, suffices to show when $\X=X$ is a single variable.

    If $FG = 1$ then $F(0)G(0)=1$.
    
    If $F = \sum a_iX^i$
    If $a_0b_0=1$, then define recursively for $n>=0$
    \[ b_{n+1} := -a_0^{-1}(a_1b_n + a_2b_{n-1} + ... a_{n+1}b_0) .\]
    Then $\sum_{0<=i<=n+1} a_ib_{n+1-i} = 0$,
    so $(\sum a_iX^i)(\sum b_iX^i) = 1$.
    .

# Convergent power series

For $F (- \R[[\X]]$, define
*\[a* \dom(\sum a_\nu\X^\nu)
  &:= \int( \{ \x (- \R^n : \sum a_\nu\x^\nu \mbox{ converges } \} ) \\\
    & = \int( \{ \x : \{ a_\nu\x^\nu : \nu \} \mbox{ is bounded } \} ) *a\]*

e.g. $\dom( \sum_\nu X^\nu Y^\nu ) = \{ (x,y) : xy < 1 \}$.

Let $\R<{ \X }> := \{ F : 0 (- \dom(F) \}$.

Fact:
    $\R<{ \X }>$ is a subring of $\R[[\X]]$.
    .

Now $F = \sum a_\nu \X^\nu (- \R<{ \X }>$ defines a function $~F : \dom(F) --> 
\R$; $~F(\x) := \sum a_\nu \x^\nu$.

Fact:
    $~F=0$ iff $F=0$.
    $~F (- C^\infty(\dom(F))$.
    .

Say $f : U --> \R$ is #analytic# at $\b (- U$
if $f(\X-\b) = ~F(\X)$ on $U_\b$, some $\b (- U_\b (=_{\"op} U$ and some $F (- 
\R<{ \X }>$.

Fact:
    $~F$ is analytic at every $b (- \dom(F)$.
    .
Proof[Idea of proof]:
    show the Taylor series at $b$,
    \[ \sum_\nu 1/((\sum\nu)!) \~{D^{\nu}F}(b) X^\nu \]
    where $D^{\nu} = D_1^{\nu_1}...D_n^{\nu_n}$ where $D_i = d/dX_i$ is formal 
    derivation,
    converges near $b$.
    See [Krantz-Park "A primer of Real Analytic Functions" Proposition 2.2.7].
    .

Fact:
    if $f$ is analytic at $b$ and $g$ is analytic at $f(b)$,
    then $(g \circ f)$ is analytic at $b$.
    .

Corollary:
    \[ \R<{ \X }>^* = \R[[\X]]^* \cap \R<{ \X }> \]
    .
Proof:
    Suppose $F (- \R<{ \X }>$ has non-zero constant term;
    WTS $F$ is invertible in $\R<{ \X }>$.
    Multiplying $F$ by a constant, WMA $F(0)=1$.
    So say $F = 1-G$ where $G (- \R[[\X]]$ with $G(0)=0$.
    Let $H(X) := \sum X^i (- \R<{ X }>$.
    Then $(1-X)H(X) = 1$,
    so $F(H\circ G) = F(\X)(H(G(\X)) = (1+G(\X))(H(G(\X))) = 1$
    and $H \circ G (- \R<{ \X }>$ by the Fact.
    .

# Weierstrass Preparation

Say $F (- \R[[\X,Y]]$ is #regular# in $Y$
if some term $aY^p$ with $p>=0$ and $a/=0$ occurs in the power series $F$,
i.e. if ``$F(0,Y) /= 0$''.

Fact[Weierstrass Preparation Theorem]:
    If $F (- \R<{ \X,Y }>$ is regular in $Y$,
    then exists $Q (- \R<{ \X,Y }>^*$ and $L (- \R<{ \X }>[Y]$,
    such that $F = QL$.
    .
    
# Denef - van den Dries Preparation

Fact:
    $\R<{ \X }>$ is Noetherian; that is, any ideal is finitely generated.
    .

Fact:
    The embedding $\R<{ \X }> <= \R[[X]]$ is faithfully flat.
    .

I omit the definition of faithful flatness, because in fact we need only the 
following consequence.
Fact{cor:fflatlinear}:
    If $F_i$,$F (- \R<{ \X }>$
    and the linear equation $F_1x_1 + ... F_nx_n = F$
    has a solution in $\R[[\X]]$,
    then it already has a solution in $\R<{ \X }>$.
    .

Corollary{cor:fflatlinearUnit}:
    If $F_i$,$F (- \R<{ \X }>$
    and the linear equation $F_1x_1 + ... F_nx_n = F$
    has a solution in $\R[[\X]]^*$,
    then it already has a solution in $\R<{ \X }>^*$.
    .
Proof:
    Say $U_i (- \R[[\X]]^*$ is a solution.
    Then $\sum_i (F_i)(U_i(0) + \sum_j x_i^j X_j) = F$
    has a solution in $\R[[\X]]$,
    hence in $\R<{ \X }>$.
    So since $U_i(0) /= 0$,
    the original equation has a solution in $\R<{ \X }>^*$.
    .

The following consequence of these facts is what we will need in the QE proof; 
I follow Wilkie in naming it as follows.

Theorem[Denef - van den Dries Preparation Theorem]:
    If $F (- \R<{ \X,\Y }>$
    then $F(\X,\Y) = \sum_{|\nu| < d} a_\nu(\X) \Y^\nu u_\nu(\X,\Y)$
    for some $d (- \N$, $a_\nu (- \R<{ \X }>$, $u_\nu (- \R<{ \X,\Y }>^*$.
    .
Proof:
    By induction on the length of $\Y$.
    So suppose for $\R<{ \X,\Y }>$; we prove it for $\R<{ \X,\Y,Z }>$.
    Let $F = \sum_{i \in \N} a_iZ^i (- \R<{ \X,\Y,Z }>$, $a_i (- \R<{ \X,\Y 
    }>$.
    $\R<{ \X,\Y }>$ is Noetherian, so there exist $d (- \N$ and $b_{i,j} (- \R<{ \X,\Y }>$
    such that $a_{d+i} = \sum_{i<d} b_{i,j} a_i$.
    So
    *\[a* F &= \sum_{i<d} a_iZ^i + \sum_{j>=0} \sum_{i<d} b_{i,j}a_iZ^{d+j} \\\
    &= \sum_{i<d} a_iZ^i + \sum_{i<d} a_i Z^i Z^{d-i} \sum_{j>=0} b_{i,j}Z^j 
    \\\
        &= \sum_{i<d} (a_iZ^i)(1 + Z^{d-i} \sum_{j>=0} b_{i,j}Z^j) \\\
        &= \sum_{i<d} a_iZ^iu_i *a\]*

    Here we have $u_i (- \R[[\X,\Y,Z]]^*$, and then by 
    Corollary~\ref{cor:fflatlinearUnit},
    we can find such $u_i (- \R<{ \X,\Y,Z }>^*$.

    Now apply the inductive hypothesis to the $a_i$.
    .

## $\Ran$

\[ ||\x|| := max_i |x_i| \]
\[ B_{<r} := \{ \x (- \R^n : ||\x|| < r \} \]
\[ B_{<=r} := \{ \x (- \R^n : ||\x|| <= r \} \]

For $r>0$,
\[ \R\{\X\}_r := \{ F (- \R[[\X]] : B_{<=r} (= \dom(F) \} ,\]
so $\R<{ \X }> = \cap_{r (- \R_{>0}} \R\{\X\}_r$.

If $F (- \R\{\X\}_r$,
\[ ~F|_r(\x) := \begin{cases}
            ~F(\x)  & \mbox{if } \x (- B_{<r} \\\
             0      & \mbox{else }
             \end{cases} \]
"restricted analytic function".

Say $(r,F)$ is #acceptable# if $r (- \R_{>0}$ and $F (- \R\{X\}_r$.

\[ \Ran := \{ \R; +,-,\cdot,<, (a)_{a (- \R}, (~F|_r)_{(r,F) acceptable} \} \]
structure in language $\Lan$.

Let $\LanD := \Lan \cup \{D\}$, and $\RanD :=$ expansion of $\Ran$ 
interpreting $D$ by
    \[ D(x,y) := \begin{cases}
            x/y &\mbox{if } y!=0 \\\
            0   &\mbox{if } y=0 \end{cases} \]

Theorem[Denef - van den Dries]:
    $\TanD := Th(\RanD)$ has QE.
    .

Corollary:
    $\Tan := Th(\Ran)$ is model complete.
    .
Proof:
    Any qf $\LanD$-formula is equivalent to an existential $\Lan$-formula.
    
    For example, if $t_1,t_2$ are terms, then
    \[ \phi(D(t_1(x),t_2(x)))
        <=> \exists z\. ( \phi(z) /\
            ( (t_2(x) = 0 /\ z=0) \/ (t_2(x) != 0 /\ z\cdot t_2(x) = t_1(x)) ) 
            ). \]
    .

Remark:
    Model completeness of $\Ran$ was previously proven (expressed in different
    but equivalent terms) by Gabrielov in the 1960s
    ("theorem of the complement" for subanalytic sets).

    %% Y (= \R^n is _semi-analytic_
    %% if every b (- \R^n has an open neighbourhood U_b such that
    %% U_b \cap Y is a boolean combination of sets
    %% { f(x) > 0 } with f analytic at b.
    %% 
    %% Exercise: Y (= B_<=r is qf-definable in \Ran iff semi-analytic.
    %%
    %% Z (= \R^n is _sub-analytic_
    %% if every b (- \R^n has an open neighbourhood U_b such that
    %% U_b \cap Z is the image under a co-ordinate projection
    %% of a bounded semi-analytic set.
    %%
    %% Exercise: Y (= B_<=r is existentially definable in \Ran iff
    %% sub-analytic.
    %%
    %% Theorem[Gabrielov, 1960s]: if Z is sub-analytic, so is \R^n \\ Z.
    %%
    %% Exercise: This is *equivalent* to model completeness of \Ran.
    .


# o-minimality of $\Ran$

Lemma{lem:omin1}:
    Suppose $0 /= F (- \R<{ X }>$.
    Then $F = X^mG$ for some unique $m (- \N$ and $G (- F[[X]]^*$,
    and $\dom(G) = \dom(F)$,
    and for some $\epsilon>0$,
    $~F$ has constant non-zero sign on $(0,\epsilon)$.
    .
Proof:
    Existence and uniqueness of $m$,$G$ is immediate from the description of 
    $F[[X]]^*$.
    For $\dom(G) = \dom(X^mG)$:
    given $x (- \R$, $\{ a_ix^i \}$ is bounded iff $\{ a_ix^{m+i} = 
    x^m(a_ix^i) \}$ is.

    Now $G$ has non-zero constant term and $~G$ is continuous, so $~G$ and hence $~F$
    has constant non-zero sign on some $(0,\epsilon)$.
    .

Lemma{lem:omin2}:
    Let $t(x)$ be an $\LanD$-term in 1 variable.
    Exists $\epsilon > 0$ s.t.
    $t(x) = 0$ on $(0,\epsilon)$
    or $t(x) = (x^m~F(x))$ on $(0,\epsilon)$
    for some $m (- \Z$ and $F (- \R[[X]]^* \cap \R\{X\}_\epsilon$.
    In particular, $t(x)$ has constant sign on $(0,\epsilon)$.
    .
Proof:
    By induction on terms.
    Obvious for $t(x)=x$ or $t(x)=b$.

    Suppose $t(x) = t_1(x)+t_2(x)$ and $t_i(x)$ are as required.
    If either $t_i(x) = 0$ on $(0,\epsilon_i)$, this is clear.
    Else, say $t_i(x) = x^{m_i}~F_i(x)$ on $(0,\epsilon_i)$
    with $F_i (- \R[[X]]^* \cap \R\{X\}_{\epsilon_i}$.
    Say $m_1 <= m_2$.
    then $t_1(x)+t_2(x) = x^{m_1}(~F_1(x) + x^{m_2-m_1}~F_2(x))$;
    but by Lemma~\ref{lem:omin1}, $F_1(X) + X^{m_2-m_1}F_2(X) = X^kG(X)$ say,
    and then $t_1(x)+t_2(x) = x^{m_1+k}~G(x)$ is as required
    with $\epsilon := \min_i \epsilon_i$.
    
    Similarly for $-$.
    Similarly for $*$ and $D$, since the product or ratio of two units is a unit.
    
    Finally, suppose $(F,r)$ is acceptable and
    $t(x) = ~F|_r(t_1(x),...,t_n(x))$
    Pick common $\epsilon$ for the $t_i$.
    If $t_i = 0$ on $(0,\epsilon)$, replace $F$ with $F(x_1,...,0,...,x_n)$.
    So WMA $t_i(x) = f_i(x)$ on $(0,\epsilon)$,
    where $f_i(x) = x_i^{m_i}~F_i(x)$
    for some $F_i (- \R[[X]]^* \cap \R\{X\}_\epsilon$.
    If any $m_i < 0$, then $t(x) = 0$ near 0 so done.
    Reducing $\epsilon$ further, WMA $r - |f_i(x)|$ has constant sign on
    $(0,\epsilon)$ by Lemma~\ref{lem:omin1}.
    If any such sign is not positive, again $F = 0$ so done.
    Else, $|f_i(0)| <= r$, so $(f_1(0),...,f_n(0)) (- B_{<=r} (= \dom(F)$.
    Then $f(x) := ~F(f_1(x),...,f_n(x))$ is analytic at 0,
    so done by Lemma~\ref{lem:omin1}.
    .

Corollary[Corollary of QE]:
    $\Tan$ is o-minimal.
    .
Proof:
    Any qf formula in $\RanD$ is equivalent to a boolean combination of
    $\{ t(x) > 0 \}$ for $t$ an $\LanD$-term in one variable,
    so STS for any such $t$ there is a partition of $\R$ into finitely many
    points and intervals such that $\sign(t(x))$ is constant on each.

    Applying Lemma~\ref{lem:omin2} to $t(D(1,x))$ and $t( -D(1,x) )$,
    $t(x)$ has constant sign on some $(-\infty,a)$ and $(b,\infty)$.
    Then for $c (- [a,b]$,
    by Lemma~\ref{lem:omin2} applied to $t(x - c)$ and $t(x - (-c))$,
    for some $\epsilon > 0$,
    $t(x)$ has constant sign on $(c - \epsilon,c)$, $\{c\}$, and 
    $(c,c+\epsilon)$.
    
    We conclude by compactness of $[a,b]$.
    .


## Proof of QE

# QE criterion

Fact:
    $T$ has QE iff:
    if $M_1,M_2 |= T$ are $\omega$-saturated
    with a common f.g. substructure $A$,
    and if $b (- M_1$,
    then there exists an embedding $<{ Ab }>^{M_1} (-> M_2$ extending $\id_A$.
    .

So let $M_1,M_2 |= \TanD$ be $\omega$-saturated
with a common f.g. substructure $K$,
and $b (- M_1$.
Note $K <= M_1$ is a subfield and $\RanD$ is a substructure of $K$.

Lemma:
    If there exists an embedding $<{ Kb }>^{M_1} (-> M_2' ~> M_2$ extending 
    $\id_K$,
    then there exists an embedding $<{ Kb }>^{M_1} (-> M_2$ extending $\id_K$.
    .
Proof:
    Say $b |-> b' (- M_2'$. Then realise $\tp(b'/K)$ in $M_2$ by $\omega$-saturation.
    .

So we may freely replace $M_2$ with an elementary extension.

# I: local $->$ global

For $M |= \Tan$,
let $\mu(M) := \{ \eta (- M : |\eta| < r \mbox{ for all } r (- \R_{>0} \}$.
For $\alpha (- M$, there is at most one $s (- \R$ s.t. $\alpha (- s+\mu(M)$.
Let $\st(\alpha) := s$ if such $s$ exists, else $\st(\alpha) := \infty$.

Remark:
    for $\alpha != 0$, $\st(\alpha) = \infty$ iff $1 / \alpha (- \mu$.
    .

Remark:
    If $\a (- \mu^n$ and $F (- \R<{ \X }>$,
    then $~F|_r(\a)$ is independent of the choice of $r$.
    We write $~F(\a)$ for the common value.
    Note $~F(\a) (- \mu$, by continuity.
    .

Definition:
    If $A (= \mu(M_1)$,
    a map $e : A --> \mu(M_2)$
    is a {\bf partial $\Tan$-$\mu$-embedding}
    if for $\a (- A^{<\omega}$ and $F (- \R<{ \X }>$,
    \[ ~F(\a) > 0 <=> ~F(e(\a)) > 0 .\]
    .

Lemma:
    Any partial $\Tan$-$\mu$-embedding
    $e : <{ Kb }> \cap \mu(M_1) --> \mu(M_2)$
    extends to an $\LanD$-embedding $e' : <{ Kb }> (-> M_2$.
    .
Proof:
    \[ e'(\alpha) := \begin{cases}
        \st(\alpha) + e(\alpha - \st(\alpha))  &\mbox{if } \st(\alpha) (- \R 
        \\\
        1/e(1 / \alpha)  &\mbox{if } \st(\alpha) = \infty
        \end{cases} \]

    Claim:
        $e'$ is an ordered field embedding.
        .
    Proof: 
        First we show that $e'$ is order-preserving.
        STS $e$ is order-preserving.
        Consider $F := X-Y (- \R\{X,Y\}_1$.
        \[ \Tan |= \forall x,y\. ( |x|<1 /\ |y|<1 -> ~F|_1(x,y) = x-y ), \]
        so for $\eta,\eta' (- <{ Kb }>\cap\mu$,
        *\[a* \eta &> \eta' \\\
            &<=> ~F(\eta,\eta') > 0 \\\
            &<=> ~F(e(\eta),e(\eta')) > 0 \\\
            &<=> e(\eta) > e(\eta'). *a\]*

        Now if $f(X,Y),g(X,Y) (- \R[X,Y]$
        and $\eta,\eta',\eta'' (- <{ Kb }>\cap\mu$
        and $g(\eta,\eta') != 0$
        and $\eta'' = f(\eta,\eta')/g(\eta,\eta')$,
        then by considering $F := Zg(X,Y)-f(X,Y)$,
        $e(\eta'') = f(e(\eta),e(\eta'))/g(e(\eta),e(\eta'))$.

        Preservation by $e'$ of $+,*$ follows.

        For example, suppose $\eta,\eta' (- <{ Kb }>\cap\mu$,
        we claim $e'(1 / \eta + 1 / \eta') = e'(1 / \eta)+e'(1 / \eta')$.
        Let $s := \st((1 / \eta + 1 / \eta')) (- \R \cup {\infty}$.

        If $s=\infty$, then
            \[ \eta'' := 1/(1 / \eta + 1 / \eta') (- <{ Kb }>\cap\mu .\]
        Then by the above applied to the rational function $1/(1/X+1/Y)$,
            \[ e(\eta'') = 1/(1/e(\eta)+1/e(\eta')). \]
        So
            *\[a* e'(1 / \eta + 1 / \eta') &= 1/e(\eta'') \\\
                &= 1/(1/(1/e(\eta) + 1/e(\eta'))) \\\
                &= e'(1 / \eta) + e'(1 / \eta'). *a\]*

        If $s (- \R$, then
            \[ \eta''' := (1 / \eta + 1 / \eta') - s (- <{ Kb }>\cap\mu. \]
        Then
            *\[a* e'(1 / \eta + 1 / \eta') &= s+e(\eta''') \\\
                &= s+((1/e(\eta) + 1/e(\eta'))-s) \\\
                &= e'(1 / \eta) + e'(1 / \eta'). *a\]*

        The other cases (e.g. $e'((s+\eta)(1 / \eta'))$) can be handled 
        similarly.

        % Is this really the neatest proof?
        % Wilkie just says it's "easy to see"...
        .

    It remains to see that for acceptable $(r,F)$,
    and $\alphabar (- <{ Kb }>^n$,
    $e'(~F|_r(\alphabar)) = ~F|_r(e'(\alphabar))$.

    If $||\alphabar|| >= r$ then also $||e'(\alphabar)|| >= r$,
    so the equality is clear.
    Else, $\s := \st(\alphabar) (- \dom(F)$,
    so $~F$ is analytic at $\s$.
    Let $s' := ~F(\s)$,
    and say $(\epsilon,G)$ is acceptable s.t.
    $~F (- \R\{\X\}_{r+\epsilon}$ and
    $~G(\x) = ~F(\s+\x) - s'$ for $\x (- \R^n$, $||\x||<\epsilon$.
    Then \[ \TanD |= \forall \x\.
        (||\x|| < \epsilon ->
            ~G|_\epsilon(\x) = ~F|_{r+\epsilon}(\s+\x) - s'). \]
    So
    *\[a* ~F|_r(e'(\alphabar))
        &= s' + ~F|_{r+\epsilon}(\s+e(\etabar)) - s' \mbox{ (where $\etabar := 
        \alphabar - \s$) } \\\
        &= s' + ~G(e(\etabar)) \\\
        &= s' + e(~G(\etabar))  \mbox{ (considering $Y-G(X)$) } \\\
        &= s' + e(~F|_{r+\epsilon}(\s+\etabar) - s') \\\
        &= e'(~F|_{r+\epsilon}(\alphabar)) \\\
        &= e'(~F|_r(\alphabar))  \mbox{ (since $||\alphabar|| < r$) } *a\]*
    as required.
    .
    
# II: finding a $\Tan$-$\mu$-embedding

It remains to show that such an $e$ exists.

Since we may replace $M_2$ by an elementary extension, it suffices to show that 
the corresponding (long) type over $K\cap\mu$ is consistent, as follows:

Lemma:
    Let $m$,$n (- \N$,
    $\X = (X_1,...,X_m)$,
    $\Y = (Y_1,...,Y_n)$,
    and $S (= \R<{ \X,\Y }>$ finite,
    and $\c (- (K\cap\mu)^m$,
    and $\b (- \mu(M_1)^n$.

    Then exists $\b' (- \mu(M_2)^n$
    s.t. for $F (- S$,
    \[ M_1 |= ~F(\c,\b) > 0 <=> M_2 |= ~F(\c,\b') > 0 .\]
    .
Proof:
    By induction on $n$, the $n=0$ case being trivial.

    First we show how to handle a single $F$.
    So suppose $S = \{F\}$.
    WMA $F /= 0$.

    By Denef - van den Dries Preparation,
    \[ F(\X,\Y) = \sum_{|\nu| < d} a_\nu(\X) \Y^\nu u_\nu(\X,\Y) \]
    for some $d (- \N$, $a_\nu (- \R<{ \X }>$, $u_\nu (- \R<{ \X,\Y }>^*$.

    Let $\nu_0$ s.t. $M := |a_{\nu_0}(\c)| >= |a_\nu(\c)| \forall \nu$.
    Define
        \[ s_\nu := \st(a_\nu(\c)/M) (- \R \]
        \[ k_\nu := a_\nu(\c)/M - s_\nu (- K \]

    (Remark: here it is crucial that $K$ is a $\LanD$-substructure, and hence 
    a subfield, rather than merely a $\Lan$-substructure.)

    Let $\Z = (Z_\nu)_{|\nu| < d}$, and define
    \[ G(\X,\Z,\Y) := \sum_{|\nu| < d} (Z_\nu + s_\nu) \Y^\nu u_\nu(\X,\Y). \]

    Then $G (- \R<{ \X,\Z,\Y }>$, and
    $~F(\c,\y) = M ~G(\c,\k,\y)$ for $\y (- \mu^n$.

    Define $\Lambda : \mu^n --> \mu^n$;
    \[ \y |->
        (y_1+y_n^{d^{n-1}}, y_2+y_n^{d^{n-2}},..., y_{n-1}+y_n^d, y_n). \]

    % Then \Lambda is a bijection, with inverse
    % \Omega : \mu^n --> \mu^n; \y |->
    %  (y_1-y_n^{d^{n-1}}, y_2-y_n^{d^{n-2}},..., y_{n-1}-y_n^d, y_n).

    Let $H(\X,\Z,\Y) := G(\X,\Z,\Lambda(\Y)) (- \R<{ \X,\Z,\Y }>$
    (considering $\Lambda$ as a tuple of (polynomial) formal power series).

    Claim:
        $H$ is regular in $Y_n$.
        .
    Proof:
        *\[a* H(0,0,0,Y_n)
          &= \sum_{|\nu| < d} s_\nu \Lambda(0,Y_n)^\nu u_\nu(0,\Lambda(0,Y_n)) 
          \\\
          &= \sum_{|\nu| < d} s_\nu Y_n^{\sum \nu_i d^{n-i}} u_\nu(0,\Lambda(0,Y_n)) *a\]*
        Now for $\nu$ with $|\nu| < d$,
        the exponents $\sum \nu_i d^{n-i}$ are distinct for distinct $\nu$, 
        and are ordered according to the lexicographic order on the $\nu$.
        So taking $\nu$ lexicographically minimal s.t. $s_\nu /= 0$, which 
        exists since $s_{\nu_0}=1$, witnesses regularity of $H$.
        .

    So by Weierstrass preparation,
        \[ ~F(\c,\Lambda(\y)) = M ~G(\c,\k,\y) = M ~Q(\c,\k,\y) ~L(\c,\k,\y) 
        \]
    where $Q (- \R<{ \X,\Z,\Y }>^*$ and $L (- \R<{ \X,\Z,\Y_{<n} }>[Y_n]$,
    where $\Y_{<n} := (Y_1,...,Y_{n-1})$.
    WLOG $Q(0) > 0$.

    Say $L(\X,\Z,\Y) = \sum_{i=0}^p L_i(\X,\Z,\Y_{<n})Y_n^i$
    with $L_i (- \R<{ \X,\Z,\Y_{<n} }>$.
    
    By QE for RCF,
    for $\epsilon (- \R_{>0}$,
    \[ \exists y_n (- (-\epsilon,\epsilon). \sum_{i=0}^p w_iy_n^i > 0 \]
    is equivalent modulo RCF to a qf ordered ring formula $\psi_\epsilon(\w)$, 
    which is a boolean combination of atomic formulae $f(\w)>0$ where $f$ is a 
    polynomial over $\|Z$.
    So by the inductive hypothesis, and since $\R<{ \X,\Z,\Y_{<n} }>$ is a 
    ring,
    there exists $\b''_\epsilon$ in $\mu(M_2)^{n-1}$ s.t.
    \[ |= \psi_\epsilon(~L_i(\c,\k,\b''_\epsilon)) \]

    So by $\omega$-saturation,
    exists $\b''$ in $\mu(M_2)^n$ s.t.
    $~L(\c,\k,\b'') > 0$.
    Hence $~F(\c,\Lambda(\b'')) > 0$,
    so $\b' := \Lambda(\b'')$ is as required.

    For general finite $S$,
    we may take a $d$ common to all $F (- S$,
    proceed as above (so using the same $\Lambda$ for all $F$),
    and apply RCF QE to the corresponding conjunction of inequalities.
    .
