**Question C.7.6.** If a map $f: \mathbb{R}^n \to \mathbb{R}$ is algebraic on $\mathbb{R}[x]$ and if it is uniformly continuous on all bounded subsets, does it have a uniform continuity modulus à la Łojasiewicz, as in Lemma C.5.3?
NB: the answer is positive in classical mathematics, but it seems much trickier in constructive mathematics.

**Question C.7.7.** Is a semialgebraic map that is continuous in the sense of Definition C.7.5 also continuous in the sense of Definition C.5.5?

Yes in classical mathematics, but the problem arises in constructive mathematics, and seems very difficult. It may be that, by preferring the Definition C.5.5 to Definition C.7.5, we are in a situation similar to that which led Bishop to define the continuity of a map $\mathbb{R} \to \mathbb{R}$ as meaning uniform continuity on any bounded interval.
<figure><img src="image_9.png" /></figure>
# D. $f$-rings

## Sommaire

<table><tr><td>Introduction</td><td>66</td></tr><tr><td>D.1 Distributive lattices</td><td>66</td></tr><tr><td>Distributive lattice theory</td><td>66</td></tr><tr><td>Ideals and filters in a distributive lattice</td><td>66</td></tr><tr><td>Quotients</td><td>67</td></tr><tr><td>D.2 $\ell$-groups</td><td>68</td></tr><tr><td>Definition of the purely equational theory $Grl$</td><td>68</td></tr><tr><td>Some rules derived in $Grl$</td><td>69</td></tr><tr><td>Quotient structures</td><td>70</td></tr><tr><td>Representation theorem</td><td>70</td></tr><tr><td>D.3 $f$-rings</td><td>72</td></tr><tr><td>Purely equational theory of $f$-rings</td><td>72</td></tr><tr><td>Note on $\ell$-rings</td><td>73</td></tr><tr><td>Some derived rules</td><td>73</td></tr><tr><td>Quotient structures</td><td>74</td></tr><tr><td>Solid ideals (or $\ell$-ideals)</td><td>74</td></tr><tr><td>Irreducible $\ell$-ideals</td><td>74</td></tr><tr><td>Formal Positivstellensatz and representation theorem</td><td>74</td></tr><tr><td>Localisations of $f$-rings</td><td>75</td></tr><tr><td>Generalities</td><td>75</td></tr><tr><td>Gluing $f$-rings</td><td>76</td></tr><tr><td>Real schemes</td><td>76</td></tr><tr><td>Rewriting terms in $f$-rings</td><td>76</td></tr><tr><td>$f$-rings of maps, semipolynomials</td><td>77</td></tr><tr><td>D.4 Beyond purely equational theories</td><td>77</td></tr><tr><td>$f$-rings without zerodivisor</td><td>77</td></tr><tr><td>Local $f$-rings</td><td>78</td></tr><tr><td>Strict $f$-ring</td><td>78</td></tr><tr><td>Reduced $f$-rings</td><td>78</td></tr><tr><td>Some derived rules</td><td>78</td></tr><tr><td>The rule FRAC in $Afrnz$</td><td>79</td></tr><tr><td>D.5 Back to ordered fields</td><td>80</td></tr><tr><td>Real $f$-rings</td><td>80</td></tr><tr><td>Formal Positivstellensätze with sup</td><td>81</td></tr><tr><td>D.6 The real lattice and spectrum of a commutative ring</td><td>83</td></tr></table>
# Introduction

This chapter takes up the problem of non discrete ordered fields from scratch.

All the theories introduced admit extensions essentially equivalent to the theory *Co* of non discrete ordered fields (Definition C.3.7).

We start (Section D.1) with the theory of distributive lattices (a non discrete ordered field is a distributive lattice for its order relation).

In Section D.2 we deal with *l*-groups or lattice groups (purely equational theory, valid for addition on the reals).

Then (Section D.3) we move on to *f*-rings (*f*-rings in french litterature), a theory inspired by rings of continuous real maps.

Section D.4 describes dynamical theories in which we add the predicate $\cdot > 0$ (strict *f*-rings and variants).

Section D.5 proposes a return to the theory *Co* by confronting it with suitable extensions of the theory of strict *f*-rings.

In this chapter we say “group” for “abelian group”. And the rings are commutative unitary as throughout the memoir.

## D.1. Distributive lattices

References: [10, 12, 15, 46]

### Distributive lattice theory

The theory of lattices *Tr0* with the only sort *Tr* is a purely equational theory based on the following signature,<fnref n="1" />

$$ \text{Signature: } \Sigma_{Tr} = (\cdot = \cdot; \cdot \wedge \cdot, \cdot \vee \cdot, 1, 0) $$

In addition to the axioms of equality we have the following axioms

$$ \bullet \vdash 0 \wedge x = 0 $$

$$ \bullet \vdash 1 \vee x = 1 $$

$$ \bullet \vdash x \wedge x = x $$

$$ \bullet \vdash x \vee x = x $$

$$ \bullet \vdash x \wedge y = y \wedge x $$

$$ \bullet \vdash x = y \vee x $$

$$ \bullet \vdash (x \wedge y) \wedge z = x \wedge (y \wedge z) $$

$$ \bullet \vdash (x \vee y) \vee z = x \vee (y \vee z) $$

$$ \bullet \vdash (x \wedge y) \vee x = x $$

$$ \bullet \vdash (x \vee y) \wedge x = x $$

We define $x \geq y$ as an abbreviation of $x = x \vee y$. This is an extension of the theory of ordered sets.

The theory *Tr* of non-trivial lattices is obtained by adding the collapse axiom

$$ \mathbf{CL} = 1 = 0 \vdash \mathbf{L} $$

The theory *Trdi* of distributive lattices is obtained by adding the following distributivity axiom (the dual axiom is deduced from this)

$$ \bullet \vdash (x \wedge y) \wedge z = (x \wedge z) \vee (y \wedge z) $$

<footnote n="1">¹More precisely, we can prefer $\cdot =_{Tr} \cdot$, $\cdot \wedge_{Tr} \cdot$, $\cdot \vee_{Tr} \cdot$, $0_{Tr}$ and $1_{Tr}$.</footnote>
## Ideals and filters in a distributive lattice

An ideal $\mathfrak{b}$ of a distributive lattice $(\mathbf{T}, \wedge, \vee, 0, 1)$ is a part that satisfies the constraints:

$$ \left. \begin{array}{rcl} x, y \in \mathfrak{b} & \implies & x \vee y \in \mathfrak{b} \\ x \in \mathfrak{b}, z \in \mathbf{T} & \implies & x \wedge z \in \mathfrak{b} \end{array} \right\} \qquad (D.1) $$

We denote $\mathbf{T}/(\mathfrak{b} = 0)$ the quotient lattice obtained by forcing the elements of $\mathfrak{b}$ to be zero. Ideals can also be defined as kernels of morphisms.

A principal ideal is an ideal generated by a single element $a$, and is denoted by $\downarrow a$. We have $\downarrow a = \{x \in \mathbf{T} | x \le a\}$. The ideal $\downarrow a$, subject to the laws $\wedge$ and $\vee$ of $\mathbf{T}$ is a distributive lattice in which the maximum element is $a$. The canonical injection $\downarrow a \to \mathbf{T}$ is not a morphism of distributive lattices because the image of $a$ is not equal to $1_{\mathbf{T}}$. On the other hand, the map $\mathbf{T} \to \downarrow a$, $x \mapsto x \wedge a$ is a surjective morphism, which therefore defines $\downarrow a$ as a quotient structure $\mathbf{T}/(a = 1)$.

The notion of filter is the opposite notion (obtained by reversing the order relation) to that of ideal.

Let $\mathfrak{a}$ be an ideal and $\mathfrak{f}$ a filter of $\mathbf{T}$. We say that $(\mathfrak{a}, \mathfrak{f})$ is a saturated pair in $\mathbf{T}$ if

$$ (g \in \mathfrak{f}, x \wedge g \in \mathfrak{a}) \implies x \in \mathfrak{a}, \text{ and } (a \in \mathfrak{a}, x \vee a \in \mathfrak{f}) \implies x \in \mathfrak{f}. $$

A saturated pair is a pair $(\varphi^{-1}(0), \varphi^{-1}(1))$ for a morphism $\varphi: \mathbf{T} \to \mathbf{T}'$ of distributive lattices. When $(\mathfrak{a}, \mathfrak{f})$ is a saturated pair, we have the equivalences

$$ 1 \in \mathfrak{a} \iff 0 \in \mathfrak{f} \iff (\mathfrak{a}, \mathfrak{f}) = (\mathbf{T}, \mathbf{T}) $$

If $A$ and $B$ are two parts of $\mathbf{T}$ we note

$$ A \vee B = \{a \vee b | a \in A, b \in B\} \quad \text{and} \quad A \wedge B = \{a \wedge b | a \in A, b \in B\}. \qquad (D.2) $$

Then the ideal generated by two ideals $\mathfrak{a}$ and $\mathfrak{b}$ is equal to $\mathfrak{a} \vee \mathfrak{b}$. The set of ideals of $\mathbf{T}$ itself forms a distributive lattice<fnref n="2" /> for inclusion, with the lower bound of $\mathfrak{a}$ and $\mathfrak{b}$ being the ideal $\mathfrak{c} = \mathfrak{a} \wedge \mathfrak{b}$. Thus the operations $\vee$ and $\wedge$ defined in (D.2) correspond to the sup and inf in the lattice of ideals.

When we consider the lattice of filters, we must pay attention to what the inversion of the order relation produces: $\mathfrak{f} \cap \mathfrak{g} = \mathfrak{f} \vee \mathfrak{g}$ is the inf of the filters $\mathfrak{f}$ and $\mathfrak{g}$, whereas their sup is the lattice generated by $\mathfrak{f} \cup \mathfrak{g}$, equal to $\mathfrak{f} \wedge \mathfrak{g}$.

## Quotients

A quotient distributive lattice $\mathbf{T}'$ of $\mathbf{T}$ is given by a binary relation $\preceq$ over $\mathbf{T}$ satisfying the following properties:

$$ \left. \begin{array}{rcl} a \preceq b & \implies & a \preceq b \\ a \preceq b, b \preceq c & \implies & a \preceq c \\ a \preceq b, a \preceq c & \implies & a \preceq b \wedge c \\ b \preceq a, c \preceq a & \implies & b \vee c \preceq a \end{array} \right\} \qquad (D.3) $$

**Proposition D.1.1.** Let $\mathbf{T}$ be a distributive lattice and $(J, U)$ be a pair of parts of $\mathbf{T}$. Consider the quotient $\mathbf{T}'$ of $\mathbf{T}$ defined by the relations $x = 0$ for the $x \in J$ and $y = 1$ for the $y \in U$. Then we have $a \preceq_{\mathbf{T}'} b$ if, and only if, there exists a finite part $J_0$ of $J$ and a finite part $U_0$ of $U$ such that:

$$ a \wedge \bigwedge U_0 \preceq_{\mathbf{T}} b \vee \bigvee J_0 \qquad (D.4) $$

We will note $\mathbf{T}/(J = 0, U = 1)$ this quotient lattice $\mathbf{T}'$.

<footnote n="2">²In fact it is necessary to introduce a restriction to really obtain a set, so that we have a well-defined procedure for constructing the ideals concerned. For example, we can consider the set of ideals obtained from the principal ideals by certain predefined operations, such as countable meetings and intersections.</footnote>
In commutative algebra, if $\mathfrak{a}$ and $\mathfrak{b}$ are two ideals of a ring $\mathbf{A}$ we have an “exact sequence” of $\mathbf{A}$-modules (with $j$ and $p$ ring homomorphisms)

$$0 \to \mathbf{A}/(\mathfrak{a} \cap \mathfrak{b}) \xrightarrow{j} (\mathbf{A}/\mathfrak{a}) \times (\mathbf{A}/\mathfrak{b}) \xrightarrow{p} \mathbf{A}/(\mathfrak{a} + \mathfrak{b}) \to 0$$

which can be read in everyday language: the system of congruences $x \equiv a \bmod \mathfrak{a}$, $x \equiv b \bmod \mathfrak{b}$ has a solution if, and only if, $a \equiv b \bmod \mathfrak{a} + \mathfrak{b}$ and in this case the solution is unique modulo $\mathfrak{a} \cap \mathfrak{b}$. It is remarkable that this Chinese remainder theorem generalises to a system of congruences if, and only if, the ring is arithmetic ([CACM, Theorem XII-1.6]), i.e. if the lattice of ideals is distributive (the Chinese remainder theorem “contemporary” concerns the special case of a family of two-by-two comaximal ideals, and it works without any hypothesis on the base ring).

Other epimorphisms in the category of commutative rings are localisations. And there is a gluing principle analogous to the Chinese remainder theorem for localisations, which is extremely fruitful (the local-global principle).

In the same way we can recover a distributive lattice from a finite number of its quotients, if the information they contain is “sufficient”. This can be seen either as a procedure for gluing (going from local to global), or as a version of the Chinese remainder theorem for distributive lattices. Let’s take a closer look.

**Definition D.1.2.** Let $\mathbf{T}$ be a distributive lattice, $(\mathfrak{a}_i)_{i=1,...,n}$ (resp. $(\mathfrak{f}_i)_{i=1,...,n}$) a finite family of ideals (resp. filters) of $\mathbf{T}$. We say that the ideals $\mathfrak{a}_i$ cover $\mathbf{T}$ if $\bigcap_i \mathfrak{a}_i = \{0\}$. Similarly we say that the filters $\mathfrak{f}_i$ cover $\mathbf{T}$ if $\bigcap_i \mathfrak{f}_i = \{1\}$.

For an ideal $\mathfrak{b}$ we write $x \equiv y \bmod \mathfrak{b}$ as an abbreviation for $x \equiv y \bmod (\mathfrak{b} = 0)$.

**Proposition D.1.3.** Let $\mathbf{T}$ be a distributive lattice, $(\mathfrak{a}_i)_{i=1,...,n}$ be a finite family of principal ideals $(\mathfrak{a}_i = \downarrow s_i)$ of $\mathbf{T}$ and $\mathfrak{a} = \bigcap_i \mathfrak{a}_i$.

1. If $(x_i)$ is a family of elements of $\mathbf{T}$ such that for each $i, j$ we have $x_i \equiv x_j \bmod \mathfrak{a}_i \lor \mathfrak{a}_j$, then there exists a unique $x$ modulo $\mathfrak{a}$ satisfying: $x \equiv x_i \bmod \mathfrak{a}_i$ ($i = 1, ..., n$).

2. Let us note $\mathbf{T}_i = \mathbf{T}/(\mathfrak{a}_i = 0)$, $\mathbf{T}_{ij} = \mathbf{T}_{ji} = \mathbf{T}/(\mathfrak{a}_i \lor \mathfrak{a}_j = 0)$, $\pi_i : \mathbf{T} \to \mathbf{T}_i$ and $\pi_{ij} : \mathbf{T}_i \to \mathbf{T}_{ij}$ the canonical projections. If $(\mathfrak{a}_i)_{i=1}^n$ covers $\mathbf{T}$, then $(\mathbf{T}, (\pi_i)_{i=1,...,n})$ is the projective limit of the diagram $((\mathbf{T}_i)_{1 \le i \le n}, (\mathbf{T}_{ij})_{1 \le i < j \le n}; (\pi_{ij})_{1 \le i \ne j \le n})$ (see figure below).

3. Now let $(\mathfrak{f}_i)_{i=1,...,n}$ be a finite family of principal filters, let $\mathbf{T}_i = \mathbf{T}/(\mathfrak{f}_i = 1)$, $\mathbf{T}_{ij} = \mathbf{T}_{ji} = \mathbf{T}/(\mathfrak{f}_i \cup \mathfrak{f}_j = 1)$, $\pi_i : \mathbf{T}_i \to \mathbf{T}_i$ and $\pi_{ij} : \mathbf{T}_i \to \mathbf{T}_{ij}$ the canonical projections. If $\mathfrak{f}_i$ covers $\mathbf{T}$, $(\mathbf{T}, (\pi_i)_{i=1,...,n})$ is the projective limit of the diagram $((\mathbf{T}_i)_{1 \le i \le n}, (\mathbf{T}_{ij})_{1 \le i < j \le n}; (\pi_{ij})_{1 \le i \ne j \le n})$.

<figure><img src="image_10.png" /></figure>

# D.2. $\ell$-groups

## Definition of the purely equational theory $\mathcal{Grl}$

The theory $\mathcal{Grl}$ of $\ell$-groups (or reticulated groups, or lattice groups) is defined as follows. There is only one sort, named $\mathcal{Grl}$.

$$ \text{Signature :} \qquad \Sigma_{\mathcal{Grl}} = (\cdot = 0; \cdot + \cdot, - \cdot, \cdot \lor \cdot, 0) $$

The symbol $\lor$ used for the binary upper bound must not be confused with the symbol $\vee$ for the logical disjunction.
## Abbreviations

### Function symbols

* $x \wedge y$ means $-(x \vee -y)$

* $|x|$ means $x \vee -x$

* $x^+$ means $x \vee 0$

* $x^-$ means $-x \vee 0$

### Predicates

* $x = y$ means $x - y = 0$

* $x \perp y$ means $|x| \wedge |y| = 0$

* $x \geq y$ means $x \vee y = x$

* $x \leq y$ means $y \geq x$

## Axioms

### Direct rules for abelian groups

$$ \mathbf{ga0} \vdash 0 = 0 $$

$$ \mathbf{ga2} \quad x = 0, y = 0 \vdash x + y = 0 $$

$$ \mathbf{ga1} \quad x = 0 \vdash -x = 0 $$

NB. The rules **ga0**, **ga1** and **ga2** define the purely equational theory *Ga* of abelian groups. We must then replace, in the explanation given on page 19 for commutative rings (Example A.2.1), the computational machinery of commutative rings $\mathbb{Z}[x_1, \dots, x_n]$ (freely generated by $x_i$'s) by that of abelian groups $\mathbb{Z}^{\{x_1, \dots, x_n\}}$ (freely generated by $x_i$'s).

### Rules for the compatibility of $\vee$ with equality

$$ \mathbf{sup1}_- \quad x = 0 \vdash (x + y) \vee z = y \vee z $$

$$ \mathbf{sup2}_- \quad x = 0 \vdash y \vee (x + z) = y \vee z $$

### Equality rules

The following identities express the fact that $\vee$ defines an unbounded sup-half lattice as well as the compatibility of $\vee$ with $+$ (the fact that translations are a morphism for the law $\vee$).

$$ \mathbf{sdt1} \quad \vdash \quad x \vee x = x $$

$$ \mathbf{sdt2} \quad \vdash \quad x = y \vee x $$

$$ \mathbf{sdt3} \quad \vdash \quad (x \vee y) \vee z = x \vee (y \vee z) $$

$$ \mathbf{grl} \quad \vdash \quad x + (y \vee z) = (x + y) \vee (x + z) $$

We thus obtain an (abelian) $\ell$-group with all the related geometric rules (see [Bigard, Keimel & Wolfenstein], [Zaanen, Chapter 2], [Bourbaki, Algebra, Chapter 6], and [CACM, Section XI-2, results 2.2-2.5, 2.11 and 2.12]). Here are a few of them.

### Some rules derived in $Gr_l$

$$ \mathbf{grl1} \quad \vdash \quad x \vee (y_1 \wedge y_2) = (x \vee y_1) \wedge (x \vee y_2) $$

$$ \mathbf{grl2} \quad \vdash \quad x \wedge (y_1 \vee y_2) = (x \wedge y_1) \vee (x \wedge y_2) $$

$$ \mathbf{grl3} \quad \vdash \quad (x \wedge y) \vee x = x $$

$$ \mathbf{grl4} \quad \vdash \quad (x \vee y) \wedge x = x $$

$$ \mathbf{grl5} \quad \vdash \quad (x \wedge y) + (x \vee y) = x + y $$

$$ \mathbf{grl6} \quad \vdash \quad x = x^{+} - x^{-} $$

$$ \mathbf{grl7} \quad \vdash \quad |x| = x^{+} + x^{-} = x^{+} \vee x^{-} $$

$$ \mathbf{Sup} \quad z \geq x, z \geq y \vdash z \geq x \vee y $$

$$ \mathbf{Gao} \quad x \geq 0, x \leq 0 \vdash x = 0 $$

$$ \mathbf{Gr1} \quad y \geq 0, z \geq 0, y \perp z \vdash (y - z)^{+} = y $$

$$ \mathbf{Gr2} \quad x \leq z \vdash (x \wedge y) \vee z = x \wedge (y \vee z) $$

$$ \mathbf{Gr1}_n \quad nx \geq 0 \vdash x \geq 0 \quad (n \in \mathbb{N}, n > 1) $$

$$ \mathbf{Gr4}_n \quad nx \geq \bigwedge_{k=1}^{n} (ky + (n-k)x) \vdash x \geq y $$
**Gauss** $x \ge 0, y \ge 0, z \ge 0, x \perp y, x \le y + z \vdash x \le z$

## Quotient structures

The kernels of morphisms of ordered (abelian) groups are the *convex subgroups*: a subgroup $H$ is convex if, and only if, it verifies the property

$$ (x \in H, y \in G, 0 \le y \le x) \Rightarrow y \in H. $$

If a subgroup is convex, the order relation “pass to quotient” in $G/H$.

The kernels of $\ell$-group morphisms are the *solid subgroups*. A subgroup is solid if, and only if, it is a convex $\ell$-subgroup, or convex and stable by $x \mapsto |x|$ ([Bigard, Keimel & Wolfenstein, theorem 2.2.1]).

The solid subgroup generated by an element $a$ is $C(a) := \{x \mid \exists n \in \mathbb{N}, |x| \le n |a|\}$.

Solid finitely generated subgroups are all principal: $C(|a| + |b|) = C(|a| \lor |b|)$ is the solid subgroup generated by $a$ and $b$. The principal solid subgroups form a distributive lattice (with $C(a) \cap (b) = C(|a| \land |b|)$), except that a maximum element is missing, which can be added formally.

The Krull dimension of this distributive lattice is called the *dimension*, or *height*, of the $\ell$-group. This is a constructive definition equivalent to the classical definition in classical mathematics, but does not require the existence of prime convex subgroups (see [CACM, section XIII-6] for the Krull dimension of distributive lattices). In the case of linearly ordered groups, this corresponds to the *rank* of the group.

## Representation theorem

In classical mathematics, any lattice group is a subgroup of a product of linearly ordered groups.

The method of proof explained in [CACM, Principle XI-2.10] gives a constructive equivalent of this property: to prove a concrete fact in a lattice group, we can always act as if we were in the presence of a product of linearly ordered groups.

In fact, we have a better (more formal) formulation in the language of dynamical theories: both dynamical theories (with and without the axiom of total order) prove the same Horn rules. Let's look at this in more detail.

**Definition D.2.1.** The dynamical theory $\mathcal{Gtosup}$ of linearly ordered groups with $sup^3$ is the dynamical theory of $\ell$-groups to which we add the dynamical rule **OT** saying that the order is total.

$$ \mathbf{OT} \vdash x \ge 0 \quad \mathbf{op} \quad x \le 0 $$

Note that compared with the usual theory of linearly ordered groups $\mathcal{Gto}$ (whose definition we leave to the reader) we have introduced into the signature the law $\cdot \lor \cdot$ which is well-defined. The $\mathcal{Gtosup}$ theory is essentially identical to the $\mathcal{Gto}$ theory.

**Formal Positivstellensatz D.2.2** (for $\ell$-groups).

The dynamical theories $\mathcal{Grl}$ and $\mathcal{Gtosup}$ prove the same Horn rules.

*Proof.* The reader can refer to the proof of the formal Positivstellensatz D.3.2, and change the very little that needs to be changed. $\square$

For example, the reader can easily prove the rules $\mathbf{Grl2}$ and $\mathbf{Grl4}_n$ using Positivstellensatz D.2.2, which would otherwise be much less simple.

A corollary in classical mathematics of Positivstellensatz D.2.2 is the following theorem (as a special case of Theorem A.5.4).

<footnote n="3">³Or totally ordered groups with sup.</footnote>
**Corollary\* D.2.3** (representation theorem). See [44, Lorenzen, 1939], and the developments [45, 47] commented in [14]. Any $\ell$-group $G$ is a subproduct of linearly ordered groups$^4$ quotients of $G$.

**Remark D.2.4.** The theory of algorithmic complexity in the space of continuous real maps on the interval $[0, 1]$ makes natural use of the divisible $\ell$-group structure (2-divisibility is sufficient). This space of functions is seen essentially as a Riesz space, and the multiplication of maps is relegated to the background. See for example [32, definition 3.2.1]. Note also that in this theory formulas are replaced by circuits (a short circuit can encode a very long formula). In this case we are in analysis rather than abstract algebra. ■

An example of the application of the formal Positivstellensatz for $\ell$-groups is given in [CACM, Fact XI-2.12] which we reproduce below.

**Fact D.2.5** (other identities in $\ell$-groups).

Let $x, y, x', y', z, t \in G, n \in \mathbb{N}, x_1, \dots, x_n \in G$.

$$1. x + y = |x - y| + 2(x \wedge y)$$

$$2. (x \wedge y)^+ = x^+ \wedge y^+, (x \wedge y)^- = x^- \vee y^-, (x \vee y)^+ = x^+ \vee y^-, (x \vee y)^- = x^- \wedge y^-.$$

$$3. 2(x \wedge y)^+ \le (x + y)^+ \le x^+ + y^+.$$

$$4. |x + y| \le |x| + |y|; \therefore |x| + |y| = |x + y| + 2(x^+ \wedge y^-) + 2(x^- \wedge y^+).$$

$$5. |x - y| |x| + |y|; \therefore |x| + |y| = |x - y| + 2(x^+ \wedge y^+) + 2(x^- \wedge y^-).$$

$$6. |x + y| \vee |x - y| = |x| + |y|.$$

$$7. |x + y| \wedge |x - y| = ||x| - |y||.$$

$$8. |x - y| = (x \vee y) - (x \wedge y).$$

$$9. |(x \vee z) - (y \wedge z)| + |(x \wedge z) - (y \wedge z)| = |x - y|.$$

$$10. |x^+ - y^+| + |x^- - y^-| = |x - y|.$$

$$11. x \le z \implies (x \wedge y) \vee z = x \wedge (y \vee z).$$

$$12. x + y = z + t \implies x + y = (x \vee z) + (y \wedge t).$$

$$13. nx \ge \bigwedge_{k=1}^{n} (ky + (n-k)x) \implies x \ge y.$$

$$14. \bigvee_{i=1}^{n} x_i = \sum_{k=1}^{n} (-1)^{k-1} \sum_{I \in \mathcal{P}_{k,n}} \bigwedge_{i \in I} x_i.$$

$$15. x \perp y \iff |x + y| = |x - y| \iff |x + y| = |x| \vee |y|.$$

$$16. x \perp y \iff |x + y| = |x| + |y| = |x| \vee |y|.$$

$$17. (x' \perp y, x' \perp y, x' \perp y', x' \perp y', x + y = x' + y') \implies (x = x', y = y').$$

$$18. \text{We define } \text{Tri}(\underline{x}) = [\text{Tri}_1(\underline{x}), \text{Tri}_2(\underline{x}), \dots, \text{Tri}_n(\underline{x})], \text{ where}$$

$$\text{Tri}_k(x_1, \dots, x_n) = \bigwedge_{I \in \mathcal{P}_{k,n}} (\bigvee_{i \in I} x_i) \quad (k \in \llbracket 1..n \rrbracket).$$

We also have the following.

$$(a) \text{ Tri}_k(x_1, \dots, x_n) = \bigvee_{j \in \mathcal{P}_{n-k+1,n}} (\bigwedge_{j \in J} x_j), (k \in \llbracket 1..n \rrbracket).$$

$$(b) \text{ Tri}_1(\underline{x}) \le \text{Tri}_2(\underline{x}) \le \dots \le \text{Tri}_n(\underline{x}).$$

<footnote>$^4$Any $\ell$-group $G$ is a substructure of a product of linearly ordered quotient groups of $G$. In other words, there is a lattice subgroup of a product of linearly ordered groups which, as a lattice group, is isomorphic to the original lattice group. The English terminology is: any lattice group is a *subdirect product* of linearly ordered groups.</footnote>
(c) If the $x_i$ are two by two comparable, the list $\text{Tri}(\underline{x})$ is the list of $x_i$'s arranged in ascending order (the group need not be discrete).

Suppose $u, v, w^i n G^+$.

$$19. u \perp v \iff u + v = |u - v|.$$

$$20. (u+v) \wedge w \le (u \wedge w) + (v \wedge w).$$

$$21. (x+y) \vee w \le (x \vee w) + (y \vee w).$$

$$22. v \perp w \implies (u+v) \wedge w = u \wedge w.$$

$$23. u \perp v \implies (u+v) \wedge w = (u \wedge w) + (v \wedge w).$$

*Proof.* All this is more or less immediate in a linearly ordered group, reasoning case by case. We conclude with the formal Positivstellensatz. $\square$

## D.3. *f*-rings

References: [Bigard, Keimel & Wolfenstein], [Johnstone, Section V-4], [8, 20, 50].

The french terminology of [Bigard, Keimel & Wolfenstein] is “f-anneau” or “anneau de fonctions”. They study the case of non-commutative and non-unitary rings, for which the results are more subtle and delicate than those given here for the commutative unitary case. The terminology “f-anneau” can be found in Bourbaki’s exercises (Algebra, Chapter VI, Exercises, §2, exercise 5).

The (commutative unitary) *f*-rings are defined by a purely equational theory. The axioms are those of commutative rings, those of *l*-groups for addition, and finally the equality rule *afr* which expresses a form of compatibility of $\vee$ with multiplication.<fnref n="5" /> Here’s everything in detail.

### Definition of the purely equational theory *Afr*

The *Afr* theory is defined as follows.

$$ \text{Signature: } (\cdot = 0; \cdot + , \cdot \times , \cdot \vee , \cdot \perp , 0, 1). $$

**Abbreviations** (as for *l*-groups)

Function symbols

* $x \wedge y$ means $-(x \vee -y)$

* $|x|$ means $x \vee -x$

* $x^+$ means $x \vee 0$

* $x^-$ means $-x \vee 0$

Predicates

* $x = y$ means $x - y = 0$

* $x \perp y$ means $|x| \wedge |y| = 0$

* $x \ge y$ means $x \vee y = x$

* $x \le y$ means $y \ge x$

**Axioms**

Rules of commutative rings

$$ \mathbf{ga0} \vdash 0 = 0 $$

$$ \mathbf{acl} \ x = 0 \vdash xy = 0 $$

$$ \mathbf{ga2} \ x = 0, y = 0 \vdash x + y = 0 $$

<footnote n="5">⁵Compared to the theory *Grl*, we added the law “$\cdot \times \cdot$” and the rules *acl* and *afr*. In addition, the computational machinery that reduces any term on the variables $X_1, \dots, X_n$ to its canonical writing in the free abelian group $\mathbb{Z}^{\{X_1, \dots, X_n\}}$ has been replaced with the computational machinery that reduces any element of $\mathbb{Z}[X_1, \dots, X_n]$ to a normal form.</footnote>
Rules for compatibility of $\vee$ with equality

$$ \mathbf{sup1}_{=} \quad x = 0 \vdash (x + y) \vee z = y \vee z $$

$$ \mathbf{sup2}_{=} \quad x = 0 \vdash y \vee (x + z) = y \vee z $$

Equality rules

$$ \mathbf{sdt1} \quad \vdash \quad x \vee x = x $$

$$ \mathbf{grl} \quad \vdash \quad x + (y \vee z) = (x + y) \vee (x + z) $$

$$ \mathbf{sdt2} \quad \vdash \quad x = y \vee x $$

$$ \mathbf{afr} \quad \vdash \quad x^{+} (y \vee z) = (x^{+} y) \vee (x^{+} z) $$

$$ \mathbf{sdt3} \quad \vdash \quad (xy) \vee z = x(yz) $$

## Note on *l*-rings

The theory *Arl* of *l*-rings (or lattice rings) is defined by replacing the rule **afr** by the rules **ao1** and **ao2** of ordered rings, valid in *Afr*.

$$ \mathbf{ao1} \quad \vdash \quad x^2 \geq 0 $$

$$ \mathbf{ao2} \quad x \geq 0, y \geq 0 \vdash xy \geq 0 $$

**Lemma D.3.1.** In the theory of *l*-rings, the following rules are all equivalent.

$$ \mathbf{afr} \quad \vdash \quad a^{+} (b \vee c) = (a^{+} b) \vee (a^{+} c) $$

$$ \mathbf{Afr} \quad a \geq 0 \vdash a(b \vee c) = ab \vee ac $$

$$ \mathbf{afr}' \quad \vdash \quad a^{+} (b \wedge c) = (a^{+} b) \wedge (a^{+} c) $$

$$ \mathbf{Afr}' \quad a \geq 0 \vdash a(b \wedge c) = ab \wedge ac $$

$$ \mathbf{afr0} \quad \vdash \quad b^{-} \wedge a^{+}b^{+} = 0 $$

$$ \mathbf{Afr0} \quad b \wedge c = 0, a \geq 0 \vdash b \wedge ac = 0 $$

$$ \mathbf{afr1} \quad \vdash \quad a^{+} a^{-} = 0 $$

$$ \mathbf{Afr1} \quad a \wedge b = 0 \vdash ab = 0 $$

$$ \mathbf{afr2} \quad \vdash \quad |a| |b| = |ab| $$

$$ \mathbf{afr6a} \quad \vdash \quad a^2 = (a^+)^2 + (a^-)^2 $$

$$ \mathbf{afr3a} \quad \vdash \quad (ab)^{+} = a^{+}b^{+} + a^{-}b^{-} $$

$$ \mathbf{afr6b} \quad \vdash \quad a^2 = |a|^2 $$

$$ \mathbf{afr3b} \quad \vdash \quad (ab)^{-} = a^{+}b^{-} + a^{-}b^{+} $$

$$ \mathbf{sup} \quad \vdash \quad ((x \vee y) - x) ((x \vee y) - y) = 0 $$

$$ \mathbf{afr4} \quad \vdash \quad c^{+} |a| = |c^{+}a| $$

$$ \mathbf{Afr2} \quad b \perp c \vdash ab \perp ac $$

$$ \mathbf{afr5} \quad \vdash \quad (a \wedge b)(a \vee b) = ab $$

In other words, each of these rules can be used to define *f*-rings by adding it to the theory *Arl*. The fact that **afr** implies **ao1**, **ao2** and the rules indicated in Lemma D.3.1 results from the formal Positivstellensatz D.3.2.

In the case of a non-unitary *f*-ring the rule **afr0** is stronger than the others (see [Bigard, Keimel & Wolfenstein], proposition 9.1.10⁶).

## Some derived rules in the theory *Afr*

In addition to the rules derived for *l*-groups and those indicated in Lemma D.3.1, here are some very useful classical rules in which multiplication is involved.

$$ \mathbf{Afr4} \quad b \geq 0, ab = 1 \vdash a \geq 0 $$

$$ \mathbf{Afr5} \quad c \geq 0, a(a^2 + c) \geq 0 \vdash a^3 \geq 0 $$

$$ \mathbf{afr7} \quad \vdash \quad ab^{+} = (ab \wedge (a^2 + 1)b) \vee -(a^2 + 1)b \wedge 0 $$

<footnote n="6">⁶The book deals more generally with ordered rings which are not necessarily commutative or unitary. The condition **afr0** must then be split to take account of the non-commutativity.</footnote>
Remark. The rule **afr7** is used to demonstrate the possibility of writing terms in a simplified form in a free f-ring: see Lemma D.3.7. ■

## Quotient structures

### Solid ideals (or $\ell$-ideals)

By definition, the kernels of f-ring morphisms are called solid ideals or $\ell$-ideals.

An ideal is solid if, and only if, it is solid as a subgroup.

The solid ideal generated by an element $a$ is

$$ \mathcal{I}(a) := \{ x \mid \exists y, |x| \le |ya| \}. $$

We have $\mathcal{I}(a) = \mathcal{I}(|a|)$ and $\mathcal{I}(a) \cap \mathcal{I}(b) = \mathcal{I}(|a| \wedge |b|)$. Finally, the $\ell$-ideal generated by $a_1, \dots, a_n$ is

$$ \mathcal{I}(a_1, \dots, a_n) = \mathcal{I}(|a_1| + \dots + |a_n|) = \mathcal{I}(|a_1| \vee \dots \vee |a_n|). $$

### Irreducible $\ell$-ideals

We say that a solid ideal $I$ of an f-ring $A$ is irreducible if the quotient f-ring is linearly ordered. In other words, for any $x \in A$, $x^+ \in I$ or $x^- \in I$.

By Lemma D.4.1, every prime solid ideal is irreducible.

Moreover, a convex prime ideal (as an additive subgroup) $p$ is solid: we must see that it is stable by $\vee$. If $a, b \in p$ we have $(a-b)^+ \text{ or } (a-b)^- \in p$. And the identities $b+(a-b)^+ = a \vee b = a+(a-b)^-$ are valid in $\ell$-groups (and a fortiori in f-rings) because they are valid in linearly ordered groups (formal Positivstellensatz D.2.2).

## Formal Positivstellensatz and representation theorem for f-rings

Recall that the dynamical theory of linearly ordered rings with sup is the dynamical theory of linearly ordered rings to which we add a function symbol $\cdot \vee \cdot$ which must satisfy the following Horn rules.

$$ \mathbf{sup1} \vdash x \vee y \ge x $$

$$ \mathbf{Sup} \ z \ge x, z \ge y \vdash z \ge x \vee y $$

$$ \mathbf{sup2} \vdash x \vee y \ge y $$

We can also see *Atosup* as the theory of f-rings to which we add as an axiom the dynamical rule **OT** (saying that the order is total).

$$ \mathbf{OT} \vdash x \ge 0 \quad \mathbf{op} \ x \le 0 $$

Given the unique existence of the lub in a linearly ordered ring, the theories *Ato* and *Atosup* are essentially identical. In particular, they prove the same dynamical rules (when formulated without using $\vee$).

The theorem for f-rings analogous to Positivstellensatz D.2.2 is as follows. It is a result of the same type as Item 2 of Positivstellensatz C.2.2.

### Formal Positivstellensatz D.3.2 (for f-rings).

The theories *Afr* and *Atosup* prove the same Horn rules.

*Proof.* Consider a Horn rule proved in the dynamical theory *Atosup*. We can assume without loss of generality that the conclusion of the rule is an equality $t = 0$ for a suitable term $t$. In the corresponding calculation, in the presence of a term $u$, we are authorised by **OT** to open two branches. One where $u \ge 0$, the other where $u \le 0$. At each node of the dynamic proof, we are in fact working in an f-ring defined by generators and relations: the generators are given in the presentation and in the hypotheses of the Horn rule to be proved; the same applies to the relations,
with the addition of those which we have added, in the branch we are in, to the branches which precede the node. Suppose that at a given moment, for two terms $a$ and $b$, we have opened a branch where $a \ge b$ and another where $a \le b$. Let's put $c = b - a$. In the first branch we have added the hypothesis $c^- = 0$, in the second the hypothesis $c^+ = 0$. If in each of the branches we can prove $t = 0$, this means that in the $f$-ring corresponding to the node in question, we have on the one hand $t \in \mathcal{I}(c^-)$, and on the other hand $t \in \mathcal{I}(c^+)$. Now in an $f$-ring we have $\mathcal{I}(c^+) \cap \mathcal{I}(c^-) = \mathcal{I}(c^+ \wedge c^-) = \{0\}$. $\square$

Let's use Positivstellensatz D.3.2 for proving Horn Rules **Afr4** and **Afr5**.

$$ \mathbf{Afr4} \quad y \ge 0, xy = 1 \vdash x \ge 0 $$

$$ \mathbf{Afr5} \quad c \ge 0, x(x^2 + c) \ge 0 \vdash x^3 \ge 0 $$

In both cases, we open two branches, one where $x \ge 0$, and the result is clear, the other where $x \le 0$. For **Afr4** we deduce that $1 \le 0$, then $1 = 0$, then $x = 0$. For **Afr5** we deduce that $x^3 \ge -xc \ge 0$.

Similarly, we prove **afr7** by examining separately the cases “$b \ge 0$”, “$b \le 0, a \ge 0$” and “$b \le 0, a \le 0$”. As a consequence of the formal Positivstellensatz D.3.2 we obtain in classical mathematics the following representation theorem (as a special case of Theorem A.5.4).

**Corollary\* D.3.3 (representation theorem).** Any $f$-ring $\mathbf{A}$ is a subproduct of linearly ordered rings quotients of $\mathbf{A}$.

The following theorem is of the same type as Item 1 of Positivstellensatz C.2.2. This result can be seen as a second form of the formal Positivstellensatz for $f$-rings. We say that a *dynamic algebraic structure of type* $\mathbf{Afr}$ *collapses when the rule $\vdash 1 = 0$ is valid*.

**Theorem D.3.4 (simultaneous collapse, for the signature $(\cdot = 0, \cdot \ge 0; \cdot +, \cdot \times, \cdot \vee, \cdot, -, 0, 1)$).**
The theories *Afr*, *Crcdsup* and all intermediate theories collapse simultaneously.

*Proof.* The theories *Afr* and *Atosup* collapse simultaneously according to Positivstellensatz D.3.2. The theories *Ato* and *Crcd* collapse simultaneously according to Item 1 of Positivstellensatz C.2.2. Finally, the theories *Ato* and *Crcd* are essentially identical to the theories *Atosup* and *Crcdsup* respectively. $\square$

## Localisations of $f$-rings

### Generalities

Consider a monoid $S$ in an $f$-ring and construct the solution of the universal problem (in the category of $f$-rings) consisting in inverting the elements of $S$.

To do this, we need only consider the usual localised ring $S^{-1}\mathbf{A}$ and define the law $\vee$ correctly. Since inverting $s$ or inverting $s^2$ amounts to the same thing, we can consider only fractions with denominator $\ge 0$. We then define

$$ \frac{a}{s} \vee \frac{b}{t} := \frac{at \vee bs}{st} \quad (s, t \ge 0). $$

*Note.* We have no choice, because since $s, t \ge 0$, we must have $st(\frac{a}{s} \vee \frac{b}{t}) = st \frac{a}{s} \vee st \frac{b}{t} = at \vee bs$ in $S^{-1}\mathbf{A}$. It remains to be seen that the law is well-defined and that it continues to satisfy the required axioms. For example, let's check that it is well-defined. Suppose that $\frac{a_1}{s_1} = \frac{a_2}{s_2}$, i.e. that $a_1 s_2 s_3 = a_2 s_1 s_3$ for an $s_3 \ge 0$ in $S$. Then we can easily check that the two elements $\frac{a_i}{s_i} \vee \frac{b}{t}$ given by the definition above are equal in $S^{-1}\mathbf{A}$. This is the same calculation that was used to justify addition in $S^{-1}\mathbf{A}$ when we were young.<fnref n="7" /> Just replace $+$ by $\vee$, with the precaution of having denominators $\ge 0$. ■

<footnote n="7">⁷When we fell over in admiration of Claude Chevalley who dared to invert zerodivisors, and nothing awful resulted, quite the contrary.</footnote>
An f-ring A can always be considered as immersed in a Q-f-algebra. Indeed, according to Gr13n, the “integers” n.1A are regular and therefore A injects itself into the Q-algebra Q ⊗Z A which is an f-ring as a localisation of A.<fnref n="8" />

### • Gluing f-rings

**Concrete local-global principle D.3.5 (concrete gluing of f-rings).**

Let $S_1, \dots, S_n$ be comaximal monoids of a ring A. Let $A_i$ denote $A_{S_i}$, $A_{ij}$ denote $A_{S_i S_j}$, and assume that an f-ring structure with a $\vee_i$ law is given on each $A_i$. It is further assumed that the images in $A_{ij}$ of the laws $\vee_i$ and $\vee_j$ coincide. Then there exists a unique f-ring structure on A which induces by localisation in each $S_i$ the structure defined on $A_i$. This f-ring is identified with the projective limit of the diagram

$$ ((A_i)_{i<j \in [1..n]}, (A_{ij})_{i<j \in [1..n]}; (\alpha_{ij})_{i \neq j \in [1..n]}), $$

where $\alpha_{ij}$ are localisation morphisms, in the category of f-rings.

<figure><img src="image_11.png" /></figure>

**Proof.** The ring A is the limit of the projective system formed by $A_i$ and $A_{ij}$ in the category of commutative rings, and therefore also in the category of sets. It follows that there is a unique law $\vee$ on A which gives the $\vee_i$ on the $A_i$ by the canonical maps $A \to A_i$. It remains to check that it satisfies the axioms of the $\vee$ law for an f-ring. This follows from the fact that these axioms are given by equalities between terms, and from the fact that the natural map $\varphi: A \to \prod_i A_i$, on the one hand preserves the laws of the f-ring structure, and on the other hand is injective. □

### • Real schemes

**Remark D.3.6.** A corollary of the gluing Principle D.3.5 is that the notion of a Grothendieck f-scheme is well-defined. An f-scheme seems to be the most natural definition for the notion of a real scheme. Indeed, it allows nilpotents and therefore a good theory of multiplicities in real schemes. But this topic apparently remains largely unexplored. ■

## Rewriting terms in f-rings

Reference: [19].

Contrary to the theory of commutative rings in which the terms are rewritten in a unique normal form, we do not have such a satisfactory result for f-rings. We do, however, have a simplified form, similar to the conjunctive normal form in distributive lattices.

**Lemma D.3.7.** Let A be an f-ring and t be a term written over indeterminates $x_1, \dots, x_n$ and constants in A. This term can be rewritten as

$$ \sup_{i \in I} (\inf_{j \in J_i} (f_{i,j}(x))) $$

for a suitable finite family of polynomials $f_{i,j} \in A[X_1, \dots, X_n]$.

**Proof.** Given the usual rewritings in distributive lattices and given that $x \mapsto -x$ exchanges $\vee$ and $\wedge$, it is sufficient to know how to rewrite $a + (b \vee c)$ and $a(b \vee c)$ in the desired form. This follows from the equality rules gr1, gr16 and afr7. □

<footnote n="8">⁸This is true even if A is trivial: the only case where the Q-algebra in question does not contain Q as a subring.</footnote>
Since the theory *Afr* is purely equational, the preceding lemma is equivalent to its statement restricted to special cases where **A** is an *f*-ring free over a finite set.

**Definition and notation D.3.8.** Let $\mathbf{B} = ((G, R), \mathcal{A}_{fr})$ be a dynamic algebraic structure of $f$-ring. Since the theory $\mathcal{A}_{fr}$ is Horn, $\mathbf{B}$ admits a generic model, denoted $\text{AFR}(\mathbf{B})$, which is the usual $f$-ring defined by the generators $G$ and the relations $R$.

**Lemma D.3.9.**

1. The elements of the ring $\text{AFR}(\mathbf{B})$ can all be written in the form given in Lemma D.3.7 with the $f_{ij} \in \mathbb{Z}[G]$.

2. If $\mathbf{C}$ is a commutative ring, take for $(G, R)$ the positive diagram of $\mathbf{C}$. Then $\text{AFR}(\mathbf{C})$ is the $f$-ring freely generated by the commutative ring $\mathbf{C}$, and the elements of $\text{AFR}(\mathbf{C})$ are written in the form $\sup_{i \in I} (\inf_{j \in J_i} a_{ij})$ with elements $a_{ij}$ of $\mathbf{C}$.

**f-rings of maps, semipolynomials**

For any set $E$ and any $f$-ring $\mathbf{A}$ the ring of maps $f: E \to \mathbf{A}$ is provided with a natural structure of $f$-ring (it is the product structure).

**Definition and notation D.3.10.** Let $\varphi: \mathbf{A} \to \mathbf{B}$ be a morphism of $f$-rings. The ring of $\mathbf{A}$-semipolynomials in $n$ variables<fnref n="9" /> on $\mathbf{B}$ is the $f$-subring of maps $f: \mathbf{B}^n \to \mathbf{B}$ generated by the constants in $\varphi(\mathbf{A})$ and the coordinate maps. It will be noted $\text{Sipd}_n(\mathbf{A}, \mathbf{B})$. We shorten $\text{Sipd}_n(\mathbf{A}, \mathbf{A})$ to $\text{Sipd}_n(\mathbf{A})$.

The definition extends to the case where $\mathbf{A}$ and/or $\mathbf{B}$ are linearly ordered rings, which are considered to be $f$-rings.

Note that it is not really restrictive to suppose that $\varphi$ is injective, which makes it possible to look at $\mathbf{A}$ as an $f$-subring of $\mathbf{B}$.

**Lemma D.3.11.** It is assumed that $\mathbf{A} \subseteq \mathbf{B}$. Any element of $\text{Sipd}_n(\mathbf{A}, \mathbf{B})$ is rewritten as $\sup_{i \in I} (\inf_{j \in J_i} (f_{i,j}))$ for a suitable finite family of polynomials $f_{i,j} \in \mathbf{A}[x_1, \dots, x_n]$.

*Proof.* Very close to proof of Lemma D.3.7. $\square$

<figure><img src="image_12.png" /></figure>

**Examples D.3.12.**

1. The two elements $x \lor (1-x)$ and $1 \lor x \lor (1-x)$ define the same map in $\text{Sipd}_1(\mathbb{Z})$, but not in $\text{Sipd}_1(\mathbb{Q})$.

2. Let $\mathbf{K} = \mathbb{Q}(\epsilon)$ with $\epsilon$ infinitesimal positive and $\mathbf{R}$ the real closure of $\mathbf{K}$.

The semipolynomial $f = x^+ \land -(x^2 - \epsilon)(x^3 - \epsilon)$ defines the null map on $\mathbf{K}$ but does not define a null map on $\mathbf{R}$: the interval $[\epsilon^{1/2}, \epsilon^{1/3}]$ is invisible on $\mathbf{K}$. This example can be simplified by taking $\mathbf{K} = \mathbb{Q}[\epsilon]$ with a suitable nilpotent $\epsilon > 0$. ■

<figure><img src="image_13.png" /></figure>

# D.4. Beyond purely equational theories

## f-rings without zerodivisor

**Lemma D.4.1.** An $f$-ring without zerodivisor is linearly ordered. In other words, if we add the axiom **ASDZ** to the theory $\mathcal{A}_{fr}$, the rule **OT** is valid. In other words, the resulting theory $\mathcal{A}_{frsdz}$ is essentially identical to the theory $\mathcal{A}_{tonz}$ of linearly ordered rings without zerodivisor (see Item 3 of Lemma C.1.6).

$$ \text{ASDZ} \quad xy = 0 \vdash x = 0 \quad \mathbf{op} \quad y = 0 $$

$$ \text{OT} \vdash x \ge 0 \quad \mathbf{op} \quad x \le 0 $$

<footnote n="9">⁹Semipolynomials are often called “SIPD” or “sup-inf-polynomially-defined maps”.</footnote>
*Proof.* Since $x^+x^- = 0$, we obtain the valid rule

$$ \vdash x^+ = 0 \quad \mathbf{op} \quad x^- = 0 $$

☐

## Local f-rings

**Lemma D.4.2.** Let $\mathbf{A}$ be a local f-ring and $x \in \mathbf{A}^\times$, then $x$ is $\ge 0$ or $\le 0$.

*Proof.* Given $x \in \mathbf{A}^\times$, we write $x = x^+ - x^-$, so $x^+ \in \mathbf{A}^\times$ or $x^- \in \mathbf{A}^\times$. Now $x^+x^- = 0$. In the first case we obtain $x^- = 0$, in the second case $x^+ = 0$. ☐

## Strict f-ring

The following theory merges the theories *Afr* and *Aso*. This theory is essentially identical to the one defined in the article [40].

**Definition D.4.3.** The language of the Horn theory *Afr* of strict f-rings is given by the following signature.

$$ \textbf{Signature}: \quad \Sigma_{\mathbf{Afr}} = (\cdot = 0, \cdot \ge 0, \cdot > 0; \cdot + \cdot, \cdot \times \cdot, \cdot \lor \cdot, \cdot \cdot, 0, 1). $$

The axioms are as follows.

* the rules of the purely equational theory *Afr*,

* the direct rules from **asol** to **aso4**, (page 45)

* the Horn rules **col**>, **lv**, **Asol** and **Aso2**, (page 45)

* finally, we have the three rules **sup1**, **sup2** and **Sup** (page 48) to link $\cdot \ge 0$ and $\cdot \lor \cdot$.

We have put the predicate "$\cdot \ge 0$" directly into the language rather than defining it from $\cdot \lor \cdot$.

The meaning of $x > 0$ is not fixed a priori by the axioms. It can range from "$x$ is regular and $\ge 0$" to "$x$ is invertible and $\ge 0$".

**Lemma D.4.4.** Consider the Horn theory of strictly lattice rings to which we add the axiom **OTF**. Then the rule **OTF**$^\times$ is also valid (these rules are recalled below).

$$ \mathbf{OTF} \ x+y>0 \vdash x>0 \quad \mathbf{op} \ y>0 $$

$$ \mathbf{OTF}^\times \ xy<0 \vdash x<0 \quad \mathbf{op} \ y<0 $$

*Proof.* Assume $xy < 0$, hence $x^2y^2 > 0$, hence, by **Aso2**, $x^2 > 0$.

Note that $x^2 = (x^+)^2 + (x^-)^2$. So by **OTF**, it is sufficient to treat the cases $(x^+)^2 > 0$ and $(x^-)^2 > 0$ separately.

If $(x^+)^2 > 0$, we have $xx^+ = (x^+)^2 > 0$, so by **Aso2**, $x > 0$. And again by **Aso2**, we get $y < 0$. If $(x^-)^2 > 0$, we have $-xx^- = (x^-)^2 > 0$, so by **Aso2**, $x < 0$. ☐

## Reduced f-rings

Here we examine the Horn theory *Afrnz* of reduced f-rings. We therefore add to *Afrnz* the axiom **Anz** of reduced rings, which is a simplification rule.

$$ \mathbf{Anz} \ a^2 = 0 \vdash a = 0 $$

The Horn theory *Afrnz* of reduced strict f-rings is the theory obtained from the theory *Afr* by adding as axiom the Horn rule **Anz**.
• Some derived rules

Let us prove in the theory *Afrnz* the four rules **Afrnz1**, **Afrnz2**, **Afrnz3**, and **Aonz** (this last one was introduced page 45).

$$ \mathbf{Afrnz1} \quad x^3 \ge 0 \vdash x \ge 0 $$

We write $x = x^+ - x^-$. Since $x^+ x^- = 0$ we have $x^3 = (x^+)^3 - (x^-)^3 \ge 0$. Multiplying by $x^-$ gives $(x^-)^4 \le 0$, so $(x^-)^4 = 0$. Now the ring is reduced: $x^- = 0$ and $x \ge 0$. $\square$

Note that from **Afrnz1** we deduce the same rule for an arbitrary odd exponent which replaces the exponent 3.

We also have the following reciprocal of the rule **Afr1**.

$$ \mathbf{Afrnz2} \quad ab = 0 \vdash |a| \wedge |b| = 0 $$

Indeed if $ab = 0$, then $(|a| \wedge |b|)^2 \le |a|$, $|b| = 0$, therefore $|a| \wedge |b| = 0$. $\square$

Thus, for $a, b \ge 0$, $ab = 0$ is equivalent to $a \wedge b = 0$.

$$ \mathbf{Afrnz3} \quad a \ge 0, b \ge 0, a^2 = b^2 \vdash a = b $$

Indeed $|a - b|^2 \le |a - b| |a + b| = |a^2 - b^2|$.

Finally

$$ \mathbf{Aonz} \quad c \ge 0, x(x^2 + c) \ge 0 \vdash x \ge 0 $$

Indeed, by **Afr5** we have $x^3 \ge 0$, hence $x \ge 0$ by **Afrnz1**. $\square$

It is now easy to obtain the following result.

**Lemma D.4.5.** In the theory *Afr* the rules **Afrnz1**, **Afrnz2**, **Afrnz3**, **Aonz** and **Anz** are equivalent.

Here is a simple example of the application of Positivstellensatz D.5.6.

**Lemma D.4.6.** In a reduced *f*-ring, the element $c = a \vee b$ is characterised by the following equalities and inequalities

$$ c \ge a, c \ge b, (c - a)(c - b) = 0. $$

More precisely, the theory *Afrnz* proves the following Horn rule

$$ \bullet \quad x \ge a, x \ge b, (x - a)(x - b) = 0 \vdash x = a \vee b. $$

*Proof.* In fact, as the rule is valid for the theory *Codsup*, this follows from Item 3 of Formal Positivstellensatz D.5.6. $\square$

• The rule **FRAC** in *Afrnz*

Recall the rules **FRAC** and **FRAC$_n$**.

$$ \mathbf{FRAC} \quad 0 \le a \le b \vdash \exists z (zb = a^2, 0 \le z \le a) $$

$$ \mathbf{FRAC}_n \quad |u|^n \le |v|^{n+1} \vdash \exists z (zv = u, |z|^n \le |v|) \quad (n \ge 1) $$

Note that the rule **FRAC**, applied with $a = 1$ implies the invertibility of any element $\ge 1$.

We now recall for the theory *Afrnz* the analogue of Lemma C.3.6 for the theory *Co0*.

**Lemma D.4.7.** The addition of the axiom **FRAC** to the theory *Afrnz* can be replaced by the introduction of a function symbol *Fr* with the axioms **fr1** and **fr2** which we recall below

$$ \mathbf{fr1} \vdash \mathrm{Fr}(a, b) |b| = (|a| \wedge |b|)^2 $$

$$ \mathbf{fr2} \vdash 0 \le \mathrm{Fr}(a, b) \le |a| \wedge $$
**Proof.** As in Lemma C.3.6, we can see that it is a question of skolemising an existential rule. This gives an essentially identical theory if we have unique existence. The proof is that of Lemma C.3.5. Assume $yb = zb = a^2$, $0 \le y \le a$ and $0 \le z \le a$. We have $(y - z)b = 0$, $|y - z| \le a \le b^{10}$ and thus $|y - z|^2 \le |y - z|b = 0$. $\square$

**Lemma D.4.8.** In the theory *Afrnz* the rule **FRAC**<sub>2</sub> is deduced from the rule **FRAC** and from the rule asserting the existence of the sixth root ≥ 0 of an element ≥ 0.

*Proof.* Assume $u^2 \le v^3$ and we want to find a $z$ such that $zv = u$ and $z^2 \le v$.

First assume $u \ge 0$ and show that there is a $z$ such that $zv = u$. The rule **FRAC** implies that the fraction $t = \frac{u^4}{v^3}$ is well-defined with $0 \le t \le u^2$. Again **FRAC** gives the fact that the fraction $w = \frac{t^2}{u^2}$ with $0 \le w \le t \le u^2$ is well-defined. We then obtain $u^2wv^6 = t^2v^6 = u^8$. So $u^2(wv^6 - u^6) = 0$. Now $w \le u^2$, so $|wv^6 - u^6| \le u^2(v^6 + u^4)$, hence $|wv^6 - u^6|^2 \le |wv^6 - u^6|u^2(v^6 + u^4) = 0$. Given the rule **Anz**, we get $wv^6 = u^6$. Take $z = w^{\frac{1}{6}}$ and $zv = u$. Furthermore, $z^6 \le u^2 \le v^3$ implies $z^2 \le v$.

For an arbitrary $u$ we write $u = u^+ - u^{-}$; we have $u^2 = (u^+)^2 + (u^-)^2 \le v^3$. We obtain a $z_1$ such that $z_1v = u^+$ and a $z_2$ such that $z_2v = u^-$, we put $z = z_1 - z_2$ and we have $zv = u$. We also get $z^2 \le 2v$. Since $z^2v^2 = u^2 \le v^3$, we have $v^2(z^2 - v) \le 0$. The inequalities $0 \le z^2 \le 2v$ imply $|z^2 - v| \le v$, hence $(z^2 - v)^2 \le v^2$ and $(z^2 - v)^3 \le v^2(z^2 - v) \le 0$, which implies $z^2 - v \le 0$. $\square$

# D.5. Back to ordered fields

## Real f-rings

The real number field satisfies all the Horn rules of the theory of discrete real closed fields, but not all the dynamical rules. Recall the following dynamical rules satisfied by discrete ordered fields.

$$ \text{IV} \quad x > 0 \vdash \exists y xy = 1 $$

$$ \text{ED}_{\#} \vdash x^2 > 0 \quad \text{op} \quad x = 0 $$

$$ \text{OTF} \quad x + y > 0 \vdash x > 0 \quad \text{op} \quad y > 0 $$

$$ \text{OT} \vdash x \ge 0 \quad \text{op} \quad x \le 0 $$

$$ \text{FRAC} \quad 0 \le a \le b \vdash \exists z (zb = a^2, 0 \le z \le a) $$

The real number field verifies **IV**, **OTF** and **FRAC** but neither **ED**<sub>#</sub>, nor **OT**.

The following lemma prepares the definition of the dynamical theory *Aftr*.

**Lemma D.5.1.** In the theory *Afrnz* to which we add the rule **FRAC**, if we define "$x > 0$" as an abbreviation of "$x \ge 0 \wedge \exists z zx = 1$", the predicate $\cdot > 0$ satisfies all the axioms of *Asrnz* where it is present as well as the rule **IV**.

*Proof.* Rules **IV**, **aso1**, **aso2**, **aso4**, **col**<sub>#</sub> are trivially valid. Let's look at the rule **aso3**: an element greater than or equal to a positive invertible element is invertible. This follows from the rule **FRAC** because if $b \ge a > 0$, we have a $z$ such that $zb = a^2$, so $b$ is invertible. For **Aso1**, **Aso2** and **Iv**, we begin by validating the rule $x > 0$, $xu = 1 \vdash u \ge 0$: indeed $u = xu^2 \ge 0$. The rest follows. $\square$

**Definition D.5.2.** We now define the dynamical theory *Aftr* of strongly real f-rings (or to abbreviate, strongly real rings) on the following signature.

$$ \text{Signature} : \quad \Sigma_{\text{Aftr}} = (\cdot = 0, \cdot \ge 0, \cdot > 0 ; \cdot + , \cdot \times , \cdot \vee , \cdot \wedge , \cdot \text{Fr}(\cdot), 0, 1) $$

The axioms of the *Aftr* theory are as follows:

* the axioms of *Afrnz*;

<footnote n="10">¹⁰We are in an *l*-group for addition, we can reason case by case, separately with $0 \le y \le z \le a$ and $0 \le z \le y \le a$. In both cases we obtain $0 \le |z - y| \le a$.</footnote>
• the axioms which define $x > 0$ as an abbreviation of “$x \ge 0 \land \exists z x z = 1$”;

• the axioms **fr1** and **fr2**.

This definition is justified by the fact that the theory of **local** strongly real rings is essentially identical to the theory **Co** of non discrete ordered field: Item 3 of Lemma D.5.4.

**Lemma D.5.3.** The dynamical theory *Aftr* is essentially identical to the theory *Asrnz* to which we add the axioms **IV** and **FRAC**<fnref n="11" />.

*Proof.* The theory *Asrnz* contains in its signature the predicate “· > 0” which is not present in *Afrnz*. When we add the axiom **IV**, we have $x > 0$ if, and only if, $x$ is $\ge 0$ and invertible. Lemma D.5.1 therefore implies that the theory *Afrnz* to which we add the axiom **FRAC** is essentially identical to the theory *Asrnz* to which we add the axioms **IV** and **FRAC**. Finally, Lemma D.4.7 shows that adding the axiom **FRAC** to *Afrnz* is equivalent to adding the function symbol Fr with the axioms **fr1** and **fr2**. □

A strongly real ring is therefore a reduced $Q$-f-algebra in which any element greater than an invertible positive element is itself invertible. Moreover, the validity of the rule **FRAC** adds a little something.

**Lemma D.5.4.**

1. The Horn theory *Asrnz* to which we add as axioms the dynamical rules **IV** and **OTF** is essentially identical to the theory *Co0*.

2. The dynamical theory *Aftr* to which we add the axiom **ED#** is essentially identical to the theory *Codsup* of discrete ordered fields with sup (or to *Cod*).

3. The dynamical theory *Aftr* to which we add the axiom **OTF** is essentially identical to the theory *Co* of non discrete ordered fields: a strongly real local ring is a non discrete ordered field.<fnref n="12" />

*Proof.* 1. Comparing the theories *Co0* (Definition C.3.2) and *Asrnz*, we find in the first the additional axioms **Aonz**, **IV** and **OTF** and the collapse axiom is missing. But collapse follows from **IV** and **Aonz** is deduced from **Anz** (Lemma D.4.5).

NB: The axiom **IV** implies that $x > 0$ is equivalent to “$x$ is $\ge 0$ and invertible”. The axiom **OTF** adds the fact that the ring is local.

2. The new theory is an extension of *Co0* from Item 1. To move on to *Codsup* we need only add **ED#** and **OT**. Since every element is zero or invertible, we are dealing with a discrete field, and the rule **ASDZ** is valid. Lemma D.4.1 then says that the rule **OT** is also valid.

3. Results from Item 1 and Lemmas D.4.7, D.5.1 and D.5.5. □

**Lemma D.5.5.** In a reduced f-ring where the rule **FRAC** is valid, the following rule **AFRL** replaces the rule **OTF** when we define the predicate $a > 0$ as an abbreviation of $a \ge 0 \land \exists z a z = 1$.

$$ \textbf{AFRL} \quad z(x+y) = 1, x+y \ge 0 \vdash \exists u (ux = 1, x \ge 0) \quad \mathbf{op} \quad \exists v (vy = 1, y \ge 0) $$

*Proof.* Direct implication. Assume **A** is local and prove the rule **AFRL**. Since $x + y$ is invertible, $x$ or $y$ is invertible. For example $x \in \mathbf{A}^\times$. By Lemma D.4.2 we have $x \ge 0$ or $x \le 0$. If $x \le 0$, then $y \ge x + y \ge 0$, therefore $y \in \mathbf{A}^\times$ (Lemma D.5.1). Reciprocal. If $x + y$ is invertible, then $x + y \ge 0$ or $x + y \le 0$ (Lemma D.4.2). In the first case, **AFRL** shows that $x$ or $y$ is invertible. In the second case, $-x$ or $-y$ is invertible. □

<footnote n="11">¹¹This implies that the theory *Aftr* defined here is slightly stronger than the one defined in [40].</footnote>

<footnote n="12">¹²We could have avoided introducing the predicate $x > 0$ in *Aftr* because it is defined as an abbreviation. The rule **OTF** should be replaced by the rule **AFRL** in Item 2. The theory would then be a Horn theory. This is hardly surprising since the theory of real closed rings is purely equational and a non discrete real closed field is a local real closed ring.</footnote>
**Formal Positivstellensätze with sup**

For simultaneous collapse, we have already given Theorem D.3.4.

**Formal Positivstellensatz D.5.6** (formal Positivstellensatz, 2).
The following dynamical theories prove the same Horn rules.

1. On the signature ($\cdot = 0, \cdot \ge 0; \cdot + , \cdot \times , \cdot, - , 0, 1$): the theory Aonz of strictly reduced ordered rings (Definition C.1.4), the theory Crcdsup of discrete real closed fields with sup and intermediate theories (for example Afrnz, Atonz, Cod or Co0).

2. On the signature ($\cdot = 0, \cdot \ge 0, \cdot > 0; \cdot + , \cdot \times , \cdot, - , 0, 1$): the Asonz theory of reduced strictly ordered rings, the Crcdsup theory and intermediate theories (for example Asrnz, Cod or Co0).

3. On the signature ($\cdot = 0, \cdot \ge 0; \cdot + , \cdot \times , \cdot, \vee, - , 0, 1$): the Afrnz theory of reduced f-rings, the Crcdsup theory and intermediate theories (e.g. Asrnz, Co0).

4. On the signature ($\cdot = 0, \cdot \ge 0, \cdot > 0; \cdot + , \cdot \times , \cdot, \vee, - , 0, 1$): the theory Asrnz of reduced strict f-rings, the theory Crcdsup and intermediate theories (for example Co and Codsup).

5. On the signature ($\cdot = 0, \cdot \ge 0; \cdot + , \cdot \times , \cdot, \vee, - , \text{Fr}(\cdot, \cdot), 0, 1$): the *Aftr* theory of strongly real rings, the theory *Crcdsup* and intermediate theories (for example *Co* and *Codsup*).

*Proof.* 1 and 2. The theory *Crcdsup* is essentially identical to *Crcd*. So Positivstellensätze C.2.2 and C.2.1 give Items 1 and 2.

3. Since the theories *Atonz* and *Crcd* prove the same Horn rules, Theorem A.5.5 tells us that the theories *Atosupnz* and *Crcdsup* prove the same Horn rules. To have Item 3, it suffices to show that *Afrnz* and *Atosupnz* prove the same Horn rules. As the theories *Afrnz* and *Atosupnz* prove the same Horn rules (formal Positivstellensatz D.3.2) we conclude with Theorem A.5.6.

4. Same reasoning as in the previous item.

5. Note that *Codsup* validates the rules **IV** and **FRAC**, which can be replaced by the introduction of Fr with its two axioms (Lemma D.4.7). On the other hand, the dynamical theory *Aftr* is essentially identical to the theory *Asrnz* to which we add the axioms **IV** and **FRAC** (Item 2 of Lemma D.5.1). Item 5 therefore results from Item 4. □

*Remark D.5.7.* In the theories *Aftr* and *Co*, we have added the function symbol *Fr* with the axioms **fr1** and **fr2**, which increases the Horn rules formulable in these theories. Nevertheless the use of the symbol *Fr* can be eliminated in the Horn rules in favour of the axiom **FRAC** (see the addition of a function symbol page 27 and Lemma C.3.6). As this axiom is satisfied in the stronger theory *Cod*, Positivstellensatz D.5.6 is not affected by the presence of *Fr*. We could also accept the presence of the function symbol *Fr* with the axioms **fr1** and **fr2** in the theory *Codsup*. ■

**Corollary D.5.8.** Consider the dynamical theory *Asrnz* = *Asrnz*(*Q*) of reduced strict *f*-rings.

1. Let $\mathbf{K}$ be a discrete ordered field and $\mathbf{R}$ its algebraic closure. Let $\mathbf{A} = ((G, \text{Rel}), \mathbf{Asrnz}(\mathbf{K}))$ be a dynamic algebraic structure with $G = (x_1, \dots, x_n)$ and $\text{Rel}$ finite. We have an algorithm which decides whether $\mathbf{A}$ collapses and which in case of a negative answer gives the description of a system $(\xi_1, \dots, \xi_n)$ in $\mathbf{R}^n$ which satisfies the constraints given in the relations $\text{Rel}$.

2. We have an algorithm that decides whether a Horn rule of $\mathbf{Asrnz}$ is valid. If the answer is negative, the algorithm gives the description of a system $(\xi_1, \dots, \xi_n)$ in $\mathbf{R}^n_{\text{alg}}$ which contradicts the Horn rule.

3. The same results are valid with $\mathbf{Aftr} = \mathbf{Aftr}(\mathbb{Q} \cap [0,1])$ instead of $\mathbf{Asrnz}$. In this case we add the function symbol $\text{Fr}$ with the two accompanying axioms to $\mathbf{Crcdsup}$.
*Proof.* We have just seen (formal Positivstellensatz D.5.6) that the Horn theory *Asrnz* (resp. *Aftr*) proves the same Horn rules as *Crcdsup* (resp. by adding Fr). Moreover, we see that a Horn rule of *Crcdsup* (possibly by adding Fr) is equivalent to a family of Horn rules of *Crcd*. We can therefore conclude with the concrete Positivstellensatz C.2.6. □

The ring $\mathrm{Sipd}_n(\mathbf{A})$ of semipolynomials over $\mathbf{A}$ in $n$ variables is explained in Definition D.3.10, the $f$-ring $\mathrm{AFR}(\mathbf{A})$ generated by $\mathbf{A}$ is defined in D.3.8.

**Theorem D.5.9.** Fix $n$ and denote $\mathbf{K}[\mathbf{x}] = \mathbf{K}[x_1, \dots, x_n]$.

1. Let $\mathbf{K}$ be a discrete ordered field and $\mathbf{R}$ its real closure. The ring $\mathrm{Sipd}_n(\mathbf{K}, \mathbf{R})$ is identified with the $f$-ring generated by $\mathbf{K}[\mathbf{x}]$. More precisely: the structure of $\mathbf{K}$ gives to $\mathbf{K}[\mathbf{x}]$ a dynamic algebraic structure of $f$-ring and the unique $\mathbf{K}$-morphism of $f$-rings from $\mathrm{AFR}(\mathbf{K}[\mathbf{x}])$ to $\mathrm{Sipd}_n(\mathbf{K}, \mathbf{R})$ is an isomorphism.

2. Let $\mathbf{K}$ be a discrete ordered field and $\mathbf{R}$ its real closure. If every semialgebraic open of $\mathbf{R}^n$ contains points of $\mathbf{K}^n$, the ring $\mathrm{Sipd}_n(\mathbf{K})$ is identified with $\mathrm{AFR}(\mathbf{K}[\mathbf{x}])$.

3. (incomplete proof) If $\mathbf{K}$ is a $\mathbb{Q}$-algebra contained in $\mathbf{R}$, the ring $\mathrm{Sipd}_n(\mathbf{K})$ identifies with $\mathrm{AFR}(\mathbf{K}[\mathbf{x}])$.

*Proof.* It must be shown that if an expression of the form given in Lemma D.3.11 defines the identically zero map, this can be proved using only the Horn rules of reduced $f$-rings.

1. By the Positivstellensatz, the fact that a semipolynomial is zero at any point in $\mathbf{R}^n$ has an algebraic certificate on $\mathbf{K}$. Now *Afrnz* and *Crcdsup* prove the same Horn rules. (For more details on this kind of subject see [26]).

2. Results from the previous item because under the considered hypothesis, a $\mathbf{K}$-semipolynomial not zero everywhere on $\mathbf{R}^n$ is not zero everywhere on $\mathbf{K}^n$.

3. If $\mathbf{K}$ is discrete, this follows from Item 1, because a $\mathbf{K}$-semipolynomial zero on $\mathbf{K}$ is zero on $\mathbb{Q}$ and therefore on $\mathbb{R}$ and a fortiori on the real closure of the field of fractions of $\mathbf{K}$. Apparently, it takes a bit of effort to obtain the result constructively in all generality, whereas it is clear in classical mathematics. It's the same kind of gymnastics as for the complete constructive proof of the solution of the 17th Hilbert problem on $\mathbb{R}$, given in [26]. The bonus is that the solution is then completely explicit, i.e. it does not use any sign test (or dependent choice axiom) on $\mathbb{R}$. □

## D.6. The real lattice and spectrum of a commutative ring

A prime cone of the commutative ring $\mathbf{A}$, i.e. an element of the real spectrum $\mathrm{Sper} \, \mathbf{A}$, can be given as a non-trivial integral quotient ring $\mathbf{A}/\mathfrak{P}$ with a linearly ordered ring structure, in other words as a minimal model of the *Aito*($\mathbf{A}$) theory of non-trivial integral linearly ordered rings based on $\mathbf{A}$ (see Definition A.2.6).

As the theory of nontrivial linearly ordered integral rings is a dynamical theory without existential axioms, the real spectrum is identified with the spectrum of the distributive lattice $\mathrm{Reel}(\mathbf{A})$ obtained by “recopying”<fnref n="13" /> the axioms of the dynamical theory *Aito*($\mathbf{A}$).

To find the usual topology on the set $\mathrm{Spec}(\mathrm{Reel} \, \mathbf{A})$<fnref n="14" /> underlying the real spectrum $\mathrm{Sper} \, \mathbf{A}$, we must consider the lattice based on the only predicate $x > 0$. This gives Definition D.6.2, which corresponds to the following valid dynamical rules in *Cod*

$$ \mathbf{col}_{\#} \ 0 > 0 \vdash \bot $$

$$ \mathbf{aso3} \ x > 0, y > 0 \vdash x + y > 0 $$

$$ \mathbf{aso4} \ x > 0, y > 0 \vdash xy > 0 $$

$$ \mathbf{aso1} \ \vdash \ 1 > 0 $$

$$ \mathbf{OTF} \ x + y > 0 \vdash x > 0 \ \mathbf{op} \ y > 0 $$

$$ \mathbf{OTF}^{\times} \ xy < 0 \vdash x < 0 \ \mathbf{op} \ y < 0 $$

<footnote n="13">¹³As we do below, in Definition D.6.2.</footnote>

<footnote n="14">¹⁴According to the tradition established when the real spectrum was invented.</footnote>
**Remark D.6.1.** If we base ourselves solely on the predicate $x > 0$ and if we introduce the predicate $x \ge 0$ as the opposite of the predicate $-x > 0$, and the predicate $x = 0$ as the conjunction $x \ge 0 \land -x \ge 0$, we obtain on the basis of the previous axioms alone a conservative extension which satisfies all the axioms of *Aito*. The minimal models of the dynamical theory described by the 6 previous axioms are therefore (in classical mathematics) the integral quotients of **A** with a relation of total order. This justifies the following definition: the spectrum of the lattice **Reel A** is indeed identified with the real spectrum of **A** (in classical mathematics). ■

**Definition D.6.2.** The real lattice of a commutative ring **A**, denoted **Reel A**, is the distributive lattice generated by (**A**, $\vdash$) where $\vdash$ is the smallest entailment relation satisfying

$$ \left. \begin{array}{lclcl} 0 & \vdash & & & \vdash 1 \\ x, y & \vdash & x + y & & x + y & \vdash & x, y \\ x, y & \vdash & xy & & -xy & \vdash & x, y \end{array} \right\} \qquad (D.5) $$

This simple and constructive way of defining the real lattice goes back to [10], which was inspired by [Johnstone, Section V-4.11].
# E. Non discrete real closed fields

## Sommaire

<table><tr><td>Introduction</td><td>86</td></tr><tr><td>E.1 2-closed ordered field (or euclidean field)</td><td>86</td></tr><tr><td>E.2 Virtual roots</td><td>87</td></tr><tr><td>Definition and first properties</td><td>87</td></tr><tr><td>A result à la Pierce-Birkhoff</td><td>91</td></tr><tr><td>f-rings with virtual roots</td><td>91</td></tr><tr><td>Domain variant</td><td>92</td></tr><tr><td>Rings of integral continuous semialgebraic maps</td><td>93</td></tr><tr><td>Pierce-Birkhoff rings</td><td>93</td></tr><tr><td>E.3 Real closed rings</td><td>93</td></tr><tr><td>Constructive definition and variants</td><td>93</td></tr><tr><td>Continuous semialgebraic maps</td><td>94</td></tr><tr><td>An example</td><td>94</td></tr><tr><td>Ordered fields with virtual roots</td><td>94</td></tr><tr><td>Formal Positivstellensatz</td><td>94</td></tr><tr><td>Quotient, localisation and gluing of real closed rings</td><td>95</td></tr><tr><td>Comparison with the definition in classical mathematics</td><td>96</td></tr><tr><td>An axiomatic of Niels Schwartz</td><td>96</td></tr><tr><td>The axiomatics of Prestel-Schwartz</td><td>97</td></tr><tr><td>The axiomatics of Marcus Tressl</td><td>98</td></tr><tr><td>E.4 Non discrete real closed fields</td><td>99</td></tr><tr><td>A reasonable definition</td><td>99</td></tr><tr><td>Real closure of a reduced f-ring</td><td>99</td></tr><tr><td>Real closure of a non discrete ordered field</td><td>100</td></tr><tr><td>E.5 A non-archimedean non discrete real closed field</td><td>100</td></tr><tr><td>E.6 Use of virtual roots in constructive real algebra</td><td>104</td></tr><tr><td>Basic semialgebraic subsets of the real line</td><td>104</td></tr><tr><td>Sign and variation tables</td><td>104</td></tr><tr><td>An approximate cylindrical algebraic decomposition (CAD)?</td><td>105</td></tr><tr><td>Stratifications</td><td>105</td></tr><tr><td>The Fundamental Theorem of Algebra (FTA)</td><td>106</td></tr><tr><td>1. The square roots of a complex number c = a + ib.</td><td>106</td></tr><tr><td>2. The general case</td><td>106</td></tr><tr><td>3. The general case in terms of multisets.</td><td>107</td></tr><tr><td>E.7 Some questions</td><td>107</td></tr><tr><td>Continuous semialgebraic maps</td><td>107</td></tr><tr><td>Real closure</td><td>108</td></tr><tr><td>Pierce-Birkhoff</td><td>108</td></tr><tr><td>The 17th Hilbert problem</td><td>108</td></tr><tr><td>The Grail?</td><td>109</td></tr></table>
# Introduction

Section E.1 explains how to introduce square roots of the elements $\ge 0$ into an $f$-ring and in particular into a non discrete ordered field. This is intended as an introduction to the more general notion of virtual roots. The case of discrete ordered fields was treated in [42, section 3.2]. The moral of this case is that we don't need to know whether a square root is already present in the ordered field in order to introduce it formally without any risk of contradiction. Here we see the superiority of the constructive point of view over the classical point of view (which usually uses LEM to decide whether the coveted square root is already present or not).

Section E.2 explains how to add virtual root maps in non discrete ordered fields. Virtual roots were introduced in [27] for discrete ordered fields. The aim was to have, for a real monic polynomial, continuous maps of the coefficients which cover the real roots. In particular, this made it possible to have a constructive version of the intermediate value theorem in which no sign test was used. In fact, similar work can be done on any $f$-ring.

Section E.3 deals with real closed rings and Section E.4 proposes a definition for non discrete real closed fields as local real closed rings. The theory of real closed rings is presented here in an elementary, purely equational form, in the style of [69].

## E.1. 2-closed ordered field (or euclidean field)

As a starting point, let's look at the question of introducing the square roots of the elements $\ge 0$. For the case of a discrete ordered field we refer to [42, section 3.2].

We are interested in the following rule which says that the elements $\ge 0$ are squares.

$$ \mathbf{sqr} \vdash \exists z \geq 0 x^+ = z^2 $$

*Remark E.1.1.* In an $f$-ring, in the presence of nilpotents, two elements $z$ and $y \ge 0$ which have the same square are not necessarily equal, but if the ring is reduced, they are equal, by virtue of the simplification rule *Afrnz3*. So the rule $\mathbf{sqr}$ is a simple existential rule with unique existence and if we solemise this rule in the theory *Afrnz* we get an essentially identical theory. ■

We now present a version in which a nonnegative square root of a nonnegative element is given as a unary law in the dynamical theory which extends *Afr*

$$ \text{Sqr: } \mathbf{R} \to \mathbf{R}, x \mapsto \sqrt{x} \quad \text{in case of a real closed field.} $$

This function symbol must obey the following natural direct rules.

$$ \mathbf{sqr}_- \quad y = 0 \vdash \text{Sqr}(x + y) = \text{Sqr}(x) $$

$$ \mathbf{sqr2} \vdash \text{Sqr}(x) = \text{Sqr}(x^+) $$

$$ \mathbf{sqr0} \vdash \text{Sqr}(0) = 0 $$

$$ \mathbf{sqr3} \vdash \text{Sqr}(x)^2 = x^+ $$

$$ \mathbf{sqr1} \vdash \text{Sqr}(x) \geq 0 $$

$$ \mathbf{sqr4} \vdash \text{Sqr}(x^+ y^+) = \text{Sqr}(x) \text{Sqr}(y) $$

### Definition E.1.2.

* We denote *Afr2c* the purely equational theory of 2-closed $f$-rings: it is obtained from *Afr* by adding the unary function symbol Sqr with the six preceding axioms.

* We denote *Asr2c* the dynamical theory of 2-closed strict $f$-rings obtained from *Asr* in the same way that *Afr2c* was obtained from *Afr*.

* We denote *Co2c* the dynamical theory of 2-closed non discrete ordered fields obtained from *Co* in the same way.

$$ \text{Nota that } \text{Sqr}(x) = 0 \text{ when } x \le 0 \text{ and } \text{Sqr}(x) = \sqrt{x} \text{ when } x \ge 0. $$

**Lemma E.1.3.** A 2-closed $f$-ring is reduced.
*Proof.* On the one hand $|a|^2 = |a^2|$, and on the other hand for a $x \ge 0$ such that $x^2 = 0$, we have the equalities $0 = \mathrm{Sqr}(x^2) = \mathrm{Sqr}(x)^2 = x^+ = x$. $\square$

**Lemma E.1.4.** The following two extensions of the *Afr* theory are essentially identical.

1. *Afr2c*: we have added the function symbol Sqr but the theory remains purely equational since **sqr1** can be written as Sqr(x) = Sqr(x)⁺.

2. Dynamic rules **Anz** and **sqr** are added as axioms (the language is not changed).

*Proof.* First of all, in the theory *Afrnz* the simple existential rule **sqr** has unique existence by virtue of Remark E.1.1. Next, we check that the symbol Sqr obtained by skolemising the existential axiom **sqr** satisfies the 6 desired axioms. $\square$

The following lemma can be seen as a generalisation to the *non* discrete case of the fact that on a 2-closed discrete ordered field, the commutative ring structure completely determines the order structure.

**Lemma E.1.5.** On a commutative ring, if there is a 2-closed $f$-ring structure, it is unique. More generally, a ring morphism between two 2-closed $f$-rings is a 2-closed $f$-ring morphism.

*Proof.* Let $\varphi: \mathbf{A} \to \mathbf{B}$ be a ring morphism where $\mathbf{A}$ and $\mathbf{B}$ are 2-closed $f$-rings. Since $x \ge 0$ are squares, the order relation is respected. Now in a 2-closed $f$-ring (or more generally in a reduced $f$-ring) the element $c = a \lor b$ is characterised by the equalities and inequalities $c \ge a$, $c \ge b$ and $(c-a)(c-b) = 0$ (Lemma D.4.6). We deduce that the ring morphism is also a morphism for $\lor$ laws. Finally, since in a reduced $f$-ring, two elements $\ge 0$ which have the same square are equal (Remark E.1.1), the law Sqr is also respected by the ring morphism. $\square$

Since the theory *Afr2c* is purely equational, any $f$-ring $\mathbf{A}$ freely generates a 2-closed $f$-ring: its 2-closure AFR2C($\mathbf{A}$). The question then arises: what does the 2-closure of an $f$-ring look like? Here's the first clue.

**Lemma E.1.6.** Any reduced $f$-ring injects into its 2-closure.

*Proof.* The theory *Afr2c* proves the same Horn rules as *Afrnz*: this follows from Item 3 of Formal Positivstellensatz D.5.6, because the map Sqr added to the theory *Crcd* gives an essentially identical theory. We therefore do not obtain any new equality between elements of the original $f$-ring after formally adding the square roots of the elements $\ge 0$. $\square$

This generalises the fact that a discrete ordered field is injected into its 2-closure ([42, 43]), which is a discrete ordered field. For the *non* discrete case arises the natural question E.7.6.

**Lemma E.1.7.** The *Co2c* theory is essentially identical to the following two theories.

1. On the signature $(\cdot = 0; \cdot + , \cdot \times , \cdot \lor , \cdot \向 , \cdot, \mathrm{Fr}(\cdot), \mathrm{Sqr}(\cdot), 0, 1)$ the theory obtained from *Afr2c* by adding the function symbol Fr with axioms **fr1**, **fr2**, and the axiom **AFRL**.

2. On the signature $(\cdot = 0, \cdot \ge 0; \cdot + , \cdot \times , \cdot \lor , \cdot \向, 0, 1)$ the theory obtained by adding as axioms to *Asr* the rules **IV**, **OTF**,**FRAC**, **Anz** and **sqr**.

A 2-closed ordered field is also called a 2-closed real field or an euclidean field.

## E.2. Virtual roots

### Definition and first properties

References: [27, 16, 2, 5, 25].

The idea which guided the introduction of virtual roots was to have, for a real monic polynomial, continuous maps of the coefficients which cover the real roots. When a real root disappears in the
complex plane, it can be replaced by the root of the derivative that coincides with the double real root when it disappears.

For example, the virtual square roots of an arbitrary real a (i.e. $-\text{Sqr}(a)$ and $+\text{Sqr}(a)$) are equal to $-\sqrt{a}$ and $\sqrt{a}$ when $a \ge 0$, otherwise they are zero: this is the value they had when they disappeared (imagine the polynomial $X^2 - a$ varying continuously with $a \in \mathbb{R}$).

First, let's recall a purely algebraic version of the mean value theorem in case of polynomials.

**Lemma E.2.1 (algebraic mean value theorem).** [43, 42]

We can construct two families $(\lambda_{i,j})_{1 \le i \le j \le n}$ and $(r_{i,j})_{1 \le i \le j \le n}$ in $\mathbb{Q} \cap (0,1)$, with $\sum_{i=1}^n r_{i,n} = 1$ for all $n \ge 1$ and such that, for any polynomial $f \in \mathbb{Q}[X]$ of degree $\le n$, we have in $\mathbb{Q}[a,b]$:

$$f(b) - f(a) = (b - a) \times \sum_{i=1}^{n} r_{i,n} \cdot f'(a + \lambda_{i,n}(b - a)).$$

The result applies to any $\mathbb{Q}$-algebra $\mathbf{A}$ (in particular to non-discrete ordered fields). If $\mathbf{A}$ is a strictly ordered $\mathbb{Q}$-algebra, this shows that a polynomial whose derivative is $> 0$ on an open interval $(a, b)$ is a strictly increasing map on the closed interval $[a, b]$.

**Example E.2.2.** For example, for polynomials of degree $\le 4$ we have

$$\frac{f(1)-f(-1)}{2} = \frac{1}{3} f'(-\frac{2}{3}) + \frac{1}{6} f'(-\frac{1}{3}) + \frac{1}{6} f'(\frac{1}{3}) + \frac{1}{3} f'(\frac{2}{3}),$$

and more generally, with $\Delta = b - a$

$$f(b) - f(a) = \Delta \cdot \left( \frac{1}{3} f'(a + \frac{1}{6}\Delta) + \frac{1}{6} f'(a + \frac{1}{3}\Delta) + \frac{1}{6} f'(a + \frac{2}{3}\Delta) + \frac{1}{3} f'(a + \frac{5}{6}\Delta) \right).$$

<figure><img src="image_14.png" /></figure>

**Lemma E.2.3 (slight variation on [27, Proposition 1.2]).**

1. Let $\sigma = \pm 1$ and $f: [a, b] \to \mathbb{R}$ ($a \le b \in \mathbb{R}$) be a continuously differentiable map such that $\sigma f'(x) > 0$ on $[a, b]$. Then $|f|$ reaches its minimum at a unique $x \in [a, b]$. We call this real $R(a, b, f)$.

We have $(x-a)(x-b)f(x) = 0$ and $x$ is the only real number satisfying the following system of inequalities.

$$\bullet \ a \le x \le b$$

$$\bullet \ \sigma(x-a)f(a) \le 0$$

$$\bullet \ \sigma(b-x)f(b) \ge 0$$

$$\bullet \ \sigma(x-a)f(x) \le 0$$

$$\bullet \ \sigma(b-x)f(x) \ge 0$$

2. Let $\sigma = \pm 1$ and $f: [a, +\infty) \to \mathbb{R}$ be a continuously differentiable map such that $\sigma f'(x) > 0$ on $(a, +\infty)$. It is assumed that there is a $b > a$ such that $\sigma f(b) > 0$.

Then $|f|$ reaches its minimum at a single $x \in [a, +\infty)$. We denote $R(a, +\infty, f)$ this real. We have $(x-a)f(x) = 0$ and $x$ is the only real verifying the following system of inequalities:

$$\bullet \ a \le x$$

$$\bullet \ \sigma(x-a)f(a) \le 0$$

$$\bullet \ (x-a)f(x) \le 0$$

$$\bullet \ \sigma f(x) \ge 0$$

3. A statement similar to the previous one, left to the reader, for the interval $(-\infty, a]$.

4. This lemma is also valid for a discrete real closed field $\mathbb{R}$ if $f$ is a continuous semialgebraic map continuously derivable on an interval $[a, b]$.

**Remark E.2.4.** 1) In the article [27], when $f$ is a monic polynomial of degree $d$, the hypothesis is formulated in the form $f'(x) \ge 0$ on $[a, b]$, which means that the set of parameters $(a, b$ and the coefficients of $f)$ satisfying the hypothesis is a semialgebraic closure of $\mathbb{R}^{d+2}$. We then show that the map $R(a, b, f)$ is semialgebraically continuous on this closed set.
2) Note that Items 2 and 3 are offset from Item 1. 3) It seems that we can explain a uniform continuity modulus for R if we give certain details about the continuous semialgebraic map $f'$ (details available when f is a monic polynomial). ■

From this lemma we obtain the construction of virtual roots for a monic polynomial of degree $d$: firstly they “cover” all the real roots, and secondly they vary continuously as a function of the coefficients of the polynomial.

For a monic polynomial $f$ of degree $d$, $f^{[k]}$ is the $k$-th derivative of $f$ divided by its leading coefficient ($0 \le k < d$): it is a monic polynomial of degree $d-k$.

**Proposition and definition E.2.5.** Let $\mathbb{R}$ be a discrete real closed field or the field $\mathbb{R}$. For any monic polynomial

$$f(X) = X^d - (a_{d-1}X^{d-1} + \dots + a_1X + a_0) \quad (d \ge 1)$$

we define the maps virtual roots of $f$

$$\rho_{d,j}(f) = \rho_{d,j}(a_{d-1}, \dots, a_0)$$

for $1 \le j \le d$ by induction on $d$: (we abbreviate below $\rho_{k,j}(f^{[d-k]})$ to $\rho_{k,j}$)

$$\bullet \rho_{1,1}(X-a) = \rho_{1,1}(a) := a;$$

$$\bullet \rho_{d,j} := \mathbb{R}(\rho_{d-1,j-1}, \rho_{d-1,j}, f) \text{ for } 1 \le j \le d \ (d \ge 2);$$

By convention we have set $\rho_{d,0} = (-1)^d \infty$ and $\rho_{d,d+1} = +\infty$ for all $d \ge 1$, and the map $\mathbb{R}$ is the one defined in Lemma E.2.3.

This proposition can be proved simultaneously with the Items 3d and 3e of the following theorem, using Lemma E.2.1.

**Theorem E.2.6** (some properties of virtual roots). [27, 16]

Let $\mathbb{R}$ be a discrete real closed field or the field $\mathbb{R}$. Let $\xi$ be an arbitrary element of the field.

1. By Lemma E.2.3, for a given monic polynomial $f$ of degree $d$, the $\frac{d(d+1)}{2}$ elements $\rho_{k,j}(f^{[d-k]})$, $k \in [1..d]$, $j \in [1..k]$, are defined by a system of large inequalities.

2. Each map $\rho_{d,j}: \mathbb{R}^d \to \mathbb{R}$ is uniformly continuous on any ball

$$B_{d,M} := \{(a_{d-1}, \dots, a_0) \mid \sum_i a_i^2 \le M\}, (M > 0).$$

Uniform continuity can be given in fully explicit form on $B_{d,M}$.

3. For a monic polynomial $f$ of degree $d$, note $\tilde{f} = \prod_{j=1}^d (X - \rho_{d,j}(f))$ and $f^* = \prod_{j=0}^{d-1} f^{[j]}$.

We use the conventions $\rho_{d,0}(f) = (-1)^d \infty$ and $\rho_{d,d+1}(f) = +\infty$.

In the following, we fix $f$ and note $\rho_{\delta,j} = \rho_{\delta,j}(f^{[d-\delta]})$ for $1 \le j \le \delta \le d$.

(a) We have $\rho_{d,1} \le \rho_{d-1,1} \le \dots \le \rho_{d-1,j} \le \rho_{d,j+1} \le \dots \le \rho_{d-1,d-1} \le \rho_{d,d}$.

(b) If $d \ge 2$ and $f = X^d - a$, then $\rho_{d,d} = \sqrt[d]{a^+}$, $\rho_{d,j} = 0$ for $1 < j < d$, $\rho_{d,1} + \rho_{d,d} = 0$ if $d$ is even and $\rho_{d,1} + \rho_{d,d} = \sqrt[d]{a}$ if $d$ is odd.

(c) If $f = \prod_{i=1}^d (X - \xi_i)$ for $\xi_i \in \mathbb{R}$, then $\tilde{f} = f$. Consequently $\rho_{d,1} = \bigwedge_i \xi_i$, $\rho_{d,d} = \bigvee_i \xi_i$ and $\rho_{d,k} = \bigwedge_{J \subseteq [1..d], \#J=k} (\bigvee_{i \in J} \xi_i)$.

(d) • If $\rho_{d-1,j} < \rho_{d-1,j+1}$, ($0 \le j \le d-1$), then $f$ is strictly monotonic on the interval, increasing if $d-j$ odd, decreasing otherwise.

• For $0 \le j \le d-1$, we have $(-1)^{d-j} (f(\rho_{d-1,j+1}) - f(\rho_{d-1,j})) \le 0$.

<footnote n="1">¹This implies that in the system of large inequalities which defines the $\rho_{k,j}$ for $k \le d$ and $1 \le j \le k$, the signs (in the broad sense) of the $\Delta$ of Item 1 of Lemma E.2.3 are known, and can be given directly, as in the example which follows the theorem, which simplifies things a little: the $\Delta$ “disappear”.</footnote>
(e) If $\rho_{d,j} < \xi < \rho_{d,j+1}$, $(0 \le j \le d)$, then $(-1)^{d-j}f(\xi) > 0$.

(f) The zeros of $f$ are zeros of $\tilde{f}$, with multiplicity greater than or equal to $\tilde{f}$. More precisely

• If $f(\xi) = 0$, then $\tilde{f}(\xi) = 0$;

• If $|\tilde{f}(\xi)| > 0$, then $|f(\xi)| > 0$;

• If $f^{[j]}(\xi) = 0$ for $j \in [1..k]$, then $\tilde{f}^{[j]}(\xi) = 0$ for $j \in [1..k]$;

• If $f^{[j]}(\xi) = 0$ for $j \in [1..k]$ and $|\tilde{f}^{[k+1]}(\xi)| > 0$, then $|f^{[k+1]}(\xi)| > 0$.

Furthermore, if the multiplicities are known, the difference in multiplicities for $f$ and $\tilde{f}$ is even (for example, a non-zero $\rho_{d,j}$ of $f$ is of even multiplicity in $\tilde{f}$).

(g) The real zeros of $f^*$ are exactly the $\rho_{d,j}$. More precisely

• each $\rho_{d,j}$ is a zero of $f^*$,

• if all $|\xi - \rho_{d,j}|$ are $> 0$, then $|f^*(\xi)| > 0$,

• the polynomial $\tilde{f}$ divides $(f^*)^d$.

(h) Let $a \in \mathbb{R}$ be such that the $|f^{[k]}(a)| > 0$ for $0 \le k \le d$, and let $r$ be the number of sign changes in the sequence of $f^{[k]}(a)$, $(k = d, \dots, 0)$, $(0 \le r \le d)$. Then $\rho_{d,d-r} < a < \rho_{d,d-r+1}$.

(i) (Intermediate Value Theorem)

If $a < b$ and $f(a)f(b) < 0$, we have $\prod_{j=1}^{d} f(\mu_j) = 0$, where $\mu_j = a \lor (b \land \rho_{d,j})$. Special cases.

• If $d$ is odd, then $\prod_{j=1}^{d} f(\rho_{d,j}) = 0$.

• If $0 \le k < \ell \le d$ and $f(\rho_{d-1,k})f(\rho_{d-1,\ell}) < 0$, then $\prod_{j=k}^{\ell-1} f(\rho_{d,j}) = 0$.

• If, according to Item 3h we have $\rho_{d,k} < a < \rho_{d,k+1} < b < \rho_{d,k+2}$, then $f(\rho_{d,k+1}) = 0$.

(j) (Extrema values) The monic polynomial $f$ “attains its upper bound and its lower bound on any closed bounded interval” in the following precise sense: if $a < b$, we have

$$ \sup_{\xi \in [a,b]} f(\xi) = f(a) \lor f(b) \lor \sup_{j=1}^{d-1} f(\nu_j) \quad \text{where} \quad \nu_j = a \lor (b \land \rho_{d-1,j}), \\ \inf_{\xi \in [a,b]} f(\xi) = f(a) \land f(b) \land \inf_{j=1}^{d-1} f(\nu_j). $$

If $f$ has a constant strict sign $\sigma = \pm 1$ on $[a, b]$, we have $\inf_{\xi \in [a,b]} (\sigma f(\xi)) > 0$.

(k) (Minimum in absolute value and non intermediate value)

If $a < b$, we have

$$ \inf_{\xi \in [a,b]} |f(\xi)| = |f(a)| \land |f(b)| \land \inf_{j=1}^{d} |f(\mu_j)|. $$

Furthermore, if the second member is $> 0$, then $f$ has a constant sign on $[a, b]$.

(l) (A bound) If $f(x) = x^d + \sum_{k=0}^{d-1} a_k x^k$ we have $|\rho_{d,j}| \le \sup_{k=0}^{d} (1 + |a_k|) (1 \le j \le d)$.

(m) (Change of variable) Let $f(x) = x^d + \sum_{k=0}^{d-1} a_k x^k$ and $g(x) = x^d + \sum_{k=0}^{d-1} c^{d-k} a_k x^k$ (formally $g(x) = c^d f(x/c)$).

• If $c \ge 0$, we have $\rho_{d,j}(g) = c\rho_{d,j}(f)$ ($1 \le j \le d$).

• If $c \le 0$, we have $\rho_{d,j}(g) = c\rho_{d,j+1-j}(f)$ ($1 \le j \le d$).

• In all cases, $\prod_{1 \le j \le d} (x - c\rho_{d,j}(f)) = \prod_{1 \le j \le d} (x - \rho_{d,j}(g))$.

**Example E.2.7.** We explain here the inequalities mentioned in Item 1 of the previous theorem leading to $\rho_{4,3}(f)$ for a polynomial $f(X) = X^4 - (a_3X^3 + a_2X^2 + a_1X + a_0)$, written here in the form of direct rules without hypotheses. We use the conventions of Item 3 of Theorem E.2.6. Thus, let $\rho_{1,1} = \rho_{1,1}(\frac{a_3}{4})$, $\rho_{2,j} = \rho_{2,j}(\frac{a_3}{2}, \frac{a_2}{6})$, $\rho_{3,j} = \rho_{3,j}(\frac{3a_3}{4}, \frac{a_2}{2}, \frac{a_1}{4})$, $\rho_{4,j} = \rho_{4,j}(a_3, a_2, a_1, a_0)$. The inequalities characterising $\rho_{1,1}$, $\rho_{2,2}$, $\rho_{3,2}$ and $\rho_{4,3}$ are given. Note that in the definition of virtual roots, the sign $\sigma = \pm 1$ before $x-a$ or $b-x$ in Item 1 of Lemma E.2.3 is known because of Item 3d of Theorem E.2.6, which explains why this sign does not appear in the inequalities below.
<table>
  <tbody>
    <tr>
      <td><b>vr</b><sub>1,1</sub> ⊢ ρ<sub>1,1</sub> = <sup>a<sub>3</sub></sup>&frasl;<sub>4</sub></td>
      <td></td>
    </tr>
    <tr>
      <td><b>vr</b><sub>2,1,0</sub> ⊢ ρ<sub>2,1</sub> ≤ ρ<sub>1,1</sub></td>
      <td><b>vr</b><sub>2,1,2</sub> ⊢ (ρ<sub>2,1</sub> - ρ<sub>1,1</sub>) f<sup>[2]</sup>(ρ<sub>2,1</sub>) ≥ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>2,1,1</sub> ⊢ (ρ<sub>2,1</sub> - ρ<sub>1,1</sub>) f<sup>[2]</sup>(ρ<sub>1,1</sub>) ≤ 0</td>
      <td><b>vr</b><sub>2,1,3</sub> ⊢ f<sup>[2]</sup>(ρ<sub>2,1</sub>) ≥ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>2,2,0</sub> ⊢ ρ<sub>1,1</sub> ≤ ρ<sub>2,2</sub></td>
      <td><b>vr</b><sub>2,2,2</sub> ⊢ (ρ<sub>2,2</sub> - ρ<sub>1,1</sub>) f<sup>[2]</sup>(ρ<sub>2,2</sub>) ≤ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>2,2,1</sub> ⊢ (ρ<sub>2,2</sub> - ρ<sub>1,1</sub>) f<sup>[2]</sup>(ρ<sub>1,1</sub>) ≥ 0</td>
      <td><b>vr</b><sub>2,2,3</sub> ⊢ f<sup>[2]</sup>(ρ<sub>2,2</sub>) ≥ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>3,3,0</sub> ⊢ ρ<sub>2,2</sub> ≤ ρ<sub>3,3</sub></td>
      <td><b>vr</b><sub>3,3,2</sub> ⊢ (ρ<sub>3,3</sub> - ρ<sub>2,2</sub>) f<sup>[1]</sup>(ρ<sub>3,3</sub>) ≤ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>3,3,1</sub> ⊢ (ρ<sub>3,3</sub> - ρ<sub>2,2</sub>) f<sup>[1]</sup>(ρ<sub>1,1</sub>) ≥ 0</td>
      <td><b>vr</b><sub>3,3,3</sub> ⊢ f<sup>[1]</sup>(ρ<sub>3,3</sub>) ≥ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>3,2,0</sub> ⊢ ρ<sub>2,1</sub> ≤ ρ<sub>3,2</sub> ≤ ρ<sub>2,2</sub></td>
      <td><b>vr</b><sub>3,2,3</sub> ⊢ (ρ<sub>3,2</sub> - ρ<sub>2,1</sub>) f<sup>[1]</sup>(ρ<sub>3,2</sub>) ≥ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>3,2,1</sub> ⊢ (ρ<sub>3,2</sub> - ρ<sub>2,1</sub>) f<sup>[1]</sup>(ρ<sub>2,1</sub>) ≥ 0</td>
      <td><b>vr</b><sub>3,2,4</sub> ⊢ (ρ<sub>3,2</sub> - ρ<sub>2,2</sub>) f<sup>[1]</sup>(ρ<sub>3,2</sub>) ≥ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>3,2,2</sub> ⊢ (ρ<sub>3,2</sub> - ρ<sub>2,2</sub>) f<sup>[1]</sup>(ρ<sub>2,2</sub>) ≥ 0</td>
      <td></td>
    </tr>
    <tr>
      <td><b>vr</b><sub>4,3,0</sub> ⊢ ρ<sub>3,2</sub> ≤ ρ<sub>4,3</sub> ≤ ρ<sub>3,3</sub></td>
      <td><b>vr</b><sub>4,3,3</sub> ⊢ (ρ<sub>4,3</sub> - ρ<sub>3,2</sub>) f(ρ<sub>4,3</sub>) ≥ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>4,3,1</sub> ⊢ (ρ<sub>4,3</sub> - ρ<sub>3,2</sub>) f(ρ<sub>3,2</sub>) ≥ 0</td>
      <td><b>vr</b><sub>4,3,4</sub> ⊢ (ρ<sub>4,3</sub> - ρ<sub>3,3</sub>) f(ρ<sub>4,3</sub>) ≥ 0</td>
    </tr>
    <tr>
      <td><b>vr</b><sub>4,3,2</sub> ⊢ (ρ<sub>4,3</sub> - ρ<sub>3,3</sub>) f(ρ<sub>3,3</sub>) ≥ 0</td>
      <td></td>
    </tr>
  </tbody>
</table>

■

A result à la Pierce-Birkhoff

We call *polyroot map* a map $\mathbf{R}^m \to \mathbf{R}$ which can be written in the form $\rho_{d,j}(f_1, \dots, f_d)$ for integers $1 \le j \le d$ and polynomials $f_j \in \mathbf{R}[x_1, \dots, x_m]$.

The following theorem à la Pierce-Birhoff is worth noting. It looks like a Nusllstellensatz: it
expresses that there is a purely algebraic reason for a map being semialgebraic continuous and
integral over the ring of polynomials.

**Theorem E.2.8.** ([27, Theorem 6.4]) Let $\mathbf{R}$ be a discrete real closed field and let $g: \mathbf{R}^m \to \mathbf{R}$ be an continuous semialgebraic map integral on the ring $\mathbf{R}[x_1, \dots, x_m]$ (seen as a ring of functions). Then $g$ is a combination by $\vee, \wedge$ and $+$ of polyroot maps $\mathbf{R}^m \to \mathbf{R}$. More precisely, if $g(x)$ is a root of the $Y$-monic polynomial $P(Y, \underline{x})$ of degree $d$, it is expressed as a sup-inf combination of maps of the form

$$
\rho_{d,j}(P) + \sqrt[r]{R_{\ell}^{+} \cdot \left(1 + \sum_{i=1}^{n} x_i^2\right)^s} \quad (\text{E.1})
$$

for $R_\ell \in \mathbf{R}[x_1, \dots, x_m]$ (the second term in the sum (E.1) is also a polyroot map, see Item 3b of
Theorem E.2.6).

Remark. When the map *g* is piecewise polynomial, it cancels a monic polynomial *P*(*Y*) = Π<sup>*d*</sup><sub><i>i</i>=1</sub>(*Y* − *f*<sub>*i*</sub>) for *f*<sub>*i*</sub> ∈ R[x<sub>1</sub>, . . . , x<sub>*m*</sub>]. In the expression obtained by E.1 for *g*, it is the Łojasiewicz inequality which is responsible for the extraction of the *r*-th root in the formula. As for the ρ<sub>*d*,*j*</sub>(*P*) they are sup-inf combinations of the *f*<sub>*i*</sub> (Item 3c of Theorem E.2.6). ■
f-rings with virtual roots

**Example E.2.9.** We take again Example C.1.7 of the $\mathbb{Q}$-linearly ordered algebra $\mathbb{Q}[\alpha]$, with $\alpha > 0$ and $\alpha^6 = 0$. We will see that the constraints imposed on $\rho_{2,2}(f)$, when $f = X^2 - a^2$ and $a \ge 0$, do not necessarily imply that $\rho_{2,2} = a$. The constraints are as follows for $x = \rho_{2,2}$ (note that $\rho_{1,1} = 0$):

$$ \mathbf{vr}_{2,2,0} \vdash 0 \le x $$

$$ \mathbf{vr}_{2,2,2} \vdash x(x^2 - a^2) \le 0 $$

$$ \mathbf{vr}_{2,2,1} \vdash -xa^2 \le 0 $$

$$ \mathbf{vr}_{2,2,3} \vdash (x^2 - a^2) \ge 0 $$

If we take $a = \alpha$, all $x \ge 0$ such that $x^2 = a^2$ fit, and therefore all $\alpha + ya^5$ for $y \in \mathbb{Q}[\alpha]$ are solutions. If we take $a^2 = 0$ the constraints are equivalent to “$x \ge 0$ and $x^3 \le 0$” and any element of the interval $[0, \alpha^2]$ is a solution, including $\zeta = \alpha^2$ whereas $\zeta^2 > 0$. ■

**Lemma E.2.10.** On an f-ring, the system of inequalities satisfied by the virtual roots $\rho_{k,j}$ ($1 \le j \le k \le d$) for a given monic polynomial of degree $d$, if they exist, defines these elements unambiguously.

*Proof.* The uniqueness in question is expressed by means of Horn rules. The theory *Afrnz* proves the same Horn rules as the theory of discrete real closed fields with sup (formal Positivstel-lensatz D.5.6). In the latter theory, uniqueness is guaranteed (Item 1 of Theorem E.2.6). □

Example E.2.9 and Lemmas E.2.10 and E.2.12 justify the following definition.

**Definition E.2.11.**

1. The purely equational theory *Afrnv* of f-rings with virtual roots is obtained as follows from the purely equational theory *Afr*.

* For $1 \le j \le d$ in $\mathbb{N}$, we add a function symbol $\rho_{d,j}$ of arity $d$;

* as axioms we add the inequalities described in Item 1 of Theorem E.2.6;

* we add the following rule vrsup

$$ \textcolor{red}{\mathbf{vrsup}} \vdash \rho_{2,2}(a+b,-ab) = a \lor b. $$

The signature is therefore as follows: $(\cdot = 0; \cdot + \cdot, \cdot \times \cdot, \cdot \lor \cdot, \cdot \land \cdot, (\rho_{d,j})_{1 \le j \le d}, 0, 1)$.

2. In the same way, we define the Horn theory *Asrnv* of strict f-rings with virtual roots from the Horn theory *Asr*.

**Lemma E.2.12.** An f-ring with virtual roots is reduced.

*Proof.* Given the rule vrsup, if $a^2 = 0$, we have with $b = -a$:

$$ 0 = \rho_{2,2}(0,0) = \rho_{2,2}(a+b,-ab) = |a|. $$

□

* Domain variant

**Definition E.2.13 (f-ring with virtual roots, domain variant).**

The Horn theory *Aitorv* of linearly ordered domains with virtual roots is obtained from the Horn theory *Aito* of linearly ordered domains by adding the virtual roots in the same way as the theory *Afrnv* is obtained from the theory *Afr* in Definition E.2.11.

Note that we don't need to put the rule vrsup in the axioms.

**Lemma E.2.14.** A linearly ordered domain with virtual roots is integrally closed and its field of fractions is discrete real closed. Reciprocally, an integrally closed domain whose fraction field is discrete real closed is an integrally closed domain with virtual roots.
*Proof.* Let $\mathbf{A}$ be the domain and $\mathbf{K}$ its field of fractions, which is discrete.

*Direct implication.* A monic polynomial $f \in \mathbf{A}[X]$ satisfies **RCF$_n$** because of Item 3i of E.2.6 and the fact that **K** is discrete. For an arbitrary polynomial of **K**[X] we use the change of variables in Item 3m to reduce to a monic polynomial of **A**[X]. So **K** is discrete real closed. Finally **A** is integrally closed due to Item 3f.

*Reciprocal implication.* The order on $\mathbf{K}$ induces a total order on $\mathbf{A}$. It must be shown that for a monic polynomial $f \in \mathbf{A}[X]$ the $\rho_{d,j}(f)$ are in $\mathbf{A}$. Now they are zeros of $f^*$, a monic polynomial of $\mathbf{A}[X]$, so they are in $\mathbf{K}$, and $\mathbf{A}$ is integrally closed, so they are in $\mathbf{A}$. Thus the maps $\rho_{d,j}(a_0, \dots, a_n)$ defined from $\mathbf{K}^n$ to $\mathbf{K}$ are restricted to maps $\mathbf{A}^n \to \mathbf{A}$. $\square$

## Rings of integral continuous semialgebraic maps

Theorem E.2.8 (for discrete real closed fields) legitimates the following definition.

**Definition and notation E.2.15.** Let $\mathbf{R}$ be an $f$-ring with virtual roots (special cases: an ordered field with virtual roots or a real closed ring). The families $\mathbf{Fsace}_m(\mathbf{R})$ ($m \in \mathbb{N}$) of integral continuous semialgebraic maps are defined as the families of maps $\mathbf{R}^m \to \mathbf{R}$ stable by composition, containing the polynomial maps (with coefficients in $\mathbf{R}$) and the virtual root maps. In other words, an element of $\mathbf{Fsace}_m(\mathbf{R})$ is a map $\mathbf{R}^m \to \mathbf{R}$ defined by a term of the language of $\mathcal{Afrrv}(\mathbf{R})$ with the $m$ variables $x_1, \dots, x_m$ (some of which may be absent).

## Pierce-Birkhoff rings

**Definitions and notations E.2.16.** Let $\mathbf{A}$ be a ring, or more generally a dynamic algebraic structure of an $f$-ring.

1. The ring $\mathbf{AFRNZ}(\mathbf{A})$ is the reduced $f$-ring generated by $\mathbf{A}$.

2. The ring $\mathbf{AFRRV}(\mathbf{A})$ is the $f$-ring with virtual roots generated by $\mathbf{A}$.

3. The ring $\mathbf{Ppm}(\mathbf{A})$ is defined as the $f$-subring of $\mathbf{AFRRV}(\mathbf{A})$ formed by the elements $x$ which cancel a polynomial $\prod_{i=1}^k (X - a_i)$ for $a_i \in \mathbf{A}$.

4. A ring $\mathbf{A}$ is called a *Pierce-Birkhoff ring* when the natural morphism $\mathbf{AFRNZ}(\mathbf{A}) \to \mathbf{Ppm}(\mathbf{A})$ is an isomorphism.

See Question E.7.11.

# E.3. Real closed rings

## Constructive definition and variants

**Definition E.3.1 (real closed rings).** The purely equational theory $\mathcal{Arc}$ of real closed rings is obtained by adding to the theory $\mathcal{Afrrv}$ the function symbol $\text{Fr}$ and the axioms **fr1** and **fr2**. The signature is therefore as follows: $(\cdot = 0; \cdot + \cdot, \cdot \times \cdot, \cdot \vee \cdot, -\cdot, \cdot, (\rho_{d,j})_{1 \le j \le d}, \text{Fr}(\cdot, \cdot), 0, 1)$

**Lemma E.3.2.** On a commutative ring, if there is a real closed ring structure, it is unique. More generally, a ring morphism between two real closed rings is a real closed ring morphism.

*Proof.* Results from the lemmas E.1.5 and E.2.10. $\square$

In the following, when we do not specify otherwise, a real closed ring always designates a ring defined in E.3.1.

**Lemma E.3.3 (variants for $\mathcal{Arc}$).**
1. The theory $\mathcal{Arc}$ can also be obtained from the Horn theory $\mathcal{Aftr}$ by adding the virtual roots in the same way that the theory $\mathcal{Afrrv}$ is obtained from the theory $\mathcal{Aftr}$ in Definition E.2.11. Moreover, given Lemma E.2.12, the axiom **Anz** of the theory $\mathcal{Aftr}$ can be omitted. A real closed ring can therefore be seen as a strongly real ring with virtual roots.

2. The theory $\mathcal{Arc}$ is essentially identical to the theory $\mathcal{Asrrv}$ of strict f-rings with virtual roots to which we add the function symbol Fr and the axioms **fr1** and **fr2**. NB. The predicate $x > 0$ must be added to $\mathcal{Arc}$ as an abbreviation of "$x$ is $\ge 0$ and invertible".

*Proof.* Item 1 is clear. We deduce Item 2 by recalling Lemma D.5.1. □

### Continuous semialgebraic maps

We now take Definition C.5.5 (legitimised by Theorem C.5.4) and extend it to real closed rings. Note that every real closed ring contains a conformal copy of $\mathbb{R}_{\text{alg}}$.

We also assume that we have proved Theorem E.3.16 and its corollaries.

**Definition and notation E.3.4.** Let $\mathbb{R}$ be a real closed ring and a map $f: \mathbb{R}^n \to \mathbb{R}$.

1. (Elementary case) The map $f$ is said to be *semialgebraic continuous* (in an elementary way) if there exists a semialgebraic continuous map $g: \mathbb{R}_{\text{alg}}^n \to \mathbb{R}_{\text{alg}}$ expressed by a term $t(x_1, \dots, x_n)$ of $\mathcal{Arc}$ and if $f$ coincides with the map defined by this term.

2. (General case) The map $f$ is *semialgebraic continuous* if there exists an integer $r \ge 0$, elements $y_1, \dots, y_r \in \mathbb{R}$ and a map $h: \mathbb{R}^{r+n} \to \mathbb{R}$ which belongs to the previous elementary case such that

$$ \forall x_1, \dots, x_n \in \mathbb{R} \ f(x_1, \dots, x_n) = h(y_1, \dots, y_r, x_1, \dots, x_n). $$

We denote $\mathfrak{Fsac}_n(\mathbb{R})$ the ring of these maps (it is a real closed ring for the natural order relation). Theorem C.5.4 shows that for a discrete real closed field $\mathbb{R}$ we find the usual definition of continuous semialgebraic maps.

For a comparison of $\mathfrak{Fsac}_n(\mathbb{R})$ with $\mathfrak{Fsace}_n(\mathbb{R})$ see the question E.7.3.

### An example

**Proposition E.3.5.** Let $\mathbb{R}$ be an f-ring with virtual roots and let $f: \mathbb{R}^n \times \mathbb{R}^p \to \mathbb{R}$ be a continuous semialgebraic map. The map

$$ g: \mathbb{R}^p \to \mathbb{R}, \underline{x} \mapsto \sup_{\underline{z} \in [0,1]^n} f(\underline{z}, \underline{x}) $$

is well-defined and continuous semialgebraic.

*Proof.* Given the ad hoc definition of the rings $\mathfrak{Fsac}_m(\mathbb{R})$ we are immediately reduced to the case where $\mathbb{R} = \mathbb{R}_{\text{alg}}$. □

See also the questions E.7.5.

## Ordered fields with virtual roots

**Definition E.3.6.** (Compare with Definition E.2.11, see Lemma E.2.10).

1. The dynamical theory *Corv* of ordered fields with virtual roots is obtained as follows from the dynamical theory *Co*.

* For $1 \le j \le d$ in $\mathbb{N}$, we add a function symbol $\rho_{d,j}$ of arity $d$;

* As axioms, we add the inequalities described in Item 1 of Theorem E.2.6;

2. The dynamical theory *Co0rv* is obtained in the same way from the theory *Co0*.

3. The dynamical theory *Codrv* is obtained in the same way from the theory *Cod*.

*Remark.* The theory *Codrv* is essentially identical to the theory obtained by adding to *Co0rv* the axiom “of third excluded” $\mathbf{ED}_{\#}$ (see remark C.3.3).
Formal Positivstellensatz

**Formal Positivstellensatz E.3.7** (formal Positivstellensatz, 3).

1. The theories *Codrv*, *Crcd* and *Crcdsup* are essentially identical.

2. The following dynamical theories prove the same Horn rules (written in the language of *Afrrv*).

(a) The theory *Afrrv* of *f*-rings with virtual roots.

(b) The theory *Arc* of real closed rings.

(c) The theory *Codrv* of discrete ordered fields with virtual roots.

3. The following dynamical theories prove the same Horn rules (written in the language of *Asrrv*).

(a) The theory *Asrrv* of strict *f*-rings with virtual roots.

(b) The theory *Corv* of ordered fields with virtual roots.

(c) The theory *Codrv* of discrete ordered fields with virtual roots.

4. Theorem E.2.6 is entirely valid for the theory *Asrrv* (thus also for *Corv*). The same is true for the purely equational theory *Afrrv* (so also for *Arc*) if the points which use the predicate · > 0 are deleted or suitably reformulated with · ≥ 0.

*Proof*. The first point is clear. Items 2 and 3 are therefore variants of formal Positivstellensatz D.5.6 taking into account Theorem A.5.5.

Finally, for Item 4, it follows from previous Items that the assertions of Items 2 and 3 of The-
orem E.2.6 can be written in the form of Horn rules.
☐

In classical mathematics given the general representation theorem A.5.4, the formal Positivstl-
lensätze stated so far give the following results, which can be seen in classical mathematics as
characterising the dynamical theories under consideration.

**Corollary\* E.3.8.** On their respective signatures, the following objects are all isomorphic to sub*T*-structures of products of discrete real closed fields (considered with the predicate *x* > 0 and the maps sup, Fr and *ρ*<sub>*d,j*</sub>).

• A reduced *f*-ring (theory *Afrnz*).

• A reduced strict *f*-ring (theory *Asrnz*).

• A strongly real ring (theory *Aftr*).

• A local *f*-ring (theory *Co*).

• An *f*-ring with virtual roots (theory *Afrrv*).

• A real closed ring (theory *Arc*).

• A strict *f*-ring with virtual roots (theory *Asrrv*).

• An ordered field with virtual roots (theory *Corv*).
## Quotient, localisation and gluing of real closed rings

**Lemma E.3.9 (quotient structure).** Let $\mathbf{A}$ be a real closed ring and $I$ a radical ideal. Then $\mathbf{A}/I$ is a real closed ring.

*Proof.* Let us first show that the radical ideal $I$ is solid. We must first show that if $x \in I$, then $|x| \in I$: indeed $|x|^2 = x^2 \in I$. Then if $0 \le |x| \le y$ with $y \in I$, we must show that $x \in I$. Now, by **FRAC**, $y$ divides $|x|^2 = x^2$, so $x^2 \in I$, then $x \in I$. The quotient $\mathbf{A}/I$ is therefore an $f$-ring. Next we need to see that the virtual root maps $\rho_{d,j}$ and the map “fraction” $\text{Fr}$ “pass to the quotient”. Now these maps, when they exist in a reduced $f$-ring, are well-defined by the systems of inequalities they satisfy (Lemma E.2.10). As these inequalities pass to the quotient, everything is in order. $\square$

**Lemma E.3.10 (localisation).** Let $\mathbf{A}$ be a real closed ring and $S$ be a monoid. Then $S^{-1}\mathbf{A}$ is a real closed ring.

*Proof.* We already know that $S^{-1}\mathbf{A}$ has a $\vee$ law which makes it an $f$-ring. Let's see what happens to the virtual roots. Let's take Example E.2.7 with a polynomial $f(X) = X^4 - (\frac{a_3}{s}X^3 + \frac{a_2}{s}X^2 + \frac{a_1}{s}X + \frac{a_0}{s})$ with $a_i \in \mathbf{A}$ and $s \in S^+$. In $S^{-1}\mathbf{A}$ with $Y = sX$ we have

$$s^4 f(X) = Y^4 - (a_3 Y^3 + s a_2 Y^2 + s^2 a_1 Y + s^3 a_0) = Y^4 - (b_3 Y^3 + b_2 Y^2 + b_1 Y + b_0) = g(Y)$$

and therefore also $s^4 g(\frac{Y}{s}) = f(X)$. Consider the virtual roots $\rho_{i,j}$ for the monic polynomial $g$ of $\mathbf{A}[Y]$ with $(i,j)$ equal to $(1,1)$, $(2,1)$, $(2,2)$, $(3,3)$, $(3,2)$, $(4,3)$, and finally the $\rho'_{i,j} = \frac{\rho_{i,j}}{s}$. We see that the inequalities in Example E.2.7, just as they are satisfied for the $\rho_{i,j}$ with respect to the polynomial $g$ in $\mathbf{A}[Y]$, are ipso facto satisfied for the $\rho'_{i,j}$ with respect to the polynomial $f$ in $S^{-1}\mathbf{A}[X]$. These inequalities completely characterise the virtual roots when they exist (Lemma E.2.10).

A similar reasoning works for the map $\text{Fr}(\cdot, \cdot)$. $\square$

**Concrete local-global principle E.3.11 (concrete gluing of real closed rings).**

Let $S_1, \dots, S_n$ be comaximal monoids of a ring $\mathbf{A}$. Let $\mathbf{A}_i$ denote $\mathbf{A}_{S_i}$, $\mathbf{A}_{ij}$ denote $\mathbf{A}_{S_i S_j}$, and assume that a structure of type $\mathcal{Arc}$ is given on each $\mathbf{A}_i$. It is further assumed that the images in $\mathbf{A}_{ij}$ of the laws of $\mathbf{A}_i$ and $\mathbf{A}_j$ coincide. Then there exists a unique structure of real closed ring on $\mathbf{A}$ which induces by localisation in each $S_i$ the structure defined on $\mathbf{A}_i$. This real closed ring is identified with the projective limit of the diagram

$$((\mathbf{A}_i)_{i<j \in [1..n]}, (\mathbf{A}_{ij})_{i<j \in [1..n]}; (\alpha_{ij})_{i<j \in [1..n]}),$$

where $\alpha_{ij}$ are localisation morphisms, in the category of real closed rings.

*Proof.* We copy, mutatis mutandis, the proof of the concrete local-global principle D.3.5 for $f$-rings. $\square$

*Remarks.* 1) This implies that the notion of a real closed scheme is well-defined.

2) The analogous concrete local-global principles, with the same proof, are valid for reduced $f$-rings, for strongly real rings, and for $f$-rings with virtual roots. $\blacksquare$

## Comparison with the definition in classical mathematics

References: [63, 56, 69].

The structure of real closed ring is defined by N. Schwartz in a very abstract way in his Phd [62, Schwartz, 1984]. An axiomatisation as a coherent theory was proposed in [56, Prestel & Schwartz, 2002] (see Definition E.3.14 and Proposition E.3.15).

The aim of N. Schwartz was to give an abstract description of the rings of continuous semialgebraic maps on semialgebraic closures for a fixed real closed field $\mathbb{R}$, and to define abstract “real closed spaces”.

### • An axiomatic of Niels Schwartz

Here is the definition of real closed rings in classical mathematics given in [63, Schwartz, 1986].
**Definition**\* E.3.12. A ring real closed is a reduced ring A satisfying the following properties.

1. The set of squares of A is the set of $\ge 0$ elements of a partial order which makes A an f-ring.

2. If $0 \le a \le b$, there exists $z$ such that $zb = a^2$ (convexity axiom).

3. For any prime ideal p, the residual ring A/p is integrally closed and its field of fractions is a real closed field.

**Proposition**\* E.3.13. In classical mathematics, Definitions E.3.1 and E.3.12 are equivalent.

*Proof.* Direct. For a real closed ring A of Definition E.3.12, the virtual root maps are well-defined, as we know that all continuous semialgebraic maps defined on $\mathbb{R}_{\text{alg}}$ are defined on A. The same applies to the map “fraction” Fr.

*Reciprocal.* For a real closed ring A of Definition E.3.1, we must show that Item 3 of Definition E.3.12 is satisfied. Given a prime ideal p, the residual ring A/p has no zerodivisors and is therefore linearly ordered (Lemma D.4.1). It is also a real closed ring by Lemma E.3.9. Lemma E.2.14 tells us that A/p is integrally closed and that its field of fractions is a real closed field. $\square$

## • The axiomatics of Prestel-Schwartz

The article [56, Prestel & Schwartz, 2002] shows in classical mathematics that the real closed ring structure of Definition E.3.12 is described by a coherent theory. The existential axioms proposed by the authors to replace Item 3 of E.3.12 are very sophisticated and the proof is also an astonishing tour de force.

**Definition E.3.14.** (Prestel-Schwartz real closed rings) A commutative ring is said to be real closed if it satisfies the following axioms.

i-iv) The commutative ring A is reduced, the elements $\ge 0$ are exactly the squares and the order relation makes A a convex f-ring (axiom CVX)

v) For each $d \ge 1$, let $f(x) = x^{2d+1} + \sum_{k=0}^{2d} a_k x^k$, $\delta = \text{discr}_x(P)$ its discriminant, and $g(x) = x^{2d+1} + \sum_{k=0}^{2d} \delta^{2(2d+1-k)} a_k x^k$, we pose the axiom

$$ \vdash \exists z g(z) = 0 $$

vi) For each $d \ge 1$ we pose the axiom

$$ x^d + \sum_{k=0}^{d-1} a_k x^k y^{d-k} = 0 \vdash \exists z_1, \dots, z_d y(x - z_1 y) \cdots (x - z_d y) = 0 $$

**Proposition E.3.15.** In the theory *Arc* the axioms of Definition E.3.14 are valid dynamical rules.

*Proof.* Recall that Theorem E.2.6 is fully valid in the theory *Arc* (Item 4 of E.3.7).

Let's look at the axiom vi). Let $f = x^d + \sum_{k=0}^{d-1} a_k x^k$ and $g = x^d + \sum_{k=0}^{d-1} a_k x^k y^{d-k}$.

We denote $\tilde{f} = \prod_{1 \le j \le d} (x - \rho_{d,j}(f))$ and $\tilde{g} = \prod_{1 \le j \le d} (x - \rho_{d,j}(g))$. Item 3m of Theorem E.2.6 gives the equality

$$ \prod_{1 \le j \le d} (x - y \rho_{d,j}(f)) = \prod_{1 \le j \le d} (x - \rho_{d,j}(g)). $$

Moreover, Item 3f of Theorem E.2.6 for the polynomial g gives

$$ x^d + \sum_{k=0}^{d-1} a_k x^k y^{d-k} = 0 \vdash (x - \rho_{d,1}(g)) \cdots (x - \rho_{d,d}(g)) = 0. $$

We therefore obtain in the *Arc* theory, by taking $z_k = \rho_{d,k}(f)$, the valid rule

$$ x^d + \sum_{k=0}^{d-1} a_k x^k y^{d-k} = 0 \vdash (x - z_1 y) \cdots (x - z_d y) = 0. $$
Let's look at the axiom v). We will show that the element $z$ whose existence is asserted can be chosen as a continuous semialgebraic map of the parameters $a_k$. Since this map is cancelled by the monic polynomial $Q$ we then conclude by the theorem “à la Pierce-Birkhoff” E.2.8. Given the formal Positivstellensatz E.3.7 (Item 2) we need only prove the validity of the rule in the theory *Codrv*. Let us therefore consider a discrete real closed field and, in the parameter space, a connected component of the open $\{ \deltata \neq 0 \}$. On this connected component, the real zeros of $f$ are simple (there is at least one because the degree is odd) and vary continuously as a function of the parameters. Those of $g$ are simply multiplied by $\delta^2$. So on this connected component we have the element $z$ sought as a continuous semialgebraic function of the parameters by choosing the largest of the real zeros. As we approach an edge of a related component, these zeros tend towards 0 (they are zeros of $f$ multiplied by $\delta^2$). So these continuous semialgebraic maps join together to form a global continuous semialgebraic map. $\square$

In classical mathematics, the reciprocal implication is demonstrated: the Prestel-Schwartz axioms imply the existence of virtual roots (because they are continuous semialgebraic maps). This gives the equivalence in classical mathematics of our axiomatics and that of Prestel-Schwartz.

### • The axiomatics of Marcus Tressl

A more elementary version, similar to the one we propose, for the theory of real closed rings can be found in [69, Tressl, 2007] (see also [63, 61, 65, 64]). In this paper, a real closed ring is an $f$-ring $\mathbb{R}$ on which are given all continuous semialgebraic maps defined on $\mathbb{R}_{\text{alg}}$, and for which all algebraic identities linking these maps on $\mathbb{R}_{\text{alg}}$ are satisfied in $\mathbb{R}$.

A good analysis of the classical mathematical articles on real closed rings should allow us to understand why it is enough to add the fractions allowed by the rule **FRAC** to an $f$-ring with virtual roots to be able to capture all the continuous semialgebraic maps $\mathbb{R}_{\text{alg}}^m \to \mathbb{R}_{\text{alg}}$. This is the subject of the following concrete results, which are valid in classical mathematics, but for which we would like a constructive proof. See in particular the question E.7.2.

Recall that according to the finiteness theorem ([Bochnak, Coste & Roy, Theorem 2.7. 1]) the graph $G_f = \text{totq}(\underline{x}, y)\underline{x} \in \mathbb{R}^n, y = f(\underline{x})$ of a continuous semialgebraic map $f: \mathbb{R}_{\text{alg}}^n \to \mathbb{R}_{\text{alg}}$ is a semialgebraic closure of $\mathbb{R}_{\text{alg}}^{n+1}$ which can be described as the zero set a semipolynomial map $F: \mathbb{R}_{\text{alg}}^{n+1} \to \mathbb{R}_{\text{alg}}, i. e. a map written in the form

$$ \sup_i (\inf_{1 \le j \le k_i} p_{ij}) \quad \text{where } p_{ij} \in \mathbb{R}_{\text{alg}}[x_1, \dots, x_n, y] $$

We can decide whether such a graph is that of a continuous semialgebraic map. The following theorem means that in such a case we can prove the existence of $y$ depending on $x_i$ directly in the purely equational theory $\mathcal{Arc}$.

**Theorem E.3.16.** Any continuous semialgebraic map $\mathbb{R}_{\text{alg}}^n \to \mathbb{R}_{\text{alg}}$ can be defined by a term of the theory $\mathcal{Arc}$.

**Corollary E.3.17.** The axiomatisation proposed in E.3.1 for real closed rings is equivalent to that proposed by Tressl [69].

**Corollary E.3.18.** Let $\mathbb{R}$ be a real closed ring. Any continuous semialgebraic map $\mathbb{R}^n \to \mathbb{R}$ (Definition E.3.4) is defined by a term of $\mathcal{Arc}(\mathbb{R})$ with $n$ free variables.

The following corollary is more problematic, can we return to the case $\mathbb{R} = \mathbb{R}_{\text{alg}}$?

**Corollary E.3.19.** Consider a real closed ring $\mathbb{R}$, a continuous semialgebraic map $g: \mathbb{R}^n \to \mathbb{R}$ (an element of $\text{Fsac}_n(\mathbb{R})$) and a polynomial $p \in \mathbb{R}[x_1, \dots, x_n]$ with at least one invertible coefficient. We assume that, on the set $\{ \xi \in \mathbb{R}^n \mid |p(\xi)| > 0 \}$, the fraction $f = g/p$ satisfies a uniform continuity modulus on all bounded subsets à la Łojasiewicz (as in Lemma C.5.3). Then there exists a unique continuous semialgebraic map $h: \mathbb{R}^n \to \mathbb{R}$ such that $hp = g$.

When the axiom **OTF** is added, Theorem E.3.16 gives the following corollary.

**Corollary E.3.20.** The theories $\text{Crc1}$ and $\text{Corv}$ are essentially identical.
# E.4. Non discrete real closed fields

## A reasonable definition

**Lemma E.4.1.** A real closed ring is local if, and only if, it satisfies the rule **AFRL**.

*Proof.* See Lemma D.5.5. □

We now propose for the theory of non discrete real closed fields a formulation essentially identical to *Corv*, but almost purely equational. The rule **AFRL** is preferred to the rule **OTF** because we do not introduce the predicate $\cdot > 0$ which would take us out of the purely equational theories for *Arc*.

**Definition E.4.2.** The dynamical theory of non discrete real closed fields, denoted *Crc2*, is the extension of the purely equational theory *Arc* obtained by adding the rule **AFRL**. In other words, a non discrete real closed field is nothing other than a local real closed ring.

**Proposition E.4.3.** The theories *Corv*, *Crc1* and *Crc2* are essentially identical (we must define the predicate $> 0$ which we add to *Crc2*).

*Proof.* Corollary E.3.20 compares *Corv* and *Crc1*. Lemma D.5.4 tells us that a non discrete ordered field is none other than a local strongly real ring. In other words, the theory *Co* is essentially identical to the theory *Aftr* to which we add the axiom **AFRL**. Let's start with *Aftr*. If we add the virtual roots then **AFRL** we pass to *Arc* (Lemma E.3.3 Item 1) then to *Crc2*. If we add **AFRL** then the virtual roots we go to *Co* then to *Corv*. □

*Remarks* E.4.4.

1) The field $\mathbb{R}$ is a constructive model of the theory *Crc2*.

2) The theory *Crcd* of discrete real closed fields is essentially identical to the theory obtained by adding to *Crc2* the axiom **ED#** which says that equality is decidable.

3) The theory *Crc2* is nothing other than the theory of local real closed rings. However, there are local real closed rings which are not fields in Heyting's sense. For example, consider the ring **A** of continuous semialgebraic maps on $\mathbb{R}_{\text{alg}}$, and let **B** = $S^{-1}\mathbb{A}$ where *S* is the monoid of maps *f* such that $f(0) \neq 0$. It is the ring of germs at (0) of maps $f \in \mathbb{A}$. An element $f \in \mathbb{A}$ is $> 0$ in **B** (resp. $\leq 0$ in **B**) if, and only if, $f(0) > 0$ in $\mathbb{R}_{\text{alg}}$ (resp. $f(x) \leq 0$ in the neighbourhood of 0). This shows that **HOF** is not satisfied in **B**, because it is not enough for $f(0) \leq 0$ for *f* to be $\leq 0$ in the neighbourhood of 0. Note that this locally real closed ring admits two minimal prime ideals, with the respective locals being the germs of maps to the right (or left) of 0.

4) The theory *Crc2* can be used to prove the existence of a square root for a complex number of modulus 1. The unit circle $\{x^2 + y^2 = 1\}$ is covered by the open areas $\{x > -1\}$ and $\{x < 1\}$, on each of which the existence is guaranteed by a continuous map. However, this existence cannot be proved in *Arc*, because in this purely equational theory, every existence is certified by a term, and every term defines a continuous semialgebraic map. ■

## Real closure of a reduced *f*-ring

Given a reduced *f*-ring **A**, we know (Positivstellensatz D.5.6) that the theory *Crcdsup*(**A**) proves the same Horn rules as *Afrnz*(**A**). The same applies to all intermediate theories, in particular to the theories *Afrrv* and *Arc*.

As the latter are purely equational theories, the reduced *f*-ring **A** gives rise to an *f*-ring with virtual roots *AFRRV*(**A**) and a real closed ring *ARC*(**A**).

Since the theories *Afrnz*, *Afrrv* and *Arc* prove the same Horn rules, **A** is a substructure (of *f*-ring) of *AFRRV*(**A**) which is itself a substructure (of *f*-ring with virtual roots) of *ARC*(**A**). In other words, adding the symbols for virtual roots and fractions (with their axioms) does not change **A** as an *f*-ring.
These two constructions of “real fences” are without mystery, and unique to within a single isomorphism.

We are in the same situation as for the construction of the real closure of a discrete ordered field ([43, 42]), but here the result seems completely obvious whereas it requires a non-negligible effort in the articles quoted. The main reason for this (very small) miracle is that we are relying here on a constructive proof of the Positivstellensatz. The secondary reason is that we are dealing here only with Horn theories (instead of dynamical theories).

*Remark E.4.5.* A construction of the real closure of a discrete ordered field $\mathbf{K}$ can also be obtained according to the following argument. We begin by establishing the simultaneous collapse of the theory of discrete ordered fields and that of discrete real closed fields (as in [17, Theorem 3.6]). This is a variant of the formal Positivstellensatz. Then we dynamically evaluate $\mathbf{K}$ as a discrete real closed field. This forces us to introduce the real zeros of any polynomial, with a Thom coding for each of them (for a polynomial which cancels this zero). Since no ambiguity is possible, the dynamic algebraic structure constructed is in fact a usual algebraic structure of a real closed field. This construction is admittedly less detailed than the one explained in [42], but it is essentially equivalent. In fact, in the other direction, we could probably deduce Theorem 3.6 of [17] from the construction given in [42]. What improves [34] and [17] on the previous result is, on the one hand, that the formal Positivstellensatz is more general (Theorem 3.8 in [17]), and on the other hand, and above all, that the concrete Positivstellensatz is demonstrated. ■

## Real closure of a non discrete ordered field

Let us consider a discrete ordered field, i.e. a model $\mathbf{K}$ of the theory $\mathcal{C}o$. We know that $\mathcal{C}orv$ proves the same Horn rules as $\mathcal{C}o$.

Let us denote $\mathbf{R}$ the dynamic algebraic structure $\mathcal{C}orv(\mathbf{K})$.

All the closed terms of the dynamic algebraic structure $\mathbf{R}$ are constructed on elements of $\mathbf{K}$ by means of the function symbols given in the signature (polynomials, virtual roots, legitimate fractions).

The dynamic structure $\mathbf{R}$ is a natural candidate to be the (usual) algebraic structure of type $\mathcal{C}orv$ generated by $\mathbf{K}$, if one exists. However, the problem is that $\mathbf{R}$ is a dynamic algebraic structure of type $\mathcal{C}orv$, but not necessarily a model of this theory, because this dynamical theory is defined with non-algebraic axioms.

We can first consider the usual real closed ring algebraic structure $\mathbf{ARC}(\mathbf{K})$ which is identified with the dynamic algebraic structure $\mathcal{Arc}(\mathbf{K})$. The question is: is the axiom TsbfAFRL a valid rule in $\mathbf{ARC}(\mathbf{K})$? In other words, is $\mathbf{ARC}(\mathbf{K})$ a model of $\mathcal{C}orv$? In which case we can identify $\mathbf{R}$ (dynamic algebraic structure) and $\mathbf{ARC}(\mathbf{K})$ (usual algebraic structure).

The answer is not obvious (see Question E.7.7).

## E.5. A non-archimedean non discrete real closed field

In this section we describe an example of a non-archimedean non discrete real closed field. Let $\varepsilon$ be an indeterminate. In Section C.4 we introduced the ordered non-archimedean non discrete ordered field $\mathbf{Q} = \mathbf{Z}[1/\varepsilon]$ where $\mathbf{Z} = \mathbb{Q}[[\varepsilon]]$ is the ring of formal series in $\varepsilon$ with rational coefficients where $\varepsilon$ is a strictly positive infinity.

In fact, the coefficients of the series under consideration could have been taken from any discrete ordered field, in particular from the field $\mathbb{R}_{\text{alg}}$ of algebraic real numbers. We will denote $\mathbf{R}_0 = \mathbb{R}_{\text{alg}}[[\varepsilon]]$ the analogue of $\mathbf{Z}$ and $\mathbf{R} = \mathbf{R}_0[1/\varepsilon]$ the analogue of $\mathbf{Q}$.

We now extend these constructions to the field $\mathbf{P}$ of Puiseux series with real algebraic coefficients.

First we have the rings of series $\mathbf{P}_{0,d} = \mathbb{R}_{\text{alg}}[[\varepsilon^{1/d}]]$ for the integers $d \ge 1$, all isomorphic to $\mathbf{R}_0$, with the inclusion morphisms $\mathbf{P}_{0,d} \to \mathbf{P}_{0,dd'}$. This forms an inductive system whose limit $\mathbf{P}_0$ (the Puiseux series of valuation $\ge 0$) can be seen as the union of $\mathbf{P}_{0,d}$.

Finally, the Puiseux series themselves form the ring defined as $\mathbf{P} := \mathbf{P}_0[1/\varepsilon]$.
Note that $\mathbf{P}_{j,d} = \{ \alpha \in \mathbf{P}_{0,d}[1/\varepsilon] | \alpha/\varepsilon^{j/d} \in \mathbf{P}_{0,d} \}$. We have $\mathbf{P} = \bigcup_{j,d} \mathbf{P}_{j,d}$.

We introduce notations which generalise to $\mathbf{P}_{j,d}$ those already given for $\mathbf{R}$. These notations are consistent with the inclusions $\mathbf{P}_{j,d} \subseteq \mathbf{P}_{jd',dd'}$.

Let $\alpha = \sum_{k=j}^{\infty} a_{k/d} \varepsilon^{k/d} \in \mathbf{P}_{j,d} \subseteq \mathbf{P}_{0,d}[1/\varepsilon] (j, d \in \mathbb{Z}, d \ge 1)$. We define:

$$ \bullet \ c_{\ell/d}(\alpha) = \begin{cases} 0 & \text{if } \ell < j, \\ a_{\ell/d} & \text{if } \ell \ge j. \end{cases} $$

• $\kappa_{\ell/d}(\alpha) = s_{\ell/d} \in \{-1, 0, 1\}$ is defined by recurrence as follows:

$$ s_{\ell/d} = \begin{cases} \ell < j, & \text{if } \ell < j, \text{ then } 0 \\ \ell \ge j, & \text{if } \ell \ge j, \begin{cases} s_{(\ell-1)/d} \ne 0, & \text{alors } s_{(\ell-1)/d}, \\ s_{(\ell-1)/d} = 0, & \text{then sign of } a_{\ell/d}. \end{cases} \end{cases} $$

• $\alpha > 0$ means $\exists \ell \ge j \ \kappa_{\ell/d}(\alpha) = 1$.

• $\alpha \ge 0$ means $\forall \ell \ge j \ \kappa_{\ell/d}(\alpha) \ge 0$.

• $v(\alpha) > k/d$ means $\kappa_{k/d}(\alpha) = 0$.

• $v(\alpha) \le k/d$ means $\kappa_{k/d}(\alpha) = \pm 1$.

• $v(\alpha) \ge k/d$ means $\kappa_{(k-1)/d}(\alpha) = 0$.

• $v(\alpha) = k/d$ means $v(\alpha) \ge k/d$ and $v(\alpha) \le k/d$.

From the previous study in Section C.4 which led to Proposition C.4.1 for the ring $\mathbb{Z}$ and to Theorem C.4.2 for the ring $\mathbb{Q}$, we deduce analogous results for the rings $\mathbf{P}_{0,d}$ then for $\mathbf{P}_0$, then for $\mathbf{P}$.

**Proposition E.5.1.**

1. The ring $\mathbf{P}_0$ is a reduced strict $f$-ring which satisfies the following properties.

• It satisfies the rules **OTF**, **OTF**$^×$, **FRAC** and **Val2**. In particular (Lemma D.4.7) the continuous semialgebraic map $\mathrm{Fr}$ satisfying the rules **Fr1** and **Fr2** is well-defined and the corresponding function symbol can be considered as part of the signature.

• This is a residually discrete henselian local ring.

• Its residual field is isomorphic to $\mathbb{R}_{\mathrm{alg}}$. We have $\mathbf{P}_0^\times = \{ \xi \in \mathbf{P}_0 | \kappa_0(\xi) = \pm 1 \}$ and $\mathrm{Rad}(\mathbf{P}_0) = \{ \xi \in \mathbf{P}_0 | \kappa_0(\xi) = 0 \}$.

• The valuation group is isomorphic to $(\mathbb{Q}, +, \ge)$ (the class of $\varepsilon$ corresponds to the element 1 of $\mathbb{Q}$).

• The elements $\ge 0$ are squares: the ring $\mathbf{P}_0$ is a 2-closed $f$-ring (theory *Asr2c*).

• More generally, the elements $\ge 0$ are powers $k$-th of elements $\ge 0$. Since we are dealing with unique existence, we can introduce the corresponding function symbols in the signature.

• Furthermore, the ordered Heyting axiom $\neg(\xi > 0) \Rightarrow \xi \le 0$ is satisfied.

2. The ring $\mathbf{P}$ is a reduced strict $f$-ring which satisfies the following properties.

• An element is $> 0$ if, and only if, it is $\ge 0$ and invertible.

• The rules **OTF**, **OTF**$^×$, **FRAC** and **IV** (a fortiori **Val2**) are satisfied. In particular (Lemma D.4.7) the continuous semialgebraic map $\mathrm{Fr}$ satisfying the rules **Fr1** and **Fr2** is well-defined.

• It is a local ring with $\mathrm{Rad}(\mathbf{P}) = 0$ (a Heyting field in the terminology of [CACM] or [MRR]).

• The elements $\ge 0$ are squares of elements $\ge 0$: the ring $\mathbf{P}$ is a 2-closed strict $f$-ring (theory *Asr2c*).
* More generally, the elements $\ge 0$ are powers $k$-th of elements $\ge 0$. Since we are dealing with unique existence, we can introduce the corresponding function symbols in the signature.

* The ordered Heyting axiom $\neg (\xi > 0) \Rightarrow \xi \le 0$ is satisfied.

**Proof.** Only the fact that the elements $\ge 0$ are powers $k$-th of elements $\ge 0$ is a really new point which requires a proof. This is left to the reader. □

We denote $\mathbf{P}_{alg}$ the integral closure of $\mathbb{R}_{alg}(\varepsilon)$ in $\mathbf{P}$: this is the ring of Puiseux series which are integral over the discrete ordered subfield $\mathbb{Q}(\varepsilon)$.

In the following we will use the notion of extension by continuity. To talk about extension by continuity, we need to define the notion of a convergent sequence, and check that the usual rules for boundary crossing work for this notion.

**Definition E.5.2** (convergent sequences in $\mathbf{P}$). We will say that the sequence $(\alpha_n)_{n \in \mathbb{N}}$ converges towards $\alpha$ in $\mathbf{P}$ if there exist $j$ and $d \in \mathbb{Z}$ with $d \ge 1$ such that

* $\alpha$ and the $\alpha_n$ are all in $\mathbf{P}_{j,d}$,

* $\lim_n v(\alpha_n - \alpha) = \lim_{k \to \infty} j_k \in \mathbb{N}$, $\lim_{k \to \infty} j_k \ge N \forall \ell \in [j..k] c_{\ell/d}(\alpha_m) = c_{\ell/d}(\alpha)$.

We will then write $\alpha = \lim_n \alpha_n$.

We can easily establish the following properties.

**Proposition E.5.3.**

1. $\lim_n \alpha_n = 0$ if, and only if, $\lim_n v(\alpha_n) = +\infty$.

2. If $\lim_n \alpha_n = \alpha$ then $\alpha$ is invertible if, and only if, $\exists N \forall n > N \ v(\alpha_n) = v(\alpha_N) < \text{infty}$. In this case $\alpha^{-1} = \lim_{n \ge N} \alpha_n^{-1}$.

3. If $\alpha = \lim_n \alpha_n$, $\beta = \lim_n \beta_n$ and $a \in \mathbb{R}_{alg}$, then

* $a\alpha = \lim_n a\alpha_n$,

* $\alpha + \beta = \lim_n (\alpha_n + \beta_n)$,

* $\alpha\beta = \lim_n (\alpha_n\beta_n)$,

* $\alpha \mathbf{v} \beta = \lim_n (\alpha_n \mathbf{v} \beta_n)$,

* $\text{Fr}(\alpha, \beta) = \lim_n \text{Fr}(\alpha_n, \beta_n)$ and

* $(\alpha^+)^q = \lim_n (\alpha_n^+)^q \quad (q \in \mathbb{Q}, q > 0)$.

4. All $\alpha \in \mathbf{P}_{j,d}$ is the limit of the sequence of Laurent polynomials $\pi_m(\varepsilon^{1/d})$ for $m \ge j$ obtained by truncation of the series $\alpha$, defined precisely by

$$ \pi_m \in \mathbb{R}_{alg}[\varepsilon^{1/d}][1/\varepsilon], \pi_m = \sum_{k:j \le k < m} c_{k/d}(\alpha)\varepsilon^{k/d} $$

We also note that $\mathbb{R}_{alg}[\varepsilon^{1/d}][1/\varepsilon] \subseteq \mathbf{P}_{alg}$.

We will now prove the following theorem.

**Theorem E.5.4.** The ring $\mathbf{P} = \mathbf{P}_0[1/\varepsilon]$ satisfies all the axioms of the theory *Crc2*. It is therefore a discrete Heyting non-archimedean real closed field.

*First proof.* We are going to generalise the passage to the limit properties described in Proposition E.5.3 to all continuous semialgebraic maps defined on $\mathbb{R}_{alg}$.

The paper [52] shows that $\mathbf{P}_{alg}$ is a discrete real closed field. It is therefore a real closure of $\mathbb{R}_{alg}(\varepsilon)$, constructed in a very different way from that proposed in [42]. Now consider a cube $[-a, a]^r = K \subseteq \mathbb{R}_{alg}^r$ and a continuous semialgebraic map $f: K \to \mathbb{R}_{alg}$. Since $\mathbf{P}_{alg}$ is a discrete
real closed field, $f$ extends uniquely into a continuous semialgebraic map $f_1: K_1 \to \mathbf{P}_{alg}$, where $K_1 \subseteq \mathbf{P}_{alg}^r$ is defined by the same system of inequalities as $K$. We will show that $f_1$ extends by continuity into a map $f_2: K_2 \to \mathbf{P}$, where $K_2 \subseteq \mathbf{P}^r$ is defined by the same system of inequalities as $K$. This will suffice to show that $\mathbf{P}$ is a model of *Crc1*.<fnref n="2" />

**Proposition and definition E.5.5.** We apply the previous notations for $K \subseteq K_1 \subseteq K_2$. Let $f: K \to \mathbb{R}_{alg}$ be a continuous semialgebraic map and $f_1: K_1 \to \mathbf{P}_{alg}$ be its extension to $\mathbf{P}_{alg}$. Then for any sequence $(\alpha_n)$ in $\mathbb{R}_{alg}[\varepsilon, \varepsilon^{-1}]^r \cap K_2$ which converges to a $\alpha \in \mathbf{P}$, the sequence $f_1(\alpha_n)$ converges in $\mathbf{P}$. The limit depends only on $\alpha$ and is denoted $f_2(\alpha)$.

*Proof.* Not so simple! First we have to see that the $f_1(\alpha_n)$'s belong to a given $\mathbf{P}_{j,D}$; next a Łojasievicz inequality could be used for the convergence. □

<figure><img src="image_15.png" /></figure>

*Second proof.* Given Proposition E.5.1 it suffices to prove the existence property of virtual roots for the ring $\mathbf{P}$. To do this we need only prove an analogue of Lemma E.2.3 for $\mathbf{P}_0$. In the recursive definition of virtual roots, not only is the polynomial assumed to be strictly monotone over the interval, but its derivative has a known strict sign over the entire open interval. We state the desired property in the following form (we restrict ourselves to the Item 1 of Lemma E.2.3 without loss of generality).

**Lemma E.5.6.** Let $s = \pm 1$. Consider a monic polynomial $f \in \mathbf{P}_0[X]$ and $\alpha \le \beta$ elements of $\mathbf{P}_0$. The following property is assumed to be satisfied: if $\alpha < \zeta < \beta$, then $sf'(\zeta) > 0$. Then the polynomial $f$ reaches its absolute minimum on $[\alpha, \beta]$ in a single $\xi \in \mathbf{P}_0$.

We have $(\xi - \alpha)(\xi - \beta)f(\xi) = 0$, and $\xi$ is the only element of $\mathbf{P}_0$ satisfying the following system of inequalities:

(1) $\alpha \le \xi \le \beta$

(2) $s(\xi - \alpha)f(\alpha) \le 0$

(3) $s(\beta - \xi)f(\beta) \ge 0$

We note $R(\alpha, \beta, f)$ this element $\xi$.

A monic polynomial $f$ of degree $n$ is given by its $n$ coefficients in degrees $< n$, and the map

$$ \mathbb{R}_{alg}^{n+2} \to \mathbb{R}_{alg}, (\alpha, \beta, f) \mapsto R(\alpha, \sup(\alpha, \beta), f) $$

is a continuous semialgebraic map defined on $\mathbb{R}_{alg}$. The aim here is to see that it extends to $\mathbf{P}_0$. We already know that such an extension is unique when it exists (Lemma E.2.10).

*Proof.* We need only deal with the case where $\alpha, \beta$ and the coefficients of $f$ are in $\mathbb{R}_{alg}[\varepsilon]$. It is also assumed without loss of generality that $\alpha = 0$ and $s = 1$. The desired inequalities then become

(1) $0 \le \xi \le \beta$

(2) $\xi f(0) \le 0$

(3) $(\beta - \xi)f(\beta) \ge 0$

(4) $\xi f(\xi) \le 0$

(5) $(\beta - \xi)f(\xi) \ge 0$

If $0 < xi < \beta$ the inequalities (4) and (5) force $f(\xi) = 0$. Furthermore, since $f' > 0$ on the open interval, we also have $f(0) < f(\xi) < f(\beta)$.

The difficult case to deal with is where $f(0) < 0 < f(\beta)$. □

<figure><img src="image_16.png" /></figure>

<figure><img src="image_17.png" /></figure>

<footnote n="2">²The details of this statement are left to the reader.</footnote>
## E.6. Use of virtual roots in constructive real algebra

The results stated in this subsection for the real number field also seem valid in the dynamical theory *Corv*. Some may require only *Co0rv* or *Arc*.

### Basic semialgebraic subsets of the real line

Let us define a *basic semialgebraic closed subset* of the real line as a subset of the form $F_f = \{x \in \mathbb{R} | f(x) \ge 0\}$ for an $f \in \mathbb{R}[X]$.

*First example.* Consider the polynomials $f(X) = X^2 - b$ and $g = -f$.

* If $b < 0$, we have $F_f = \mathbb{R}$ and $F_g = \emptyset$.

* If $b > 0$, we have $F_f = [-\infty, -\sqrt{b}] \cup [\sqrt{b}, +\infty[$ and $F_g = [-\sqrt{b}, \sqrt{b}]$.

* If $b = 0$, we have $F_f = \mathbb{R}$ and $F_g = \{0\}$.

To obtain such a precise description of these semialgebraic closures it is absolutely necessary to
know the sign of $b = -f(0)$.

If we denote $\alpha$ and $\beta$ the virtual roots of $f$, we have the following alternative description.

* If $\alpha < \beta$, i.e. if $f(\frac{\alpha+\beta}{2}) > 0$ we have $F_f = [-\infty, \alpha] \cup [\beta, +\infty[$ and $F_g = [\alpha, \beta]$.

* If $\alpha = \beta$ and $f(\alpha) < 0$, i.e. if $f(\frac{\alpha+\beta}{2}) < 0$, we have $F_f = \mathbb{R}$ and $F_g = \emptyset$.

* If $\alpha = \beta$ and $f(\alpha) = 0$, that is if $f(\frac{\alpha+\beta}{2}) = 0$, we have $F_f = \mathbb{R}$ and $F_g = \{\alpha\}$.

*Second example.*

The case of a monic polynomial $f$ of degree $\delta > 2$. Let us denote $\mathrm{Vr}_f$ the list of its virtual roots.
Theorem E.2.6 allows us to describe the adherence of $F_f \cup \mathrm{Vr}_f$ exactly as the adherence of the
union of the following intervals

* $(-\infty, \rho_{\delta,1}]$ if $\delta \equiv 0 \mod 2$

* $[\rho_{\delta,k}, \rho_{\delta,k+1}]$ for $k \in [0..\delta - 2]$, $k \equiv \delta \mod 2$

* $[\rho_{\delta,\delta}, +\infty)$

In imprecise imagery: “we know $F_f$ to the nearest $\mathrm{Vr}_f$”.

Generally speaking, the problem with a polynomial of known degree arises from the fact that Theorem E.2.6 asserts something precise about the sign of the polynomial on an interval $[\rho_{\delta,j}, \rho_{\delta,j+1}]$ only when $\rho_{\delta,j} < \rho_{\delta,j+1}$. The result is as follows.

**Lemma E.6.1.** Let $f \in \mathbb{R}[X]$ be a polynomial of degree $\delta$ known and $g = f/c_\delta$ the corresponding monic polynomial ($c_\delta$ is the leading coefficient, $> 0$ or $< 0$). Let us note $\rho_{\delta,k} = \rho_{\delta,k}(g)$.

1. The adherence of $F_f \cup \mathrm{Vr}_f$ is equal to the adherence of an explicit finite union of closed intervals whose bounds are $\rho_{\delta,k}$ or $+\infty$, or $-\infty$.

2. When we know the signs of $(\rho_{\delta,k+1} - \rho_{\delta,k})$ and $g(\rho_{\delta,k})$, we have an exact description of the closed $F_f$ in the form of a finite union of disjoint closed intervals. The information required is equivalent to giving the signs of $g(\frac{\rho_{\delta,k}+\rho_{\delta,k+1}}{2})$.

When the degree of $f$ is not known, we lose control of the situation in $+\infty$ and $-\infty$. The fuzziest situation, in which we have no control at all, arises when we don't know whether the polynomial is identically zero or not.

Similar results hold for a basic open $U_f = \{x \in \mathbb{R} | f(x) > 0\}$.
**Sign and variation tables**

Let $\mathbf{R}$ be a constructive model of $\mathcal{Co}_0$. Two elements $a$ and $b$ are said to be “distinct” if $a \# b$, i.e. $a - b$ is invertible.

**Lemma E.6.2.** Given a list $L$ of $k$ elements and a list $L'$ of $k + \ell$ distinct elements in $\mathbf{R}$, at least $\ell$ elements of $L'$ are distinct from all elements of $L$.

Theorem E.2.6, Items 3d and 3e, almost gives a complete table of signs and variations for the monic polynomial $f$.

For the complete table of signs of $f$, any hesitations concern the signs of $f$ in the virtual roots $\xi_k$ of $f'$. The same applies to the table of variations of $f$, with the signs of $f'$ at the virtual roots of $f''$.

This leads to the following result.

**Proposition E.6.3.** Let $\mathbf{R}$ be an ordered field with virtual roots.

1. Let $f(x) \in \mathbf{R}[x]$ be a monic polynomial of degree $k \ge 2$ and $k + \ell - 1$ distinct elements $a_i \in \mathbf{R}$. For at least $\ell$ of these elements, the polynomial $f(x) + a_i$ has a known strict sign at each of the virtual roots of $f'$, and its complete sign table is known exactly. If $k = 2$ then the complete table of signs and variations is known exactly.

2. Let $f(x) \in \mathbf{R}[x]$ be a monic polynomial of degree $k \ge 3$, $k + \ell - 1$ distinct elements $a_i \in \mathbf{R}$, and $k + \ell - 2$ distinct elements $b_j \in \mathbf{R}$. For at least $\ell^2$ of the pairs $(a_i, b_j)$, we have a complete table of signs and variations known exactly for the polynomial $f(x) + b_jx + a_i$.

*Remarks E.6.4.*

1) We probably have a perturbation result of the same style which says that for almost all perturbations of a finite number of monic polynomials $f_i$, we know with certainty the strict equalities and inequalities between all the virtual roots of $f_i$ and all their derivatives, as well as the signs of $f_i$ in each of these virtual roots, which gives a complete table of signs and variations for the family of $f_i$ and their derivatives.

2) If we want a result analogous to Proposition E.6.3 for a continuous semialgebraic map, we will have to place ourselves in the theory *Corv* and restrict the table of signs and variations sought to a bounded closed interval. ■

**An approximate cylindrical algebraic decomposition (CAD)?**

The problem arises of giving an approximate CAD for a finite family of polynomials of $\mathbf{R}[X_1, \dots, X_n]$ where $\mathbf{R}$ is a constructive model of $\mathcal{Co}_0\nu$ (or of $\mathcal{Corv}$). This would be a result that cleverly generalises Lemma E.6.1 or Proposition E.6.3.

In piano-mover terms, instead of deciding whether “this passes” or “that doesn’t pass”, we’d get approximate results of the following kind: given the data of the problem and a desired precision $\epsilon$, we’d compute uniformly a $\alpha \in \mathbf{R}$ such that:

* if $\alpha > 0$, there is a way of passing at a distance $> \epsilon$ from the obstacles, and we’ll tell you how,

* si $\alpha < 1$ il n'y a pas moyen de passer en respecter un distance $> 2\epsilon$.

Naturally, the piano must be a well-defined semialgebraic compact, as must the obstacles, and as must the space in which the piano is moved.

In general, since it is impossible to control, even in an approximate way, the behaviour at infinity of a polynomial whose coefficients are all close to 0, we must necessarily limit ourselves to calculating an approximate CAD for a finite family of polynomials on a well-defined compact of the style $[0, 1]^n$. If we try to reproduce a usual CAD (for a discrete real closed field) on $\mathbb{R}$, we can see that the coefficients of a sub resultant polynomial may well all be very close to 0. But a *priori* virtual roots are only effective for monic polynomials.

On this kind of subject, we’re still in our infancy.
# Stratifications

It seems that stratifications, when assumed, are a restful framework in which many results valid for discrete real closed fields can be extended without too much difficulty to the non discrete case.

# The Fundamental Theorem of Algebra (FTA)

For a treatment of FTA without the axiom of dependent choice, see [58].

Since the virtual roots are continuous maps, and since it is impossible to follow by continuity the zeros of a complex polynomial (monic of fixed degree $m$ and with variable coefficients), we certainly cannot obtain one of these zeros expressed as an element of $\text{Fsace}_m(\mathbb{R})$. Nevertheless, we can cover the zeros of a complex polynomial of degree $\delta$ by a finite number of expressions in $\text{Fsace}_{\delta^2}(\mathbb{R})$.

What we'd like to do here is to do it in a fairly optimal way.

## 1. The square roots of a complex number $c = a + ib$.

The zeros of the polynomial $f(Z) = Z^2 - c$ are given in the form $x + iy$ by the real solutions of the system "$x^2 - y^2 = a$, $2xy = b$" and are calculated as follows:

$$ \bullet \quad (x^2 + y^2)^2 = a^2 + b^2, \text{ so } x = \pm u \text{ with } u = \sqrt{\frac{1}{2}(a + \sqrt{a^2 + b^2})} \in \text{Fsace}_4(\mathbb{R}) $$

$$ \bullet \quad y = \pm v \text{ with } v = \sqrt{\frac{1}{2}(-a + \sqrt{a^2 + b^2})}, \text{ with the constraint } xyb \ge 0. $$

If we denote $z_1 = u + iv$, $z_2 = -z_1$, $f_1(Z) = (Z - z_1)(Z - \bar{z_1})$, $f_2(Z) = (Z - z_2)(Z - \bar{z_2})$ and $g(Z) = (Z - c)(Z - \bar{c})$ we obtain the equality

$$ g(Z^2) = f(Z)\bar{f}(Z) = f_1(Z)f_2(Z) \qquad (E.2) $$

The polynomials $f_1, f_2, g$ and $\bar{f}\bar{f}$ are real, everywhere $\ge 0$, each with a simple algebraic certificate for its character $\ge 0$ when the variable is real. When $c \ne 0$, the zeros of $f$ are divided between the zeros of $f_1$ and those of $f_2$.

We can estimate that we have thus obtained the optimal solution for the square roots of a complex number in the context of the $\mathbb{R}$-algebra of maps generated by the maps "virtual square roots" $\rho_{2,2}$, and more generally the optimal solution in the context of the algebras $\text{Fsace}_m(\mathbb{R})$.

Note that $x$ and $y$ being roots of real polynomials of degree 4, there were 16 possible choices for $x + iy$.

## 2. The general case.

We have the following non-optimal result.

**Proposition E.6.5 (FTA) via the virtual roots).**

Let $f$ be a complex monic polynomial of degree $\delta$. There exist $\delta^4$ polynomials $q_\ell$ positive quadratic$^3$ having their coefficients constructed over $\rho_{\delta^2,k}(\dots)$ (polyroots in the real and imaginary parts of the coefficients of $f$) such that $\overline{f}\overline{f}$ divides the product of $q_\ell$.

If the real closed field under consideration is discrete, the polynomial $f(z)$ decomposes into a product of $(z - \zeta_j)$ factors explicit on $\mathbb{C}$, with the $\zeta_j$ whose real and imaginary parts are roots of monic real polynomials of degree $\delta^2$, whose coefficients are $\mathbb{Q}$-polynomials in the real and imaginary parts of the coefficients of $f$.

*Proof.* The real part of a zero $\zeta_j$ of $f$ is written $(\zeta_j + \overline{\zeta_j})/2$. The $(\zeta_j + \overline{\zeta_k})/2$ are $\delta^2$ and are the zeros of a real polynomial $h_1$ of degree $\delta^2$ whose coefficients are expressed as $\mathbb{Q}$-polynomials in the real and imaginary parts of the coefficients of $f$. Among the real zeros of $h_1$ are the $\frac{1}{2}(\zeta_j + \overline{\zeta_j})$. These are therefore virtual roots of $h_1$. Similar reasoning applies to the imaginary part, with a real polynomial $h_2$ of degree $\delta^2$. If $\alpha$ is a virtual root of $h_1$ and $\beta$ a virtual root of $h_2$, we associate the polynomial

$$ q = (z - \alpha + i\beta)(z - \alpha + i\beta) = (z - \alpha)^2 + \beta^2 $$

which is one of the $q_\ell$ in the statement.

□

<footnote>$^3$Precisely: monic polynomials of degree 2 everywhere $\ge 0$.</footnote>
Remark E.6.6. In the paper [54] the authors prove that a discrete ordered field $\delta^2$-closed (i.e. satisfying the intermediate value theorem for polynomials of degree $\le \delta^2$) satisfies the fundamental theorem of algebra for polynomials of degree $\le \delta$. We can deduce this result from Proposition E.6.5 using the formal Positivstellensatz as follows. Assume that the real closed field is discrete. Then the fact that $f\bar{f}$ divides the product of $q_\ell$ implies that $f$ admits at least one complex zero, among the zeros of $q_\ell$.<fnref n="4" /> Moreover, the virtual roots of $h_1$ and $h_2$ are characterised by systems of large inequalities. A Horn rule on the language of ordered fields states that, for a discrete real closed field, if we put these systems of large inequalities into hypotheses, we obtain as a valid consequence the fact that the product of $f(\alpha \pm i\beta)$ suitable is zero. According to Item 2 of the formal Positivstellensatz C.2.1, this Horn rule is valid for any ordered field (discrete or not) as well as for real closed rings, since it is valid in the theory *Asonz*. And if the field satisfies the **TVI** for polynomials of degree $\le \delta^2$, the hypotheses are satisfied by the virtual roots of $h_1$ and $h_2$. In the same way, if the language of ordered fields has been enriched by introducing virtual root maps for polynomials of degree $\le \delta^2$, with the corresponding axioms, we will also obtain for the corresponding dynamic algebraic structures the fact that the product of $f(\alpha \pm i\beta)$ suitable is zero.■

• 3. The general case in terms of multisets. Reference: the **FTA** in [58, Richman].
A priori, the “FTA version multisets” seems difficult to formulate correctly without having the metric space of *n*-multisets of complex numbers.

To get around this, we can reduce the “**FTA** version multisets” to a set of dynamically valid rules giving an essentially equivalent formulation that uses counting the number of zeros inside rectangles in the style of [24, Eisermann]. The article [54] seems to us to give all the necessary details.

Since we do not assume that the ordered field is discrete, we must use only rectangles on whose edges we are certain that there are no complex zeros of the polynomial under consideration.

An explicit test shows that we must avoid at most $\delta$ horizontal lines and at most $\delta$ vertical lines for our rectangles. This is formulated by saying that if we consider $\delta + m$ distinct horizontal lines, we are certain that at least $m$ of them are good (the same goes for the verticals).

For these rectangles, counting the zeros inside works and always gives a well-defined integer.

We have a valid rule which ensures that no complex zero lies outside an explicitly large enough rectangle. For this sufficiently large rectangle the count gives the expected number $\delta$. And a valid rule says that when a rectangle is cut in half, the sum of the two counts equals the previous count.

If we also want to deal with the non-archimedean case, we need to establish Horn rules saying that we can enclose the $\delta$ zeros in a union of rectangles of arbitrarily small size.

Further study of the paper [54] should lead to the desired results, which are more precise than the **FTA** considered in Item 2, results which can be considered to be the satisfactory constructive form of **FTA**, and which will be valid for *Corv* theory, formulable as valid Horn rules in that theory. But these Horn rules would not be valid in the theory of real closed rings.

# E.7. Some questions

## Continuous semialgebraic maps

**Question E.7.1.** Make more explicit the (constructive) result of continuity of virtual root maps: Item 2 of Theorem E.2.6. Each map $\rho_{d,j}: \mathbf{R}^d \to \mathbf{R}$ is uniformly continuous on any ball $B_{d,M} := \{(a_{d-1}, \dots, a_0) \mid \sum_i a_i^2 \le M\}$, ($M > 0$). Continuity should be given in fully explicit form à la Łojasiewicz.

**Question E.7.2.** Give a constructive proof of Theorem E.3.16.

**Question E.7.3.** Let $\mathbf{R}$ be a real closed ring. Is any element of $\mathrm{Fsac}_n(\mathbf{R})$ an integer on the ring of polynomials $\mathbf{R}[x_1, \dots, x_n]$ an element of $\mathrm{Fsace}_n(\mathbf{R})$ ?

<footnote n="4">⁴We have a little better. The product of $q_\ell$ decomposes into a product of linear, and therefore irreducible, factors in $\mathbb{C}[Z]$. Since $f(Z)$ divides this product, and since $\mathbb{C}[Z]$ is a gcd domain, it is in fact a by-product.</footnote>
**Question E.7.4.** Is every continuous map $\mathbb{R}^m \to \mathbb{R}$ which is integral on the ring of polynomials an element of $\text{Fsace}_m(\mathbb{R})$ ? The answer in classical mathematics is yes, because we can apply Theorem E.2.8 to $\mathbb{R}$.

Questions E.7.5 have to do with the o-minimal character of the *non* discrete real closed field structure. The word “compact” below is used to mean “closed bounded subset”.

**Questions E.7.5.** (remember Proposition E.3.5)

Consider an ordered field with virtual roots $\mathbf{R}$.

1. Show that a continuous semialgebraic map which is everywhere $> 0$ on the compact $[0, 1]^n \subseteq \mathbb{R}^n$ is minorized (on this compact) by an element $> 0$. And that the lower bound is an element of $\mathbf{R}$.

2. Extend the result to an arbitrary “well-defined” semialgebraic compact: by this we mean a bounded semialgebraic closure $K$ for which the function “distance to $K$” is a continuous semialgebraic map (an element of $\text{Fsac}_n(\mathbf{R})$).

## Real closure

**Question E.7.6.** If $\mathbf{K}$ is a model of $\mathcal{Co}$ (or of $\mathcal{Co0}$), is its 2-closure $\mathbf{L}$ as an $f$-ring still a model of $\mathcal{Co}$ (or of $\mathcal{Co0}$)?

We repeat the previous question (adding some details) for the real closure.

**Question E.7.7.** Let $\mathbf{K}$ be a model of the theory $\mathcal{Co}$ and $\mathbf{R}$ be the dynamic algebraic structure $\text{Corv}(\mathbf{K})$ (as page ??). Is $\mathbf{R}$ a constructive model of $\text{Corv}$?

In particular, is the following metatheorem satisfied? Given two closed terms $\alpha$ and $\beta$ of $\mathbf{R}$ such that the rule $\vdash \alpha + \beta > 0$ is valid, is it true that one of the two rules $\vdash \alpha > 0$, $\vdash \beta > 0$ is valid?

We can ask the same question in the following form: if $\mathbf{K}$ is a model of $\mathcal{Co}$, does the (usual) algebraic structure $\text{ARC}(\mathbf{K})$ satisfy the rule **AFRL**?

**Question E.7.8.** Can the article [24, Eisermann] be reread for a *non* discrete real closed field, i.e. in the theory *Crc2*? This question requires a detailed development of the ideas in Item 3, page 107 in the paragraph concerning **FTA**.

**Question E.7.9.** Show that the intermediate value theorem, stated in the form of the rule $\text{RCF}_n$ page 45, is not valid in the theory *Crc2*. Note that a slightly weakened form is valid: see Item 4 of the formal Positivtellensatz E.3.7 and Item 3i of Theorem E.2.6.

**Question E.7.10.** Show that the theorem which states that every complex number has a square root is not a valid rule in the theory *CRC2*. Compare with Proposition E.6.5 which might seem to assert the opposite.

## Pierce-Birkhoff

**Questions E.7.11.**

1) Does the definition of a Pierce-Birkhoff ring given in E.2.16 coincide in classical mathematics with the notion defined in [49, Madden, 1989]?

2) If this is indeed the case, the question arises of giving constructive proofs for sophisticated results, such as the fact that a regular Noetherian coherent ring of dimension $\le 2$ is a Pierce-Birkhoff ring [48].

3) Recall that the usual Pierce-Birkhoff conjecture is proved in [51] for $\mathbf{R}[x, y]$ when $\mathbf{R}$ is a discrete real closed field but it is not so clear that there is a constructive proof for $\mathbb{R}[x, y]$.
## The 17th Hilbert problem

**Question E.7.12.** To what extent does the constructive solution of the 17th Hilbert problem for $\mathbb{R}$ (see [26, section 6.1]) apply to any strict $f$-ring with virtual roots? If not, what stronger theory would do: *Crc2*, *Arc*, *Crca*, *Icrc* (page ??)?

## The Grail?

The question arises of a theorem analogous to Theorem C.2.5, but now for the non-discrete case.

The formal Positivstellensatz E.3.7 implies that the theory *Arc* is the Horn theory generated by $\mathbb{R}_{\text{alg}}$, by $\mathbb{R}$ or by $\mathbb{R}_{\text{PR}}$ on the signature of *Arc*.

**Question E.7.13.** Is the theory *Arc* skolemised from the cartesian theory generated by $\mathbb{R}_{\text{alg}}$, by $\mathbb{R}$ or by $\mathbb{R}_{\text{PR}}$ on the signature of commutative rings?

**Question E.7.14.** In what sense could we say that the theory *Corv* is the dynamical theory generated by $\mathbb{R}$ “without axiom of dependent choice” on the signature of *Arc*? Same question with $\mathbb{R}_{\text{PR}}$.

NB: this question seems impossible to formulate in classical mathematics, and in constructive mathematics, we would need to have a clear idea of $\mathbb{R}$ “without an axiom of dependent choice”.
<figure><img src="image_18.png" /></figure>
# F. The axiom of archimedianity

## Sommaire

<table><tr><td>F.1</td><td>Archimedean non discrete real closed fields</td><td>111</td></tr><tr><td>F.2</td><td>Some questions</td><td>111</td></tr><tr><td></td><td>Axiom of archimedianity</td><td>111</td></tr><tr><td></td><td>The principle of omniscience LPO is safe in real algebra?</td><td>112</td></tr><tr><td></td><td>Convergent series in real algebra?</td><td>112</td></tr><tr><td></td><td>Schmüdgen's Positivstellensatz</td><td>112</td></tr></table>

In this chapter, in order to better describe the algebraic properties of $\mathbb{R}$, we make an attempt which consists in not leaving the dynamical theories while preserving the essence of the non-dynamical rule **HOF**.

However, the language remains essentially that of ordered rings.

In the third part, we will make a much more ambitious attempt using a much richer language, which will essentially show us a geometric theory of the reals as a precursor of the theory of o-minimal structures.

## F.1. Archimedean non discrete real closed fields

The following rule, which means that the field is archimedean, is satisfied on $\mathbb{R}$

$$ \textcolor{red}{\mathbf{AR1}} \vdash \textcolor{blue}{\mathbf{OP}}_{n \in \mathbb{N}} |x| \le n \qquad (\text{Archimedes 1}) $$

**Definition F.1.1.** We define the theory *Crc* of real closed archimedean fields as the geometric theory obtained by adding the axiom **AR1** to the theory *CRC*.

The example given in Item 3 of Remark E.4.4 (a local real closed ring with zerodivisors, model of the theory *CRC*2) remains a model of *CRC*. Examples C.3.4 are also models of the theory *CRC*: in general the subrings of $\mathbb{R}$ stable for virtual root maps, the fraction Fr and the inverses of invertible elements, are models of *CRC*.

## F.2. Some questions

### Axiom of archimedianity

#### Questions F.2.1.

We know that we cannot express the fact that $\mathbb{R}$ is archimedean in a finitary way. We express it with the infinite rule **AR1**.

* One question that arises is whether the theory *CRC* obtained by adding the rule **AR1** is a conservative extension of *CRC*2, this seems likely.
* We could start by showing that *Crca* proves the same Horn rules as *Crc2*.

* On the other hand, for the corresponding formal theory in which we allow the introduction of predicates for $P \Rightarrow Q$ and $\forall x P$ (with Gentzen's natural deduction rules) it could be that a statement like **HOF** becomes provable.

* The principle of omniscience LPO is safe in real algebra?

**Question F.2.2.**

The following rule is not satisfied on $\mathbb{R}$, because it implies the **ED#** rule.

$$ \textcolor{red}{\mathbf{AR2}} \vdash x = 0 \ \mathbf{op} \ \mathbf{OP}_{n \in \mathbb{N}} |x| > 1/2^n \quad (\mathbf{Archimedes 2}) $$

But no doubt it is “admissible”, in the sense that adding it to *Crca* would provide a conservative extension of *Crcd*.

This result would be a kind of realisation of Hilbert's programme for LPO, restricted to the theory *Crca*. Indeed, the theory *Crcd* is itself harmless compared to *Crc2* because it proves the same Horn rules.

* Convergent series in real algebra?

**Question F.2.3.** Let $[x]^n = \frac{1}{2^n} \wedge (x \vee -\frac{1}{2^n})$. The following rule is not a dynamical rule

$$ \mathbf{Cauchy} \vdash \exists x \bigwedge_{n \in \mathbb{N}} |x - \operatorname{sum}_{p=0}^{n} [x_p]^p| \le 1/2^n \quad (\mathbf{Cauchy}) $$

A function symbol $\sum_{n=0}^{\infty} [x_n]^n$ should be introduced for these infinite sums. This would replace the illegitimate rule **Cauchy** by an infinite number of legitimate Horn rules. But is such a function symbol legitimate?

## Schmüdgen's Positivstellensatz

References: [60, 66, 67]

**Question F.2.4.** Is geometric theory sufficient to develop theorems of the Schmüdgen type?
# Conclusion

The most important questions that remain to be resolved for this 2nd part seem to us to be the following.

1. Question C.7.1. Give a constructive proof of Theorem C.5.4.

2. Let $\mathbf{R}$ be a discrete real closed field and $f: \mathbf{R}^n \to \mathbf{R}$ be a continuous semialgebraic map. There exists an integer $r \ge 0$, a continuous semialgebraic map $g: \mathbf{R}^{r+n} \to \mathbf{R}$ defined on $\mathbb{R}_{\text{alg}}$, and an element $\underline{y} \in \mathbf{R}^r$ such that

$$ \forall x_1, \dots, x_n \in \mathbf{R} \ f(x_1, \dots, x_n) = g(y_1, \dots, y_r, x_1, \dots, x_n). $$

3. Question E.7.1. Make explicit Item 2 of Theorem E.2.6 asserting the uniform continuity of maps $\rho_{d,j}: \mathbf{R}^d \to \mathbf{R}$ on any closed ball.

4. Question E.7.2. Give a constructive proof of Theorem E.3.16 Any continuous semialgebraic map $\mathbb{R}_{\text{alg}}^n \to \mathbb{R}_{\text{alg}}$ can be defined by a term of the theory $\mathcal{Arc}$. This will make it possible to clarify definitively the constructive Definition E.3.1 of real closed rings and its relationship in classical mathematics with various constructive characterisations of real closed rings.

5. Question E.7.7 concerning the possibility of constructing a real closure of a non-discrete ordered field. Let $\mathbf{K}$ be a model of the theory $\mathcal{Co}$ and $\mathbf{R}$ the dynamical algebraic structure $\mathcal{Corv}(\mathbf{K})$ (as page ??). Is $\mathbf{R}$ a constructive model of $\mathcal{Corv}$?
# Part III

*An improved version of the theory of *non* discrete real closed fields and an attempt at a constructive version of o-minimal structures*
<figure><img src="image_19.png" /></figure>
# Introduction

In this third part we explore the possibility of better describing the algebraic properties of $\mathbb{R}$ by extending the language through the introduction of sorts for continuous semialgebraic maps on compact cubes.

Indeed, we note that the general situation became clearer when we introduced the maps $\vee$, $\wedge$ and the virtual root maps. These natural extensions to the language used have gone a long way towards overcoming the obstacles that the notion of *non* discrete order seems to offer to a formalisation in finitary dynamical theory.

However, from a constructive point of view, it is not natural to be interested in the real zeros of polynomials whose degree is fixed. The good reason for this with $\mathbb{R}$ is that we don't control the zeros in the neighbourhood of infinity when the degree is not clearly fixed. By replacing $\mathbb{R}$ by the real interval $\mathbb{I}_{\mathbb{R}} = [-1, 1] \subseteq \mathbb{R}$ this so-called good reason disappears by itself.

The idea is that you control things constructively only within the compact framework. We need to detox from $\pm\infty$ and go back to Greek mathematics! Consequently, we must drop $\mathbb{R}$ in favour of the interval $\mathbb{I}_{\mathbb{R}}$, for example by replacing $+$ by the half-sum. This requires us to go back to the axiomatics, but the benefit will be that it will be easier to formulate certain properties linked to the fact that from the constructive point of view $\mathbb{R}$ is not discrete.

Note that up to now, we have been rather dry concerning some of the desirable properties stated in C.5.6: indeed we have not been able to correctly state the principles of extension by continuity or the gluing principles with sufficient generality. We could only talk about uniform continuity from outside the dynamical theory. Indeed, uniform continuity requires an alternation of quantifiers of the type $\forall n \exists m \forall x, y$ which requires a priori to leave the framework of geometric theories. This is also due to the fact that we had no sort of continuous semialgebraic maps.

In this section we try to make up for this lack. And we must remember that from a constructive point of view, a continuous map on a compact does not exist without a uniform continuity modulus. The gamble we take here is to internalise the question of uniform continuity. This means that, for the moment, we remain within a finitary dynamical theory framework.

Moreover, the extended framework that we propose with the introduction of these new sorts seems to be a correct framework for approaching a constructive treatment of o-minimal structures.

Here is a brief description of the contents of the third part.

Chapter G recalls the fascinating properties of o-minimal structures in classical mathematics. These are finiteness properties exactly similar to those of the algebraic geometry of discrete real closed fields, and yet devoid of algorithmic character by the use of the sign test on real numbers in classical theory. Constructing an algorithmic theory of o-minimal structures is a crucial challenge in the “constructive Hilbert programme”, which aims to uncover hidden constructions in contemporary classical mathematics and to reformulate purely ideal theorems into constructive statements. This programme avoids the use of the formal theory *ZFC*, which describes an hypothetical set universe that does not correspond to any proven mathematical construction.

Chapter H proposes a first finitary dynamical theory for sorts describing uniformly continuous real maps with values in $\mathbb{I}_{\mathbb{R}}$.

Chapter J gives a general framework to describe the properties of uniformly continuous maps defined on $\mathbb{I}_{\mathbb{R}}^m$ with values in $\mathbb{I}_{\mathbb{R}}^n$. A decisive aspect is to take into account the fact that a uniform
continuity modulus of a map $f$ can be seen as another uniformly continuous map $g$ attached to the map $f$.

Chapter K proposes new axioms which are a priori satisfied for the algebraic geometry of real closed fields and which seem decisive for approaching an hypothetical and highly desirable constructive theory of o-minimal structures. We are nevertheless very far from having formalised in a dynamical theory what would be a constructive version of o-minimal structures.
# G. O-minimal structures

## Sommaire

<table><tr><td>Definition, definable parts</td><td>119</td></tr><tr><td>Definable maps, outstanding results</td><td>119</td></tr><tr><td>Variant</td><td>120</td></tr></table>

## Definition, definable parts

References: [Coste], [van den Dries, 1998], [70, 21].

The definition of an o-minimal structure over a real closed field $\mathbb{R}$ in classical mathematics is given by a collection $(S_n)_{n \in \mathbb{N}}$, where each $S_n$ is a set of parts of $\mathbb{R}^n$, which verifies the following stability properties.

1. The semi-algebraic subsets of $\mathbb{R}^n$ are in $S_n$.

2. Every $S_n$ is a Boolean algebra of sets (stability by finite intersection and reunion, and complementary passage).

3. If $A \in S_n$ and $B \in S_m$ then $A \times B \in S_{m+n}$.

4. If $A \in S_{n+1}$ and $p_n: \mathbb{R}^{n+1} \to \mathbb{R}^n$ is the projection onto the first subspace $\mathbb{R}^n$ of coordinates (forgetting the last coordinate), then $p_n(A) \in S_n$.

5. The elements of $S_1$ are precisely the finite unions of open intervals and points.

The elements of $S_n$ are called the *definable parts* of the o-minimal structure under consideration.

## Definable maps, outstanding results

A map $A \to B$ between definable sets is said to be *definable* if its graph is definable.

Let's recall some key results.

* The domain of definition and the image set of a definable map are definable.

* The composite of two definable maps is definable.

* Any definable part is a Boolean combination of definable closed parts. More precisely, we have a definable cylindrical decomposition of $\mathbb{R}^n$ adapted to any finite family of definable parts (analogously to the CAD in the case of semi-algebraic parts for a discrete real closed field). The cells of the decomposition are homeomorphic to open simplexes, with definable homeomorphisms.
• If $A \in S_n$ is closed (for the Euclidean distance of $\mathbf{R}^n$) and non-empty, then the function “distance to A”

$$d_A : \mathbf{R}^n \to \mathbf{R}, x \mapsto \inf_{y \in A} \|x - y\|$$

is (continuous and) definable.

• If $f: \mathbf{R}^n \to \mathbf{R}$ is continuous and definable, the zeros of $f$ form a definable closed part. Conversely, according to the previous item, any definable closed part of $\mathbf{R}^n$ is the zero set a definable continuous map.

• If $I = (a, b) \subseteq \mathbf{R}$ (with $a, b \in \mathbf{R}_\infty := \mathbf{R} \cup \{-\infty, +\infty\}$) and if $f: I \to \mathbf{R}$ is a definable map, then

– there is a subdivision of $I$

$$a = a_0 < a_1 < \dots < a_k = b$$

such that on each open interval of the subdivision, $f$ is either constant, or strictly monotone and continuous,

– we also have a subdivision such that on each open interval of the subdivision, $f$ is derivable with definable derivative, continuous and of constant sign ($= 0$ or $> 0$ or $< 0$).

• If $A \in S_n$ is a definable closed subset and $f: A \to \mathbf{R}$ is definable continuous, it can be extended into a definable continuous map on $\mathbf{R}^n$.

• Any definable continuous map $(-1, 1) \to (-1, 1)$ extends by continuity into a definable continuous map $[-1, 1] \to [-1, 1]$.

• Any continuous map $[-1, 1] \to [-1, 1]$ is bounded.

• If $f: [-1, 1]^{n+1} \to \mathbf{R}$ is continuous and definable, the map $g: [-1, 1]^n \to \mathbf{R}$ defined by

$$g(x_1, \dots, x_n) := \sup_{y \in [-1, 1]} f(x_1, \dots, x_n, y)$$

is continuous and definable. Note that in particular if $f$ is everywhere $\le 0$ and if $A$ is the zero set $f$, then $p_n(A)$ is the zero set $g$. If $A$ is a definable closed set $\subseteq [-1, 1]^{n+1}$, we can take for $f$ the map $-d_A: [-1, 1]^{n+1} \to \mathbf{R}$.

Variant

All this implies that we could just as easily define the considered o-minimal structure on $\mathbf{R}$ by giving the following objects.

1. Definable continuous maps $[-1, 1]^n \to [-1, 1]$.

2. The bicontinuous increasing bijection (definable in any o-minimal structure)

$$(-1, 1) \to \mathbf{R}, x \mapsto x/(1 - x^2)$$

and the reciprocal bijection

$$\mathbf{R} \to (-1, 1), x \mapsto (\sqrt{4x^2 + 1} - 1)/2x$$

In fact, using the coding given in Item 2, to get the definable continuous maps $\mathbf{R}^n \to \mathbf{R}$ we just need to know how to describe the definable continuous maps $f: (-1, 1)^n \to (-1, 1)$. To do this, all we need to know is how to describe the continuous definable maps $g: [-1, 1]^n \to [-1, 1]$.

Let us note $\|x\| = \sup_{i \in \{1, \dots, n\}} |x_i|$ for $x = (x_1, \dots, x_n) \in \mathbf{R}^n$.

In the case where the growth to infinity of any definable map $f$ from $\mathbf{R}^n$ to $\mathbf{R}$ is bounded by a polynomial, for such a map $f$, we have a continuous definable map $g: [-1, 1]^n \to [-1, 1]$ written in the form $g(x) = (1 - \|x\|^2)^k f(x)$, and the map $f$ can be encoded by the pair $(g, k)$. The map $g$ tends uniformly towards 0 when $x$ tends towards the edge of $[-1, 1]^n$.

In the general case, we can replace $h(x) := 1 - \|x\|^2$ in $g(x)$ by a map $\varphi \circ h$ where $\varphi: [0, 1] \to [0, 1]$ is continuous definable and strictly positive on $[0, 1)$.
# H. Rings of bounded real maps

## Sommaire

<table><tr><td>H.1 Some reminders of the second part</td><td>121</td></tr><tr><td>H.2 Dynamical theory of rings of bounded real maps</td><td>121</td></tr><tr><td>H.3 Dynamical theory of compact real intervals</td><td>122</td></tr></table>

## H.1. Some reminders of the second part

The Horn theory *Aftr* of strongly real rings is the theory of reduced *f*-rings to which we add the relation symbol $\cdot > 0$ as an abbreviation of "$x \ge 0 \land \exists z x z = 1$" and the function symbol $\text{Fr}$ with the axioms **fr1** and **fr2** (Definition D.5.2).

A strongly real ring is therefore a reduced $\mathbb{Q}$-f-algebra in which any element greater than an invertible positive element is itself invertible, and in which the rule **FRAC** is valid.

Finally, the dynamical theory *Co* of non discrete ordered fields can be described as the theory of local strongly real rings, which amounts to adding the axiom **OTF** (Lemma D.5.4, Item 3) to the theory *Aftr*.

**Lemma H.1.1.** Let $\mathbf{A}$ be a strongly real ring. Let $\mathbf{I} = \{ x \in \mathbf{A} | -1 \le x \le 1 \}$. We define on $\mathbf{I}$ the law $x \oplus y = \frac{1}{2}(x + y)$. The structure obtained on $\mathbf{I}$ for the signature

$$ \text{Signature} : \quad \Sigma_{Icr} = (\cdot = \cdot, \ge, \cdot, > \cdot; \oplus, \cdot, \times, \cdot, \vee, \cdot, \text{Fr}(\cdot, \cdot), -, 0) $$

allows us to reconstruct, in a unique way, the structure of $\mathbf{A}$ as a strongly real ring.

*Proof.* This is essentially because any element $z \in \mathbf{A}$ can be written in the form $x/y$ with $-1 < x < 1$ and $0 < y < 1$ (for example $x = \frac{z}{2+|z|}$ and $y = \frac{1}{2+|z|}$). $\square$

## H.2. Dynamical theory of rings of bounded real maps

We are going to use a more complete signature which corresponds better to the intuition of an interval as a convex subset.

We denote $x \oplus y$ the following composition law in an *f*-ring: $(x, y) \mapsto -1 \vee (1 \land (x + y)).^1$

We denote $\text{Cb}$ the set of systems of barycentric coefficients, defined precisely as follows:

$$ \text{Cb} = \{ (r_k)_{k \in \llbracket 1..n \rrbracket} | n \ge 2, r_1, \dots, r_n \in \mathbb{Q}, r_1, \dots, r_n \ge 0, \sum_{k=1}^{n} r_k = 1 \}. $$

We note $\mathbb{I}_{\mathbb{Q}} = \{ r \in \mathbb{Q} | -1 \le r \le 1 \}$.

<footnote n="1">¹This is the addition, put back into the interval $\mathbf{I}$ if it comes out of it.</footnote>
For each $\rho = (r_k)_{k \in \mathbb{I}[1..n]}$ in Cb, $\mathrm{Brc}_\rho$ is a function symbol of arity $n$ corresponding to the map: $\mathbf{I}^n \to \mathbf{I}$, $(x_k)_{k \in \mathbb{I}[1..n]} \mapsto \sum_{k=1}^n r_k x_k$. The language of the dynamical theory of rings of bounded real maps *Afrb* is defined by the following signature. There is only one sort, denoted *Afrb*

$$ \text{Signature :} \qquad \Sigma_{\text{Afrb}} = (\cdot = 0, \cdot > 0, \cdot \ge 0; (\mathrm{Brc}_{\rho})_{\rho \in \mathrm{Cb}}, \cdot \oplus, \cdot \times, \cdot, \cdot, \cdot \lor, \cdot, \mathrm{Fr}(\cdot, \cdot), (r)_{r \in \mathbb{I}_{\mathbb{Q}}}) $$

## Abbreviations

### Function symbols

* $x \wedge y$ means $-(x \vee -y)$

* $|x|$ means $x \vee -x$

* $x^+$ means $x \vee 0$

* $x^-$ means $-x \vee 0$

### Predicates

* $x = y$ means $x - y = 0$

* $x \ge y$ means $x - y \ge 0$

* $x > y$ means $x - y > 0$

* $x \perp y$ means $|x| \wedge |y| = 0$

* $x \le y$ means $y \ge x$

* $x < y$ means $y > x$

## Axioms

The axioms are all the dynamical rules stated in the language of *Afrb* which are valid for the interval $\mathbf{I} = [-1, 1]$ in the theory *Aftr*($\mathbb{Q}$) of strongly real $\mathbb{Q}$-algebras.

**Lemma H.2.1.** Valid Horn rules in *Afrb* are decidable.

*Proof.* Consequence of Item 3 of Corollary D.5.8. □

Note that it is not known whether valid dynamical rules are decidable. The same question arises in the local case for the dynamical theory *Co*. This question does not seem very important insofar as we are essentially interested in the case of the theories *Crc1* and *CRC2*, where the problem remains mysterious and is added to that of knowing whether we have captured all the algebraic properties of the field $\mathbb{R}$.

# H.3. Dynamical theory of compact real intervals

The dynamical theory *Icr* of compact real intervals has a single sort, denoted *Icr*. Its language is defined by the following signature.

$$ \text{Signature :} \qquad \Sigma_{\text{Icr}} = (\cdot = 0, \cdot > 0, \cdot \ge 0; (\mathrm{Brc}_{\rho})_{\rho \in \mathrm{Cb}}, \cdot \oplus, \cdot \times, \cdot, \cdot, \cdot \lor, \cdot, (T_n)_{n \in \mathbb{N}}, \mathrm{Fr}(\cdot, \cdot), (r)_{r \in \mathbb{I}_{\mathbb{Q}}}) $$

The dynamical theory *Icr* is obtained from the theory *Afrb* described in Section H.2 by adding

* The function symbols $T_n$ for Chebyshev polynomials, with the axioms
  $\vdash T_0(x) = 1, \vdash T_1(x) = x, \vdash T_n(x) = 2xT_{n-1}(x) - T_{n-2}(x) (n \ge 2)$.
  For the main properties of Chebyshev polynomials we refer to the book [Mason & Handscomb, Chebyshev Polynomials]

* The axiom **OTF** (valid for the non discrete ordered field structure) reformulated as follows:

$$ \text{OTF}' x \oplus y > 0 \vdash_{x,y:\text{Icr}} x > 0 \quad \text{op} \quad y > 0 $$

**Remark H.3.1.** Theories *Icr* and *Co* are probably essentially identical. Otherwise it would be necessary to add axioms to *Icr* to make it true. ■
# J. A reinforced language and the first corresponding axioms

## Sommaire

<table><tr><td>Introduction</td><td>123</td></tr><tr><td>J.1 The sorts of reinforced language</td><td>123</td></tr><tr><td>J.2 An abstraction principle</td><td>124</td></tr><tr><td>J.3 First structures on sorts Df<sub>m,n</sub></td><td>124</td></tr><tr><td>Sorts Df<sub>m,n</sub></td><td>124</td></tr><tr><td>Identification of Df<sub>m,n</sub> and (Df<sub>m</sub>)<sup>n</sup></td><td>124</td></tr><tr><td>Composition of maps</td><td>124</td></tr><tr><td>Evaluation of maps</td><td>125</td></tr><tr><td>Constant maps</td><td>125</td></tr><tr><td>Rearrangement of variables</td><td>125</td></tr><tr><td>Gluing of elements of Df<sub>1</sub> on consecutive intervals</td><td>125</td></tr><tr><td>Restrict an element of Df<sub>1</sub> to an interval</td><td>125</td></tr><tr><td>Gluing</td><td>126</td></tr><tr><td>Axioms of weak extensionality</td><td>126</td></tr></table>

## Introduction

We now introduce the sorts of continuous semialgebraic maps in order to obtain a more expressive dynamical theory than *Crc2* for non discrete real closed fields.

This new dynamical theory, which we shall call *CRC3*, attempts here to summarise what we are entitled to expect from an o-minimal structure for uniformly continuous definable maps on $I_R$.

As we have already indicated, we restrict ourselves to uniformly continuous bounded maps, in much the same spirit as Bishop.

### J.1. The sorts of reinforced language

1. The sort *Icr*, for the compact interval $I = [-1, 1]$.

2. For each $m \ge 0, n \ge 1$, a sort $Df_{m,n}$ for uniformly continuous definable maps$^1$ $I^m \to I^n$, the sort $Df_{m,1}$ is noted $Df_m$. In particular $Icr = Df_0 = Df_{0,1}$.

3. A sort $L_i$ seen as a subset of $Df_n$, for certain smooth maps given at the start (at least Chebyshev polynomials).

4. A sort $M_c$ for uniform continuity moduli. They are seen as particular objects of sort $Df_1$.

<footnote n="1">¹Continuous semialgebraic maps for the theory of real closed fields.</footnote>
5. A sort $Df_{mc_n}$ for pairs formed by an object of sort $Df_n$ and by a uniform continuity modulus that fits it.

## J.2. An abstraction principle

For any term $t(x_1, \dots, x_n)$ of type $Icr^n \to Icr$ from the theory (where the $x_i$ cover all the free variables present in the term), a term which provides a map $I^n \to I$ in a model, we must do what is necessary so that there exists a term $\dot{t}$ in $Df_n$ which “evaluates as $t$”. In other words, we need to put in place what we need to mimic, within our geometric theory, the $\lambda$-abstraction of the $\lambda$-calcul.
To do this, the signature

* symbols of type $Df_n \times Icr^n \to Icr$ for the evaluation of a $u : Df^n$ into $x_i : Icr$;

* symbols for the composition of maps (with suitable axioms);

* symbols which give a name to the maps given in the signature (for example $\cdot \times \cdot$ must have a name as an object so $Df_2$);

* ...

This approach is essential if we are to be able to talk uniformly, and not just occasionally, about the properties of continuous definable maps.<fnref n="2" />

*Remark J.2.1.* One might think that some function symbols introduced a priori to mimic $\lambda$-abstraction could have been added a posteriori by virtue of the possibility of adding a function symbol in the case of unique existence, thus providing a dynamical theory essentially identical to the previous one. But the existence (in the unique existence in question) of a well-defined map from the sort $Icr \times Icr$ to the sort $Icr$ does not mean the existence of a corresponding object in $Df_2$, or even its uniqueness (because the extensionality axioms introduced later are too weak). What we mean by introducing a priori these maps as objects of sort $Df_{m,n}$, is that all sufficiently simple maps, in particular those described in the signatures, are indeed continuous and definable. ■

## J.3. First structures on sorts $Df_{m,n}$

### Sorts $Df_{m,n}$

The sort $Icr$ of compact real intervals ($f$-rings) has the structure described in Section H.3.

Each sort $Df_m$ ($m \ge 0, n \ge 1$) is accompanied by function symbols and predicates as well as axioms of rings of bounded real maps (dynamical theory *Afrb*).

*Remark.* The axiom **OTF'** page 122 is not valid for the sorts $Df_m = Df_{m,1}$ for $m \ge 1$. ■

* **Identification of $Df_{m,n}$ and $(Df_m)^n$**

For each $i \in [1..n]$ we have a function symbol $\pi_{m,n,i}$ of type $Df_{m,n} \to Df_m$ corresponding to the $i$-th coordinate. We also give a function symbol of type $(Df_m)^n \to Df_{m,n}$ for the bijection; we will note it $(\varphi_1, \dots, \varphi_n)$ in an admittedly somewhat ambiguous way. With the appropriate axioms, this allows us to identify $Df_{m,n}$ and $(Df_m)^n$.

$$ \vdash_{\varphi_1, \dots, \varphi_n : Df_m} ; \varphi_i = \pi_{m,n,i}((\varphi_1, \dots, \varphi_n)) \quad (i \in [1..n]) $$

$$ \vdash_{\varphi: Df_{m,n}} \varphi = (\pi_{m,n,1}(\varphi), \dots, \pi_{m,n,n}(\varphi)) $$

We give the axioms that $\pi_{m,n,i}$ is a morphism for the ring structures of bounded real maps of $Df_{m,n}$ and $Df_m$.

<footnote n="2">²This is reminiscent of what Kleene does when he defines (uniformly) primitive recursive maps.</footnote>
### • Composition of maps

We have function symbols $C_{m,n,p}$ of type $Df_{n,p} \times Df_{m,n} \to Df_{m,p}$ corresponding to the composition of maps. For $\varphi: Df_{m,n}$ and $\psi: Df_{n,p}$, we write $\psi \circ \varphi := C_{m,n,p}(\psi, \varphi)$. We have constants of sort $Df_{n,n}$ for the “identity maps” $\mathrm{Id}_n: \mathbf{I}^n \to \mathbf{I}^n$.

The axioms for the associativity of composition are given.

We give the axioms which say that for $\varphi$ fixed of sort $Df_{m,n}$, the map $\psi \mapsto \psi \circ \varphi$ is a morphism for the ring structures of bounded real maps of $Df_{n,p}$ and $Df_{m,p}$.

We abbreviate $C_{n,m}$ to the term of type $Df_n \times (Df_m)^n \to Df_m$, defined by

$$C_{n,m}(\varphi, \eta_1, \dots, \eta_n) \stackrel{\text{déf}}{=} \varphi \circ (\eta_1, \dots, \eta_n).$$

### • Evaluation of maps

For $\mathrm{Icr} = Df_0$, the function symbol $C_{n,0}$ of type $Df_n \times \mathrm{Icr}^n \to \mathrm{Icr}$ defines the evaluation of a map in variables taken from $\mathbf{I}$. The associativity of composition is then naturally related as follows with $x_i$ of sort $\mathrm{Icr}$, $\varphi$ of sort $Df_n$ and $\psi$ of sort $Df_1$

$$(\psi \circ \varphi)(x_1, \dots, x_n) = (\psi \circ \varphi) \circ (x_1, \dots, x_n) = \psi \circ (\varphi \circ (x_1, \dots, x_n)) = \psi(\varphi(x_1, \dots, x_n)).$$

### • Constant maps

We have a function symbol $j_n = j_{0,n}$ of type $\mathrm{Icr} \to Df_n$ for constant maps.

Axioms are given which say that these are morphisms for ring structures of bounded real maps<fnref n="3" /> and that the evaluation of a constant map in any arguments is indeed the desired constant.

More generally, if $0 \le m < n$ we have a function symbol $j_{m,n}$ of type $Df_m \to Df_n$ for objects of sort $Df_n$ corresponding to maps which depend only on the $m$ first variables and which can therefore be expressed from objects of sort $Df_m$. The axioms are analogous to those given for the case $m = 0$.

### • Rearrangement of variables

For $m, n > 0$ and a map $\kappa: [1..m] \to [1..n]$ we have an object $\tilde{\kappa}$ of sort $Df_{n,m}$ with the axiom

$$\mathbf{c}_{\kappa} \vdash_{x_1, \dots, x_n; \mathrm{Icr}} \tilde{\kappa}(x_1, \dots, x_n) = (x_{\kappa_1}, \dots, x_{\kappa_m})$$

We also give the associated natural axioms: $\tilde{\kappa} \circ \tilde{\tau} = \tilde{\kappa} \circ \tilde{\tau}$.

So for $m < n$ we have the equality $j_{m,n}(\varphi) = \varphi \circ \tilde{\kappa}$, where $\kappa: [1..m] \to [1..n]$ verifies $\kappa(i) = i$ for $i \in [1..m]$. This equality means that we do not need to introduce the symbol $j_{m,n}$.

We also have, for $\tau_{n,i}: [1] \to [1..n]$ defined by $\tau_{n,i}(1) = i$ and $\psi$ so that $Df_{m,n}$, the equality $\pi_{m,n,i}(\psi) = \tilde{\tau}_{n,i} \circ \psi$.

## Gluing of elements of $Df_1$ on consecutive intervals

### • Restrict an element of $Df_1$ to an interval

If $f$ is of sort $Df_1$, we want to have a name for the map $g$ obtained from the restriction of $f$ to an interval $[a, b] \subseteq \mathbf{I}$.

This is done using a function symbol $\mathrm{Rs}: Df_1 \times \mathrm{Icr} \times \mathrm{Icr} \to Df_1$.

When $a \le b$, we extend $g$ with $g(x) = f(b)$ if $x \ge b$ and $g(x) = f(a)$ if $x \le a$. When $a \ge b$, we permute $a$ and $b$. We therefore have the following axioms

<footnote n="3">³For example for $r \in \mathbb{Q}$, an axiom says that $j_n(r)$ is equal, as an object of sort $Df_n$, to the $r$ given in the ring structure of bounded real maps.</footnote>
• $\vdash_{a,b:Icr,f:Df_1} \mathrm{Rs}(f, a, b) = \mathrm{Rs}(f, a \wedge b, a \vee b)$

• $x \le a \wedge b \vdash_{a,b,x:Icr,f:Df_1} \mathrm{Rs}(f, a, b)(x) = f(a \wedge b)$

• $x \ge a \vee b \vdash_{a,b,x:Icr,f:Df_1} \mathrm{Rs}(f, a, b)(x) = f(a \vee b)$

• $a \wedge b \le x \le a \vee b \vdash_{a,b,x:Icr,f:Df_1} \mathrm{Rs}(f, a, b)(x) = f(x)$

### • Gluings

If $f_0, \dots, f_n$ are of sort $Df_1$, and if $0 \le a_1 \le \dots \le a_n \le 1$ we want to have a name for the map which glues the $f_i$ restricted to $[a_i, a_{i+1}]$, possibly shifted vertically to ensure continuity.

This is done using a function symbol $\mathrm{Rc}_n: (Df_1)^{n+1} \times (Icr)^n \to Df_1$.

We have the following basic axioms (let $a_0 = 0$ and $a_{n+1} = 1$)

$$ \mathbf{Rc}_{n,j} \quad \bigwedge_i (a_i \le a_{i+1}, f_i(a_{i+1}) = f_{i+1}(a_{i+1})) \quad \vdash_{a_i:Icr,f_i:Df_1} \mathrm{Rs}(\mathrm{Rc}(\underline{f}, \underline{a}), a_j, a_{j+1}) = \mathrm{Rs}(f_j, a_j, a_{j+1}) $$

We add the appropriate axioms to force the assumptions of $\mathbf{Rc}_{n,j}$.

## Axioms of weak extensionality

For each sort $Df_n$ with $n \ge 1$ we have the following axiom of weak extensionality.

$$ \mathbf{EXT}_n \quad a > 0 \quad \vdash_{a:Icr,\varphi:Df_n} |\varphi| < j_n(a) \quad \mathbf{op} \quad \exists x \ |\varphi(x)| > \frac{a}{2} $$

As a consequence, a map which is everywhere null is “almost” null: it is increased in absolute value by any constant $> 0$. To conclude that it is null, we would have to invoke **HOF**, a non-geometric axiom which we do not want, or a dubious axiom of archimedeanity such as **AR2** in an infinitary geometric theory.<fnref n="4" />

Note that the axiom $\mathbf{EXT}_0$ simply says that for $x, a: Icr$ and $a > 0$, we have $|x| < a$ or $|x| > \frac{a}{2}$, which is a variant of **OTF**.

Finally, note that the rule $\mathbf{EXT}_n$ follows from **OTF** and the upper bound axioms in Section K.1 (with $m = 0$).

<footnote n="4">⁴A very unsound solution to this weakness of dynamical theory would be to consider as models only those where objects of sort $Df_n$ are $\ge 0$ (resp. $> 0$) exactly when they are evaluated $\ge 0$ (resp. $> 0$) at any point of I.</footnote>
# K. Decisive axioms

## Sommaire

<table><tbody><tr><td><b>K.1 Upper bound axioms</b></td><td><b>127</b></td></tr><tr><td>Axioms of uniform continuity</td><td>127</td></tr><tr><td><b>K.2 Axioms for smooth maps</b></td><td><b>129</b></td></tr><tr><td>Density axiom.</td><td>129</td></tr><tr><td>The derivation</td><td>129</td></tr><tr><td>What other axioms for derivation?</td><td>130</td></tr><tr><td>Axioms of virtual roots</td><td>130</td></tr><tr><td><b>K.3 Axioms of real closure or o-minimal closure</b></td><td><b>130</b></td></tr><tr><td>Finiteness axioms.</td><td>130</td></tr><tr><td>Gluing of maps defined on an open covering</td><td>130</td></tr><tr><td>Gluing of maps defined on a closed covering</td><td>131</td></tr><tr><td>Axioms of extension by continuity</td><td>131</td></tr><tr><td>Conclusion: the improved real closed field structure.</td><td>132</td></tr><tr><td><b>K.4 O-minimal structures</b></td><td><b>132</b></td></tr><tr><td><b>K.5 Some questions</b></td><td><b>133</b></td></tr></tbody></table>

## K.1. Upper bound axioms

The upper bound axioms replace a *priori* the projection axiom for definable parts in o-minimal structures.

For $m > 0$ we have a function symbol $\sup_m$ of type $Df_m \to Icr$ for the lub. It satisfies the axioms describing the lub, namely

$$ \sup_m^{Df} \vdash_{\varphi: Df_m} \varphi \leqslant j_m(\sup_m(\varphi)) $$

$$ \text{SUP}_m^{Df} \quad \epsilon > 0 \quad \vdash_{\epsilon: Icr; \varphi: Df_m} \exists \underline{y} \quad \varphi(\underline{y}) + \epsilon > \sup_m(\varphi) $$

More generally for $n \ge 0$ and $m > 0$ we have a function symbol $\sup_{m+n,n}$ of type $Df_{m+n} \to Df_n$ for the upper bound on the $m$ last variables (in $I^m$) with the following axioms (so $\sup_{m,0}$ is none other than $\sup_m$).

$$ \sup_{m+n,n}^{Df} \vdash_{\varphi: Df_{m+n}} j_{n,m+n}(\sup_{m+n,n}(\varphi)) $$

$$ \text{SUP}_{m+n,n}^{Df} \quad \epsilon > 0 \quad \vdash_{\epsilon, x_1, \dots, x_n: Icr; \varphi: Df_{n+m}} \sup_{m+n,n}(\varphi(\underline{x}, \underline{y}) + \epsilon) > \sup_{m+n,n}(\varphi(\underline{x})) $$

<figure><img src="image_20.png" /></figure>
Axioms of uniform continuity

We now explain how a suitable system of axioms can translate the fact that any definable continuous map admits a uniform continuity modulus, while remaining within the framework of a geometric theory. This is possible because definable continuous maps admit uniform continuity moduli that are themselves particular continuous definable maps. The sorts $Mc$ and $Dfmc_n$ with their axioms are crucial here.

We start by giving a function symbol $j_{Mc}$ for an injection of type $Mc \to Df_1$. An axiom specifies that $j_{Mc}$ is injective.

We have a predicate $Mcu_n$ on $Df_n \times Mc$ which expresses that $\mu$ is a modulus for $\varphi$ by means of the following abbreviation.

• $Mcu_n(\varphi, \mu)$ is an abbreviation for: $\mu(|\varphi(\underline{x}) - \varphi(\underline{x}')|) \le \|(\underline{x}) - (\underline{x}')\|$

where $\|(\underline{z})\| = \sup_i |z_i|$. Here the inequality seems to be written, in the form of evaluated maps, with $x_i$ and $x'_i$ of sort $Icr$. But in fact, this inequality should be read as linking two objects of sort $Df_{2n}$. This avoids the use of the universal quantifier on $x_i$ and $x'_j$ in the definition of uniform continuity! Dynamic theories do not allow the creation of new formulas using universal quantifiers, so we get round the difficulty by mimicking $\lambda$-abstraction!

The following axioms specify constraints on objects $\mu$ of sort $Mc$.

$$ \mathbf{Mc}_1 \quad 0 < b < c \vdash_{\mu:Mc;b,c:Icr} 0 < \mu(b) < \mu(c) \quad \mathbf{Mc}_2 \quad a \le 0 \vdash_{\mu:Mc;a:Icr} \mu(a) = 0 $$

$$ \mathbf{mc}_1 \vdash_{\mu:Mc} Mcu_1(j_{Mc}(\mu), \mu) $$

*Remark.* In the case where we consider only continuous semialgebraic maps, Łojasievicz assures us that any uniform continuity modulus can be taken from the only maps $\epsilon > 0 \mapsto c \epsilon^n$ (with some $c > 0$) ■

The not very intuitive axiom $\mathbf{mc}_1$ will be a valid rule if we require in another axiom that any object of sort $Mc$ corresponds to a convex map. ■

The sort $Dfmc_n$ is defined as a subsort of the product sort $Df_n \times Mc$. It is accompanied by two function symbols $df_n$ and $mc_n$, with the appropriate axioms, which mean that an object of sort $Dfmc_n$ can be considered as a pair of objects $(\varphi, \mu)$ of respective sorts<fnref n="1" /> $Df_n$ and $Mc$. The axiom $\mathbf{mcu}_n$ says how the subsort is defined: if $(\varphi, \mu)$ is of sort $Dfmc_n$, then the predicate $Mcu_n(\varphi, \mu)$ is satisfied.

$$ \mathbf{mcu}_n \vdash_{\psi:Dfmc_n} Mcu_n(df_n(\psi), mc_n(\psi)) $$

Finally, we have the axiom $\mathbf{DFMC}_n$ which says that any object $\varphi$ of sort $Df_n$ is the image by $df_n$ of an object $\theta$ of sort $Dfmc_n$.

$$ \mathbf{DFMC}_n \vdash_{\varphi:Df_n} \exists \theta; df_n(\theta) = \varphi $$

All this machinery explicitly guarantees the uniform continuity of maps represented by objects of sort $Df_n$.

*Remark* K.1.1. Each time we introduced a constant of sort $Df_n$, we actually had to introduce a constant “above it” of sort $Dfmc_n$. This is not difficult because in each case a uniform continuity modulus is obvious. ■

<footnote n="1">¹It is not necessary to create the product type as such. The following axiom will suffice: $df_n(\theta) = df_n(\theta'), mc_n(\theta) = mc_n(\theta') \vdash_{\theta,\theta':Dfmc_n} \theta = \theta'$.</footnote>
## K.2. Axioms for smooth maps

Objects of sort $Li_n$ are seen as objects of sort $Df_n$ which define certain smooth maps (i.e. $C^\infty$). The signature includes a function symbol $j_{Li_n}$ for the corresponding injection, with the axioms which say that it is an injective morphism for suitable laws (those which preserve the smooth maps).

Constant maps and coordinate maps are given as objects of sort $Li_n$.

The sort $Li_1$ contains the Chebyshev polynomials.

It might be possible to introduce other Nash maps into $Li_n$; this should not change the dynamical theory but could facilitate certain proofs.

In the case where we are aiming at a particular o-minimal structure (other than that provided by the continuous semialgebraic maps), other maps can be given which will serve as a basis for the definition of the structure.

### Density axiom

The zeros of a non-zero smooth map (in an o-minimal structure) form a closed $F$ with an empty interior. We can express (at least partially) this density property (for the complementary of $F$) by means of the following axiom

$$ \mathrm{Dens}_n |\varphi(a_1, \dots, a_n)| > 0, \varphi \times \psi = 0 \vdash_{a_1, \dots, a_n; \mathrm{Icr}; \varphi; \mathrm{Li}_n; \psi; Df_n} \psi = 0 $$

### The derivation

We think it is convenient to introduce the derivative (or partial derivative) following the Bridger-Stolzenberg definition (see [1] and [9]). A map $\varphi: \mathbb{I} \to \mathbb{R}$ is continuously derivable if the map “rate of increase” can be extended by continuity, i.e. if there exists a uniformly continuous map $\psi: \mathbb{I}^2 \to \mathbb{R}$ satisfying the identity $[\varphi(x_1) - \varphi(x_2)] = \psi(x_1, x_2) \times (x_1 - x_2)$. The derivative of $\varphi$ is then given by $\varphi'(x) = \psi(x, x)$.

As we only want maps $\mathbb{I}^n \to \mathbb{I}$, we must use an implicit coding $(x, p)$ with $x \in \mathbb{I}$ and $p \in \mathbb{N}$ for the real $px$.

The map $\psi$ is uniquely determined by $\varphi$ (see below the valid rule **Der**) so in our dynamical theory we can introduce it by means of a function symbol $\Delta = \Delta_{1,1}$ of type $Li_1 \to Li_2$ which satisfies the axiom

$$ \mathbf{der} \vdash_{\varphi:Li_1} \varphi(x_1) - \varphi(x_2) = \Delta(\varphi)(x_1, x_2) \times (x_1 - x_2) $$

*Remark.* This equality appears to be written in the form of maps evaluated as linking two objects of sort $\mathbb{R}$, but in fact it should be read as linking two objects of sort $Li_2$, which are evaluated in $(x_1, x_2)$ in the form indicated in the axiom as it appears to be written.

In fact we have to use the implicit coding alluded to above and the rule **der** must in fact be written in the form

$$ \mathbf{der} \vdash_{\varphi:Li_1} \frac{1}{2p}(\varphi(x_1) - \varphi(x_2)) = \Delta_p(\varphi)(x_1, x_2) \times (x_1 - x_2) $$

To avoid complicating the presentation, in the following we pretend that $\Delta(\varphi)$ is the real map “rate of increase”.

The following uniqueness rule follows from the axiom **Dens₂**: in the first member we must read an equality between objects of sort $Df_2$ and the smooth map is $x_1 - x_2$ seen as an element of $Li_2$.

$$ \mathbf{Der} \varphi(x_1) - \varphi(x_2) = \psi(x_1, x_2) \times (x_1 - x_2) \vdash_{\varphi:Li_1; \psi: Df_2} \Delta(\varphi) = \psi $$

In the same way, for several variables, analogous axioms are required for each partial derivative.
In particular, for $n \ge 2$ and $i \in [1..n]$ we have a function symbol $\Delta_{n,i}$ of type $Li_n \to Li_{n+1}$ which satisfies the axiom

$$ \mathbf{der}_{n,i} \vdash_{\varphi:Li_n} \varphi(x_1, \dots, x_i, \dots, x_n) - \varphi(x_1, \dots, x'_i, \dots, x_n) = \Delta_{n,i}(\varphi)(x_1, \dots, x_i, x'_i, \dots, x_n) \times (x_i - x'_i) $$

This equality must be read as linking two objects of sort $Li_{n+1}$.

*Remark.* Using the upper bound axiom, we obtain that smooth maps are lipschitzian, which gives a particularly simple uniform continuity modulus. ■

## What other axioms for derivation?

Here we need to consider which axioms need to be introduced corresponding to the usual properties of derivation. Most of these properties should result from the definition (axioms $\mathbf{der}_{n,i}$) and the axioms $\mathbf{Dens}_n$.

## Axioms of virtual roots

Virtual roots can be defined a priori for any smooth map whose derivative of order $k$ is $> 0$ (on $\mathbb{I}$), by virtue of Lemma E.2.3 and the uniform constructive version of the mean value theorem. We then obtain most of the properties described in Definition E.2.5 and Theorem E.2.6. The polynomial $f(X) = X^d - (a_{d-1}X^{d-1} + \dots + a_1X + a_0)$ which depends on $d+1$ variables can be replaced by any smooth $\varphi$ map of $d+1$ variables $X, a_1, \dots, a_d$ whose $k$-th partial derivative with respect to $X$ is $> 0$ as an object of sort $Li_{d+1}$.

If $\inf(\varphi^{(k)}) = \phi(a_1, \dots, a_d)$, we can treat the map $\psi_k = \varphi + (c - \phi)^+ X^k / k!$, for a constant $c > 0$. Its $k$-th derivative with respect to $X$ is $\ge c$, and it is equal to $\varphi$ if $\phi \ge c$. We can then introduce the $k$ virtual roots of $\varphi$ on $\mathbf{I}$ as objects of sort $Df_d$ as in Definition E.2.5 and Theorem E.2.6, but using our $\lambda$-abstraction. More precisely, we have “virtual roots” function symbols $Rv_{d,k,j}$ of type $Li_{d+1} \to Df_d$. And we have the corresponding axioms, direct translations of Definition E.2.5 and of Theorem E.2.6 (by replacing $-\infty$ and $+\infty$ by $-1$ and $+1$).

## K.3. Axioms of real closure or o-minimal closure

From now on we deal with axioms that correspond to the general idea of real closure and o-minimal structure.

### Finiteness axioms

The virtual root axioms are already axioms of finiteness, but independent of any o-minimal structure.

We should have an analogue to Proposition E.6.3 (table of signs and variations) for continuous semialgebraic maps, and this should also work for o-minimal structures. In classical mathematics, tables of signs and variations exist for definable maps of an o-minimal structure, and Proposition E.6.3 shows how to transform the classical statement into a constructive one. Here again, the problem is to formulate dynamical axioms that capture this type of result. One solution would be to have an infinite dynamical theory with axioms that say roughly that a continuous definable map is “piecewise smooth monotone” in a statement to be specified, similar to Item 2 of Proposition E.6.3.

### Gluing of maps defined on an open covering

A finite cover of $\mathbf{I}^n$ by definable opens is given here in the form

$$ V_i = \{ \underline{x} \in \mathbf{I}^n \mid g_i(\underline{x}) > 0 \} \quad i \in [1..p] $$