[proofplan] Use quantifier elimination for real closed fields to replace the defining formula by a Boolean combination of polynomial equations and strict polynomial inequalities in the single variable $x$. The finitely many roots in $R$ of the polynomials appearing in this quantifier-free formula form a finite set of algebraic points over the parameter field $K$. These points decompose $R$ into finitely many singleton cells and open interval cells; on every open interval cell, each polynomial has constant sign, so the Boolean combination has constant truth value. Selecting precisely the cells on which the formula holds gives the desired finite union. [/proofplan] [step:Replace the defining formula by a Boolean combination of polynomial sign conditions] Since $X$ is definable over $a$, there is an $\mathcal{L}_{\mathrm{or}}$-formula $\varphi(x,a)$ with one object variable $x$ such that \begin{align*} X = \{x \in R : R \models \varphi(x,a)\}. \end{align*} Let $K \subset R$ be the subfield generated by the coordinates of $a$. By Tarski-Seidenberg quantifier elimination for real closed fields (citing a result not yet in the wiki: Tarski-Seidenberg Quantifier Elimination for Real Closed Fields), the formula $\varphi(x,a)$ is equivalent in $R$ to a quantifier-free Boolean combination of atomic formulas of the form \begin{align*} p_i(x) = 0 \quad\text{and}\quad p_i(x) > 0, \end{align*} where $p_1,\dots,p_N \in K[X]$ are polynomials in one indeterminate $X$ with coefficients in $K$. Replacing the list by the nonzero polynomials among them does not change the argument; constant zero and nonzero constant polynomials have fixed truth values in every cell. [guided] We begin by turning the definability problem into a finite algebraic sign problem. Since $X$ is definable over the parameter tuple $a$, there is a formula $\varphi(x,a)$ in the language of ordered rings such that \begin{align*} X = \{x \in R : R \models \varphi(x,a)\}. \end{align*} The parameters $a_1,\dots,a_m$ generate a subfield $K \subset R$. Every term in the variable $x$ with parameters from $a$ evaluates to a polynomial expression in $x$ whose coefficients lie in $K$. Now apply Tarski-Seidenberg quantifier elimination for real closed fields (citing a result not yet in the wiki: Tarski-Seidenberg Quantifier Elimination for Real Closed Fields). It says that every formula in the language of ordered rings is equivalent, over any real closed field, to a quantifier-free formula. In one variable, this means that $\varphi(x,a)$ is equivalent in $R$ to a Boolean combination of finitely many polynomial equations and strict polynomial inequalities: \begin{align*} p_i(x) = 0 \quad\text{and}\quad p_i(x) > 0, \end{align*} with $p_i \in K[X]$ for $1 \le i \le N$. Constant polynomials cause no geometric subdivision of the line: a constant zero polynomial makes $p_i(x)=0$ always true, and a nonzero constant polynomial has a fixed sign. Thus only the nonzero nonconstant polynomials matter for cutting the line into cells. [/guided] [/step] [step:Cut the line at the algebraic roots of the appearing polynomials] For each $i \in \{1,\dots,N\}$, define the root set \begin{align*} Z_i := \{r \in R : p_i(r) = 0\}. \end{align*} Since $p_i \in K[X]$ is a nonzero one-variable polynomial, $Z_i$ is finite, and every element of $Z_i$ is algebraic over $K$. Hence the finite set \begin{align*} Z := \bigcup_{i=1}^N Z_i \end{align*} is contained in $K_R^{\mathrm{alg}}$. Write its distinct elements in increasing order as \begin{align*} c_1 < c_2 < \cdots < c_\ell. \end{align*} If $Z = \varnothing$, take $\ell = 0$. The associated cells are the singleton cells $\{c_j\}$ for $1 \le j \le \ell$ and the open interval cells \begin{align*} (-\infty,c_1),\quad (c_1,c_2),\quad \dots,\quad (c_{\ell-1},c_\ell),\quad (c_\ell,\infty), \end{align*} with the evident interpretation when $\ell = 0$, namely the single interval cell $R = (-\infty,\infty)$. [guided] We now define the finite set of possible boundary points. For each polynomial $p_i \in K[X]$, let \begin{align*} Z_i := \{r \in R : p_i(r) = 0\}. \end{align*} Because $p_i$ is a nonzero polynomial in one variable, it has at most $\deg(p_i)$ roots in the field $R$, so $Z_i$ is finite. Moreover, if $r \in Z_i$, then $p_i(r)=0$ is a nontrivial polynomial equation over $K$, so $r$ is algebraic over $K$. Therefore $Z_i \subset K_R^{\mathrm{alg}}$ for every $i$. Taking the union over the finitely many polynomials gives \begin{align*} Z := \bigcup_{i=1}^N Z_i \subset K_R^{\mathrm{alg}}. \end{align*} This set is finite. List its distinct elements in increasing order: \begin{align*} c_1 < c_2 < \cdots < c_\ell. \end{align*} These points split the ordered field line into finitely many cells: the point cells $\{c_j\}$ and the open interval cells between consecutive roots, together with the two unbounded interval cells. If there are no roots, then no cutting occurs and the only interval cell is all of $R$. [/guided] [/step] [step:Show that every polynomial has constant sign on each interval cell] Let $I \subset R$ be one of the open interval cells. Fix $i \in \{1,\dots,N\}$. By construction, $p_i$ has no root in $I$. We prove that $p_i$ has constant sign on $I$. Since $R$ is real closed, $p_i$ factors in $R[X]$ as \begin{align*} p_i(X) = \lambda \prod_{\alpha \in A_i} (X-\alpha)^{m_\alpha} \prod_{q \in Q_i} q(X), \end{align*} where $\lambda \in R^\times$, $A_i \subset R$ is the finite set of roots of $p_i$ in $R$, each $m_\alpha \in \mathbb{N}$ is the multiplicity of the root $\alpha$, and each $q \in Q_i$ is an irreducible quadratic polynomial over $R$. For $\alpha \in A_i$, the function \begin{align*} \ell_\alpha: I &\to R \\ x &\mapsto x-\alpha \end{align*} has constant sign on $I$, because $\alpha \notin I$. Each irreducible quadratic factor $q$ has constant sign on all of $R$: writing \begin{align*} q(X)=aX^2+bX+c \end{align*} with $a \in R^\times$, irreducibility implies $b^2-4ac<0$, and completing the square gives \begin{align*} q(X)=a\left(X+\frac{b}{2a}\right)^2+\frac{4ac-b^2}{4a}, \end{align*} so $q(X)$ has the sign of $a$ for every $X \in R$. Thus every factor in the displayed product has constant sign on $I$, and therefore $p_i$ has constant sign on $I$. [guided] The point of cutting at all roots is that, after the cut, no polynomial can change sign inside an interval cell. We verify this algebraically. Let $I$ be one of the open interval cells, and fix a polynomial $p_i$. By construction of the cells, $I$ contains no root of $p_i$. Since $R$ is real closed, every polynomial over $R$ factors into linear factors and irreducible quadratic factors. Thus \begin{align*} p_i(X) = \lambda \prod_{\alpha \in A_i} (X-\alpha)^{m_\alpha} \prod_{q \in Q_i} q(X), \end{align*} where $\lambda \in R^\times$, $A_i$ is the finite set of roots of $p_i$ in $R$, $m_\alpha$ is the multiplicity of the root $\alpha$, and $Q_i$ is a finite list of irreducible quadratic factors. For a linear factor, define \begin{align*} \ell_\alpha: I &\to R \\ x &\mapsto x-\alpha. \end{align*} Since $\alpha$ is not in the interval $I$, either every $x \in I$ satisfies $x<\alpha$, or every $x \in I$ satisfies $x>\alpha$. Hence $\ell_\alpha$ is everywhere negative on $I$ or everywhere positive on $I$. For an irreducible quadratic factor, write \begin{align*} q(X)=aX^2+bX+c \end{align*} with $a \in R^\times$. Irreducibility over a real closed field is equivalent here to having no root in $R$, so its discriminant satisfies $b^2-4ac<0$. Completing the square gives \begin{align*} q(X)=a\left(X+\frac{b}{2a}\right)^2+\frac{4ac-b^2}{4a}. \end{align*} The second term has the same sign as $a$, because $4ac-b^2>0$. The square term is nonnegative and is multiplied by $a$, so the whole expression has the sign of $a$ for every $X \in R$. Thus each quadratic factor has constant sign on all of $R$. The product of finitely many functions with constant sign has constant sign. Therefore $p_i$ has constant sign on $I$. [/guided] [/step] [step:Select the cells on which the Boolean combination is true] On any singleton cell $\{c_j\}$, the truth value of $\varphi(x,a)$ is fixed because there is only one point. On any open interval cell $I$, each atomic condition $p_i(x)=0$ is constantly false, and each atomic condition $p_i(x)>0$ has constant truth value by the previous step. Hence the entire Boolean combination equivalent to $\varphi(x,a)$ has constant truth value on $I$. Let $\mathcal{C}$ be the finite collection of all point cells and interval cells constructed above, and define \begin{align*} \mathcal{C}_X := \{C \in \mathcal{C} : C \subset X\}. \end{align*} Then \begin{align*} X = \bigcup_{C \in \mathcal{C}_X} C. \end{align*} Each point cell has its point in $K_R^{\mathrm{alg}}$, and each interval cell has endpoints in $K_R^{\mathrm{alg}} \cup \{-\infty,\infty\}$. Therefore $X$ is a finite union of points and open intervals of the required form. [/step]