Rational polynomial solvability reduces to stratifiability of semilinear sets

Introduction

For a set $S \subseteq\mathbb{N}^d$ and distinct letters $a_1,\ldots,a_d$, consider

The coordinates record the lengths of successive letter blocks; a language contained in $a_1^*\cdots a_d^*$ is called letter-bounded. Suppose that $S$ is semilinear: equivalently, it is definable in first-order arithmetic with addition, or Presburger arithmetic. Can we decide whether $L(S)$ is context-free?

Ginsburg and Spanier’s characterization [2 Theorem 2.1] expresses context-freeness of $L(S)$ as a restriction on the periods in a presentation of $S$. A linear set consists of a base vector plus arbitrary nonnegative integer combinations of finitely many period vectors, and a semilinear presentation writes $S$ as a finite union of linear sets. Such a presentation is a stratification if each period has at most two nonzero coordinates and no two periods in the same component connect alternating positions: for $i<j<k<l$, one period cannot be nonzero at $i,k$ while another is nonzero at $j,l$. A set admitting a stratification is stratifiable. The characterization states that $L(S)$ is context-free if and only if $S$ is stratifiable. Our decision question is therefore whether a set given by an arbitrary semilinear presentation admits a stratification.

For example, the periods $(1,1,0)$ and $(0,1,1)$ stratify $\{(n,n+m,m):n,m\in\mathbb{N}\}$, whose language is $\{a^n b^{n+m}c^m:n,m\in\mathbb{N}\}$. In contrast, the semilinear set

is not stratifiable, since the language it induces is not context-free.

Our main contribution is the following:

To prove Theorem 1.1, we first apply the classical reduction from polynomial equations to quadratic systems [6]. It therefore suffices to reduce rational solvability of finite quadratic systems to stratifiability. We do this by two reductions through an intermediate problem. Section 2 provides a detailed overview of the reductions. Formal treatment starts with the preliminaries in Section 3. Section 4 then proves the first reduction and Section 5 the second. Section 6 combines them with the standard reduction from polynomial equations to quadratic systems. Margin arrows link to appendix proofs (↓) and back to the main text (↑).

Conditional undecidability consequence. An OpenAI preprint [9 Theorem 1.1] claims that rational polynomial solvability is undecidable. As of 9 October 2026, we are not aware of a completed independent review of this proof. If its claim is correct, Theorem 1.1 implies undecidability of general stratifiability. The reduction itself does not depend on that claim.

Related work. Ginsburg and Spanier studied languages contained in $w_1^* \cdots w_k^*$ for fixed words $w_i$ in [1]. Their later paper [2 Theorems 1.3 and 2.1] proves the effective equivalence between semilinear presentations and Presburger formulas and the stratified-period characterization used here. They decide stratifiability for a single linear set [2 Theorem 2.2] and explicitly leave the semilinear case open in 1966 [2 p. 296]. The problem also appears in Ginsburg’s book [3]. Ibarra and Seki [4] relate stratifiability to equivalence questions for multitape automata and establish decidable cases. Leroux, Penelle, and Sutre [5] prove coNP-completeness of stratifiability for sets of nonnegative integer solutions of a single finite system of linear inequalities. Our input class allows arbitrary finite unions of linear sets.

Overview of the two reductions

We now consider a finite system $f_i(x_1,\ldots,x_n)=0$ of rational polynomial equations of degree at most two. We reduce its rational solvability to the following separation problem, then reduce that problem to stratifiability.

The intermediate separation problem. The input is a finite family of rational subspaces $D_1,\ldots,D_k\leq\mathbb{Q}^r\times\mathbb{Q}^r$, given by spanning vectors.

The separator is a product map $u\times v$ defined by nonzero rational linear forms $u,v\colon\mathbb{Q}^r\to\mathbb{Q}$ by $(u\times v)(x,y)=(u(x),v(y))$. It separates a pair $w$ from the subspaces if

The problem, finite separation by Cartesian products of rational linear forms, asks whether there is a finite list of separators such that every rational $w\notin\bigcup_i D_i$ can be separated by one of those separators.

For example, take $D=\{((t,t),(t,s)):t,s\in\mathbb{Q}\}$. An outside pair $((x_1,x_2),(y_1,y_2))$ has $x_1\ne y_1$ or $x_2\ne y_1$. In the first case, the separator with $u_1(x)=x_1$ and $v_1(y)=y_1$ distinguishes it from $D$; in the second, use $u_2(x)=x_2$ and $v_2(y)=y_1$. Each separator sends $D$ to the diagonal, while at least one separates its pair off that diagonal. Thus $u_1\times v_1,u_2\times v_2$ are a finite separating family. It actually suffices to construct a separator for each outside pair: Lemma 4.2 selects a finite subcollection separating all of them, using an elementary basis argument.

First reduction: from equations to finite separation

Recovering a root from one designated pair. We illustrate the construction with $f=x^2-1$. Let $[p]$ be the coefficient vector of $p$ in the basis $1,x,x^2$, so $[f]=(-1,0,1)$, and write $[p,q]=([p],[q])$ and $u[p]=u([p])$. We want separation of the designated pair $e=[0,1]$ by a separator $u\times v$ to force a root. A diagonal subspace $\Delta$ will make the forms $u$ and $v$ agree after normalization, a multiplication subspace $M$ will make their common form be an evaluation, and an equation subspace $E$ will make that evaluation vanish on $f$:

If $u\times v$ separates $e$, linearity gives its image $(0,v[1])$. Thus $v[1]\ne0$, since every subspace image contains zero; also $u[1]\ne0$, since otherwise $[1,1]\in\Delta$ has the same image as $e$. Divide the forms by these two values so that $u[1]=v[1]=1$. The image of $\Delta$ contains $(1,1)$ and avoids $(0,1)$, so it is the diagonal and the normalized forms agree. Denote their common form by $\lambda$.

Put $c=\lambda[x]$. The two generator images of $M$, namely $(1,c)$ and $(c,\lambda[x^2])$, must be collinear. Hence $\lambda[x^2]=c^2$, making $\lambda[p]=p(c)$ for every polynomial $p$ of degree at most two. Thus $\lambda$ is evaluation at $c$. The images $(1,2)$ and $(f(c),f(c))$ of the generators of $E$ span the plane unless $f(c)=0$, so separation forces a root. For $f=x^2-2$, separation would require $c^2=2$ and is therefore impossible over $\mathbb{Q}$.

Assigning image slopes to separate $[x,1]$. Finite separation requires that every outside pair is separated. Yet even for $f=x^2-1$, the pair $[x,1]$ lies outside $\Delta$, $M$, $E$ and cannot be separated (Example 4.4). We therefore modify the subspaces to permit its separation, while retaining the root requirement at $e$.

Choose nonzero rational linear forms $u,v$ on the coefficient space of $\mathbb{Q}[x]_{\le2}$ and write $(u\times v)[x,1]=(\rho,\sigma)$. If $(\rho,\sigma)\ne(0,0)$, we can choose a rational slope $s_L$ for each $L\in\{\Delta,M,E\}$ with $\sigma\ne s_L\rho$. Placing each modified subspace image in its chosen line would separate $[x,1]$, provided the image of $[x,1]$ stays $(\rho,\sigma)$. To do this, we give $v$ an independently adjustable coefficient for every generator.

Number the generators of each $L$ in the listed order, starting at $d=0$, and write them as $[p_{L,d},q_{L,d}]$. Introduce a distinct polynomial variable $b_{L,d}$ for each index $(L,d)$ and append these monomials to the coefficient basis. Thus $[b_{L,d}]$ is a new unit vector; coefficient vectors of polynomials in $\mathbb{Q}[x]_{\le2}$ acquire zero coefficients at every $b_{L,d}$. Replace each generator by $[p_{L,d}+b_{L,d},q_{L,d}]$, and call their span $\widehat L$. For example, $\widehat E=\operatorname{span}\{[1,2+b_{E,0}],[f,f+b_{E,1}]\}$. Extend $v$ by assigning, for every $L,d$,

These are values on independent new basis vectors; the values $v[b_{L,d}]$ can still be chosen independently. Every modified generator has image $(u[p_{L,d}],s_Lu[p_{L,d}])$, so $\widehat L$ maps into the line of slope $s_L$. Since $[x,1]$ has zero coefficients at the new basis vectors, its image stays $(\rho,\sigma)$ and avoids these lines. For example, choose $u[1]=1$, $u[x]=2$, $u[x^2]=0$, let $v$ extract the constant coefficient on $\mathbb{Q}[x]_{\le2}$, and take every $s_L=3$. The image of $[x,1]$ is then $(2,1)$, off every chosen line.

Preserving the root requirement at $e$. The freedom to choose image slopes must preserve the implication from separation of $e$ to a root. We therefore introduce one last variable $t$, giving the coefficient basis $1,x,x^2,t,(b_{L,d})$, and add

The pair $e$ still lies outside every subspace. A separator of $e$ must have $u[t] \ne0$, since otherwise the generator of $H$ has the same image $(0,v[1])$ as $e$. The image of $K$ then contains the nonzero horizontal vector $(u[t],0)$. Any nonzero value $v[b_{L,d}]$ would add a nonhorizontal vector and make that image the whole plane. Thus $v[b_{L,d}]=0$ for every $L,d$. Each modified generator has the same image as $[p_{L,d},q_{L,d}]$, so the restrictions of $u,v$ to $\mathbb{Q}[x]_{\le2}$ separate $e$ from $\Delta$, $M$, $E$ and yield a root by the earlier calculation.

Conversely, at a rational root $c$, let both forms evaluate polynomials in $\mathbb{Q}[x]_{\le2}$ at $c$:

Extend them by setting

For every positive rational $\tau$, the images of $\widehat{\Delta},\widehat{M},\widehat{E}$ have finite slopes $1,c,2$, the image of $K$ is horizontal, and $H$ maps to $\mathbb{Q}(\tau,1)$. All avoid the nonzero vertical image of every nonzero multiple of $e$.

For the earlier separator of $[x,1]$, instead complete the assignment with

Now $H$ maps to the vertical axis and $K$ into the diagonal. The image $(2,1)$ avoids both and the slope-$3$ images of the $\widehat{L}$, so $u\times v$ separates $[x,1]$ from the enlarged family.

More generally, the same extension rule separates every $[p,q]\notin\mathbb{Q}e$ with $p,q\in\mathbb{Q}[x]_{\le2}$, choosing the forms and slopes afresh for each pair. If $p\ne0$, choose $v[1]=1$ and $u[p]\in\{0,v[q]\}$, then choose every $s_L\ne v[q]/u[p]$: the image avoids the vertical axis, the diagonal, and the chosen slope lines. If $p=0$ and $q$ is nonconstant, choose $u[1]=1$, $v[1]=0$, and $v[q]\ne0$, then recompute all added values by the same rule. Now $H$ maps to zero, while the nonzero vertical image $(0,v[q])$ avoids the diagonal containing the image of $K$ and the finite-slope images of all $\widehat{L}$. Together with the root-based separators for the nonzero multiples of $e$, this separates every nonzero pair $[p,q]$ with $p,q\in\mathbb{Q}[x]_{\le2}$ from the enlarged family. Among these pairs, a root is required only for the nonzero multiples of $e$.

Separating outside pairs with added variables. We now seek separators for the outside pairs with a nonzero coefficient at $t$ or some $b_{L,d}$ in at least one entry. We first construct separators that do not require a root. Every constructed subspace has zero coefficient of $t$ in its second entry. If an outside pair’s second entry has a nonzero coefficient of $t$, let $v$ extract that coefficient and take any nonzero $u$. Its image is off the horizontal axis containing every subspace image, so $u\times v$ separates the pair from all the constructed subspaces.

For pairs whose second entry has zero coefficient of $t$, changing the slopes can change the pair’s image through its $b_{L,d}$ terms. We choose the values of $u,v$ on $1,x,x^2$ jointly with the slopes, extend $v$ by the earlier formula, and set $u[b_{L,d}]=v[b_{L,d}]$ and $u[t]=v[t]=0$. Setting $u[t]=0$ permits nonzero $v[b_{L,d}]$: otherwise the generator of $K$, together with $[t,0]$, would have images spanning the plane. With $v[1]=1$, the image of $H$ is vertical and that of $K$ lies in the diagonal, so an image $(\rho,\sigma)$ outside these and the chosen slope lines gives a separator. For such a pair with first entry $[\alpha t]$ whose full second entry is not a scalar multiple of $[1]$, choose new values on $1,x,x^2$ and new slopes, subject to $u[1]=1$ and $v[1]=0$, and recompute all added values by the extension formula. Some such choice gives the pair a nonzero vertical image, while $H$ maps to zero and the other subspace images have finite slopes.

These slope constructions separate every outside pair whose second entry has zero coefficient of $t$, except possibly pairs $[\alpha t,\beta]$ and pairs $g+\alpha[t,0]$ with $g\in\widehat{L}$.

For $[\alpha t,\beta]$, being outside $K$ and $H$ gives $\beta\ne0$ and $\beta\ne\alpha$. If $\alpha=0$, the pair is a nonzero multiple of $e$, already separated under the root hypothesis. If $\alpha\ne0$, let $u$ extract the coefficient of $t$ and let $v$ extract the constant coefficient. The image $(\alpha,\beta)$ avoids the vertical images of the $\widehat{L}$, the horizontal image of $K$, and the diagonal image of $H$, so these forms separate the pair.

The slope extensions cannot separate an outside pair $\boldsymbol{g}+\alpha[t,0]$, with $\alpha\ne0$ and $\boldsymbol{g}\in\widehat{L}$, from $\widehat{L}$: setting $u[t]=0$ sends it to the same image as $\boldsymbol{g}$. Instead, fix $u$ to extract the coefficient of $t$ and let $v$ vary on the coefficient space of $\mathbb{Q}[x]_{\le2}$, extending it by zero on every added basis vector. We determine when these choices separate the shifted pair from the whole family. Write $\boldsymbol{g}=[p,q+\sum_d\theta_d b_{L,d}]$, where $[p,q]\in L$. Here $q\ne0$: the second-entry polynomials of the listed generators of $L$ are linearly independent, so $q=0$ would force all $\theta_d=0$ and $\boldsymbol{g}=0$, placing the shifted pair in $K$.

The pair’s image is $(\alpha,v[q])$, off the vertical images of all the $\widehat{L}$. The images of $K$ and $H$ are the horizontal axis and $\mathbb{Q}(1,v[1])$, respectively. Thus $u\times v$ separates the pair exactly when $v[q]\ne0$ and $v[q]-\alpha v[1]\ne0$. If $q\ne\alpha$, the polynomials $q$ and $q-\alpha$ are both nonzero, so some rational linear form satisfies both inequalities. This separates every such shifted pair without a root. When $q=\alpha$, however, the image is always $\alpha(1,v[1])$, in the image of $H$; no choice of $v$ completes a separator with this fixed $u$. Such a pair is

Removing the $t$-shift gives $\boldsymbol{g}\in\widehat{L}$. By the construction of $\widehat{L}$, this means $[p,\alpha]\in L$, and the $\theta_d$ are the coefficients of $[p,\alpha]$ in the listed generators of $L$. Determining $[p,\alpha]$ therefore determines the added terms too, and hence the whole shifted pair.

In $\Delta$, the condition $[p,\alpha]\in\Delta$ forces $p=\alpha$. Only the generator $[1,1]$ occurs, so $\boldsymbol{g}=\alpha[1,1+b_{\Delta,0}]$. In $M$, the second entry is divisible by $x$, so it cannot equal the nonzero constant $\alpha$. In $E$, write $[p,\alpha]=[a+\kappa f,2a+\kappa f]$, with $a,\kappa\in\mathbb{Q}$. Since $f=x^2-1$, a constant second entry forces $\kappa=0$ and $a=\alpha/2$. Only the generator $[1,2]$ occurs, so $\boldsymbol{g}=\alpha[\frac{1}{2},1+\frac{1}{2}b_{E,0}]$. Restoring the shift $\alpha[t,0]$ therefore gives the following two shifted lines:

The preceding constructions separate every outside pair off these two lines, using a rational root only to separate the nonzero multiples of $e$. We now choose the evaluation extension to separate the nonzero pairs on these two lines as well.

Choosing the root extension for the two shifted lines. Return to the evaluation extension defined by (2) and (3), with $u[t]=\tau>0$. The two shifted representatives have images $(1+\tau,1)$ and $(\frac{1}{2}+\tau,1)$. Their nonzero second coordinates keep them off the horizontal image of $K$. Their first-coordinate offsets $1$ and $\frac{1}{2}$ keep them off $\mathbb{Q}(\tau,1)$, the image of $H$. Each finite-slope $\widehat{L}$ image excludes at most one value of $\tau$ for each representative. Choose one positive rational $\tau$ outside these finitely many exclusions. The resulting separator separates every nonzero multiple of both representatives and preserves the separation of the nonzero multiples of $e$ already proved.

A rational root therefore supplies separators for every outside pair, and Lemma 4.2 supplies a finite list. Conversely, such a list separates $e$ and yields a root. Section 4 gives the construction for arbitrary quadratic systems.

Second reduction: from finite separation to stratifiability

For a family $D_1,\ldots,D_k$, represent integer pairs outside its union by differences of nonnegative coordinates. The output is

Membership is given by linear equations and their negations, so Lemma 5.1 computes a semilinear presentation of $S$. The order of the four coordinate blocks will be used when checking stratifiability.

For each separator $u\times v$, collect the elements of $S$ whose represented pairs it separates. Membership in this subset depends on two weighted sums:

After clearing the coefficient denominators of $u,v$, the permitted values satisfy a Presburger condition on two integer-weighted sums over consecutive coordinate blocks. Lemma B.7 shows that the associated letter-bounded language is context-free; Ginsburg and Spanier’s characterization [2 Theorem 2.1] makes this subset stratifiable. Thus a finite separating family for all outside pairs gives a finite stratifiable cover of $S$.

Conversely, suppose $S$ is stratifiable. We extract a finite separating family for $D_1,\ldots,D_k$ from a stratification. Increasing matching positive and negative coordinates by the same amount leaves the represented pair unchanged. The representations of each outside integer pair therefore contain a grid of these cancellation directions. In any finite stratification, some component meeting this grid has nonnegative period combinations with signed difference zero spanning all these directions.

Consider the periods occurring in these combinations. Their signed images can be added and subtracted within the set of pairs represented by the component. The restriction on alternating supports ensures that every linear form vanishing on the rational span of these images is a linear combination of one fixed form $u$ on the first entry and one fixed form $v$ on the second. The forms can be chosen nonzero, and $\ker u\times\ker v$ is therefore contained in that span. Fix such a separator for every component with the stated spanning property.

Fix a rational pair outside the subspaces. If a selected separator fails to separate it from $D_i$, the pair differs from a point of $D_i$ by a rational combination of those period images. Choose one such expression for each candidate component and each $D_i$ whenever possible. Clear all these coefficients and the pair’s coordinates by one common integer multiple, then select a component representing that multiple. Subtracting the resulting integer combination from the represented multiple would put a point of $D_i$ among the pairs represented by this component, a contradiction. Thus the fixed separators separate every outside rational pair (Lemma 5.3). The proof adapts the minimal-element argument of Ginsburg and Spanier [2], proof of Theorem 1.3 and the structure of stratified periods studied by Brough [7].

Preliminaries

Put $\mathbb{N}=\{0,1,2,\ldots\}$. Bold letters denote vectors and tuples; their coordinates are written in ordinary type. A linear set in $\mathbb{N}^d$ is a set

The vector $a$ is its base, and the elements of $P$ are its periods. A semilinear set is a finite union of linear sets. A semilinear presentation lists the base and periods of each component.

A finite period set $P$ is stratified if

1. every $t \in P$ has at most two nonzero coordinates; and

2. there are no $t_1,t_2 \in P$ and $i < j < k < l$ with $t_{1,i}t_{1,k}t_{2,j}t_{2,l} \ne0$.

A stratification of a set is a finite semilinear presentation whose period sets are stratified. A set is stratifiable if it has a stratification.

Presburger arithmetic is first-order arithmetic on the integers, or on $\mathbb{N}$, with addition and order but without multiplication of variables. A subset of $\mathbb{N}^d$ is semilinear if and only if it is Presburger-definable. One can effectively convert between these formulas and semilinear presentations [2 Theorem 1.3]. We also use the following classical theorem [2 Theorem 2.1].

All vector spaces are over $\mathbb{Q}$. We write $\operatorname{span}$ for linear span, $U \le V$ for a subspace, and $\dim V$ for dimension. A linear form $u:\mathbb{Q}^r \to\mathbb{Q}$ is a weighted sum $u(z) = \sum_i c_i z_i$ with $c_i \in\mathbb{Q}$. For a linear map $T$, $T(E)$ and $T^{-1}(E)$ denote image and inverse image.

Write $\mathbb{Q}[z]_{\le d}$ for polynomials of total degree at most $d$, whose monomials of degree at most $d$ are a basis. We use $[p]$ for the coefficient vector in a specified ordered monomial basis, $[p,q] = ([p],[q])$, and $u[p] = u([p])$.

The source problem for our construction is the following.

Solvability of quadratic systems over $\mathbb{Q}$

Input: A finite list $f_1,\ldots,f_m \in\mathbb{Q}[x_1,\ldots,x_n]$ of polynomials of total degree at most two.

Question: Is there a tuple $c \in\mathbb{Q}^n$ such that $f_i(c) = 0$ for every $i$?

Rational coefficients are represented by integer numerators and nonzero integer denominators.

From quadratic systems to finite separation

Recall that a separator is the map $u \times v : (x,y) \mapsto(u(x),v(y))$ defined by nonzero rational forms $u,v : \mathbb{Q}^r \to\mathbb{Q}$. It separates $w$ from a family of subspaces when $(u \times v)(w)$ lies outside all their images under $u \times v$.

Finite separation by Cartesian products of rational linear forms

Input: An integer $r \ge1$ and finitely many rational subspaces $D_1,\ldots,D_k \le\mathbb{Q}^r \times\mathbb{Q}^r$, each specified by finitely many rational spanning vectors.

Question: Is there a finite list of separators $u_1 \times v_1,\ldots,u_h \times v_h$ such that, for every rational pair $w$ outside the subspaces, some $j$ satisfies

Proof. Write the input equations as $f_i = 0$. First test by rational linear algebra whether $1 \in\operatorname{span}_{\mathbb{Q}}\{f_1,\ldots,f_m\}$. If so, the system has no rational solution; replace it by $x^2 - 2 = 0$, which also has no rational solution and whose equation span does not contain $1$. We may therefore assume $1 \notin\operatorname{span}_{\mathbb{Q}}\{f_1,\ldots,f_m\}$.

The construction in § 4.1 and § 4.2 computes from the input equations a finite family $\mathcal{D}$ of rational subspaces and a designated pair outside their union. Lemmas 4.5 and 4.3 show that any separator of this pair yields a rational solution. Thus a finite separating family for $\mathcal{D}$ yields a solution.

Conversely, under the assumption on the equation span, Lemma 4.7 separates every outside pair off three explicit rational lines, by choosing image slopes and extracting coefficients of the added variable $t$. If a rational solution exists, the evaluation extension in Lemma 4.8 separates every nonzero pair on those three lines with one choice of its positive parameter. Lemma 4.2 then selects finitely many separators serving all outside pairs.

The following fact about a fixed finite family of rational subspaces justifies this finite selection. It allows the forms in a separation proof to depend on the pair being separated.

Making separation at one pair equivalent to a rational root

Let the input equations be $f_i(\mathbf{x}) = 0$, $1 \leq i \leq m$, where $\mathbf{x} = (x_1,\ldots,x_n)$. Throughout this construction assume $1 \notin\operatorname{span}_{\mathbb{Q}}\{f_1,\ldots,f_m\}$, as permitted by the preliminary step in the proof of Theorem 4.1. Fix an ordering of the monomials $1$, $x_j$, and $x_jx_k$ with $j \leq k$ in $\mathbb{Q}[\mathbf{x}]_{\leq2}$, beginning with $1$. Represent polynomials by their coefficient vectors in this basis, as in § 3.

To recover a common root, we make the separator determine one evaluation of the input polynomials. A diagonal subspace makes its forms agree after normalization; multiplication subspaces make their common form respect products; an equation subspace makes this evaluation vanish on every $f_i$. Define

Let $\mathcal{L} = \{\Delta, M_1,\ldots,M_n,E\}$. Set $\mathbf{e} = [0,1]$. A separator of this designated pair will determine a rational solution.

Enlarging the space while preserving the root requirement at $\mathbf{e}$

We enlarge the space so that a rational solution supplies separators for every outside pair. Giving each basis generator its own added coordinate in the second entry lets $v$ move the modified generator’s image vertically, independently of the other generators. adjustments place each modified subspace image in a chosen line through the origin of finite rational slope. A separate coordinate and two additional subspaces ensure that separating $e$ forces $v$ to vanish on every coordinate added to a generator. Each modified generator then has the same image as the generator it replaces, so separation of $e$ still forces a rational root.

Fix a basis $[p_{L,d},q_{L,d}]$, $0 \le d < \dim L$, for each $L \in\mathcal{L}$. For $\Delta$, take $[\mu,\mu]$ over the monomials, with $[1,1]$ first; for $M_j$, take $[\mu,x_j\mu]$ over $\mu\in\{1,x_1,\ldots,x_n\}$. For $E$, compute a basis $[\tilde{f}_1],\ldots,[\tilde{f}_s]$ of $\operatorname{span}\{[f_1],\ldots,[f_m]\}$ and take $[1,2],[\tilde{f}_1,\tilde{f}_1],\ldots,[\tilde{f}_s,\tilde{f}_s]$, in this order. A sum over $L,d$ ranges over all these basis vectors; in particular, $d=0$ indexes $[1,1]$ for $\Delta$ and $[1,2]$ for $E$.

The generators specified for $E$ are independent: subtracting the entries of a zero linear combination forces the coefficient of $[1,2]$ to vanish, and independence of the $[\tilde{f}_i]$ forces the other coefficients to vanish.

Introduce a polynomial variable $t$ and one variable $b_{L,d}$ for every basis index $(L,d)$, and work in the vector space

The summands share $1$. Extend the monomial basis of $\mathbb{Q}[x]_{\le2}$ by $t$ and all $b_{L,d}$, obtaining a basis of length $r$ for both entries. Each coefficient vector is uniquely

For $p\in\mathbb{Q}[x]_{\le2}$, the vector $[p]$ has zero coefficients at $t$ and every $b_{L,d}$; the designated pair in the enlarged space is still $e=[0,1]$. Replacing $[p_{L,d},q_{L,d}]$ by $[p_{L,d},q_{L,d}+b_{L,d}]$ changes its second image value by $v[b_{L,d}]$. To make each modified generator map to $(u[p_{L,d}],v[q_{L,d}])$ whenever $u\times v$ separates $e$, the line $H$ below forces $u[t]\ne0$, allowing $K$ to force every $v[b_{L,d}]=0$.

Accordingly, define the following subspaces of $\mathbb{Q}^r\times\mathbb{Q}^r$:

Let $\mathcal{D}=\{\widehat{L}:L\in\mathcal{L}\}\cup\{H,K\}$ be the resulting family of $n+4$ subspaces.

The constructed instance of finite separation is $\mathcal{D}$. Its finite separating families yield rational solutions by Lemmas 4.5 and 4.3. For the converse, put $Y=\mathbb{Q}^{2r}\setminus\bigcup_{D\in\mathcal{D}}D$. We first separate all pairs in $Y$ off three explicit lines, using only the assumption on the equation span. A rational solution supplies one separator for the nonzero pairs on those lines; Lemma 4.2 then gives a finite separating family.

Separating pairs without using a root

The slope extensions keep $u[t]=0$ to permit nonzero $v[b_{L,d}]$ while keeping the image of $K$ proper. These extensions send $g+\alpha[t,0]$ to the same point as $g\in\widehat{L}$. We then choose $u$ to extract the coefficient of $t$ and set every $v[b_{L,d}]=0$, which permits $u[t]=1$ while keeping the image of $K$ horizontal. The proof first treats the pairs $[\alpha t,\beta]$, then the shifted pairs $g+\alpha[t,0]$.

Proof. The coefficient extraction and slope extensions verified in Appendix A.6 separate all pairs in $Y$ except possibly

where $\beta\ne0$, $\beta\ne\alpha$ in the first case, and $\alpha\ne0$, $q\ne0$ in the second. For $[\alpha t,\beta]$, the case $\alpha=0$ gives a nonzero multiple of $e$, on the first line in (10). If $\alpha\ne0$, let $u$ and $v$ extract the coefficients of $t$ and $1$, respectively. The images of all the $\widehat{L}$ lie on the vertical axis, the image of $K$ is horizontal, and the image of $H$ is diagonal. The pair’s image $(\alpha,\beta)$ avoids all of them because $\alpha\ne0$, $\beta\ne0$, and $\beta\ne\alpha$. Both forms are nonzero.

Now consider a shifted pair $g+\alpha[t,0]$ in (11). Fix $u$ to extract the coefficient of $t$, and let $v$ vary on the coefficient space of $\mathbb{Q}[x]_{\le2}$, extending it by zero on every added basis vector. For every $J\in\mathcal{L}$, the $J_b$ generators map to $(0,v[q_{J,d}])$; the image of $K$ is horizontal, and $H$ maps to $\mathbb{Q}(1,v[1])$. The shifted pair maps to $(\alpha,v[q])$ and already avoids every $\widehat{J}$ image since $\alpha\ne0$. Thus it is separated exactly when

By linearity, the second inequality is $v[q-\alpha]\ne0$. If $q\ne\alpha$, both $q$ and $q-\alpha$ are nonzero. The product $v[q]v[q-\alpha]$, viewed as a polynomial in the coefficients of $v$, is therefore nonzero at some rational tuple, giving a separator. Both forms are nonzero since $u[t]=1$ and $v[q]\ne0$.

If $q=\alpha$, the shifted pair has image $\alpha(1,v[1])$, in the image of $H$ for every $v$. To describe these pairs, note that $[p,\alpha]\in L$ with $\alpha\ne0$. The coefficients $\theta_d$ in $g$ are precisely the coefficients of $[p,\alpha]$ in the fixed basis of $L$, so determining $[p,\alpha]$ also determines every added term.

For $L=\Delta$, this forces $p=\alpha$. Only the basis generator $[1,1]$ occurs, so the shifted pair is $\alpha[1+t,1+b_{\Delta,0}]$. No $M_j$ contributes such a pair, since its second entry is divisible by $x_j$ and cannot be a nonzero constant. For $L=E$, write $[p,\alpha]=[a+h,2a+h]$ with $h\in\operatorname{span}_{\mathbb{Q}}\{f_1,\ldots,f_m\}$. The equation $2a+h=\alpha$ makes $h$ constant; the standing assumption on the equation span gives $h=0$ and $a=\alpha/2$. Only the basis generator $[1,2]$ occurs, so the shifted pair is $\alpha[\frac{1}{2}+t,1+\frac{1}{2}b_{E,0}]$. These are precisely the other two lines in (10).

Completing separation using a rational root

Lemma 4.7 separates every outside pair off the three lines in (10) without using a root. At a rational root $c$, let both forms evaluate polynomials in $\mathbb{Q}[x]_{\le2}$ at $c$, set every $u[b_{L,d}]=v[b_{L,d}]=v[t]=0$, and put $u[t]=\tau>0$. Every such extension separates the nonzero multiples of $e$, so we choose $\tau$ to separate the nonzero pairs on the two shifted lines as well. Their representatives have images $(1+\tau,1)$ and $(\frac{1}{2}+\tau,1)$, which avoid the horizontal image of $K$ and the image $\mathbb{Q}(\tau,1)$ of $H$. Each $\widehat{L}$ image excludes at most one value of $\tau$ for each representative, so one positive rational value separates every nonzero multiple of either representative while preserving separation of the nonzero multiples of $e$.

When the system has a rational solution, Lemma 4.8 supplies a separator for every outside pair; Lemma 4.2 selects a finite list, completing the first reduction.

From finite separation to stratifiability

Let $D_1,\ldots,D_k\leq\mathbb{Q}^r\times\mathbb{Q}^r$ be an instance of finite separation, with $u\times v$ as in Section 4. We construct a semilinear set that is stratifiable exactly when this instance admits a finite separating family.

To construct the semilinear output, we represent an integer coordinate as a difference of two nonnegative coordinates. We keep all $x$ positions before all $y$ positions so that the two forms act on consecutive groups of letter blocks. Within each entry, the positive and negative blocks are indexed in the same order, so matching pairs for distinct indices alternate; this is the arrangement used to extract the forms from a stratification (Lemma B.5). We therefore order the coordinates as

Define the signed-coordinate map $A:\mathbb{Q}^{4r}\to\mathbb{Q}^{2r}$ and the sets $Y,S$ by

The set $Y$ consists of the rational pairs outside the deleted union. The set $S$ contains every nonnegative integer representation of each integer pair in $Y$. These representations are not unique: for example, $(x_i^+,x_i^-)=(1,0)$ and $(2,1)$ both represent $x_i=1$. More generally, increasing matching positive and negative coordinates by the same nonnegative integer leaves their difference unchanged. Keeping every representation supplies the grids of cancellation directions used to extract separators from a stratification.

To obtain a stratification from a finite separating family, we first consider the signed representations of pairs separated by one fixed separator $u\times v$:

Every $S_{u,v}$ is contained in $S$.

Proof sketch. After clearing the coefficient denominators of $u$, $v$, membership in $S_{u,v}$ is a Presburger condition on two integer-weighted sums over consecutive coordinate blocks. Lemma B.7 and Theorem 3.1 give stratifiability.

Proof sketch. Adding the same amount to a positive coordinate and its matching negative coordinate preserves the represented pair. Thus the signed representations of an outside integer pair contain a grid of independent cancellation directions. In a finite stratification, some component meeting this grid has nonnegative period combinations with image zero under $A$ that span all those directions.

For each such component, let $L$ be the rational span of the images under $A$ of periods occurring in these combinations. These period images can be added and subtracted within the component’s image. The support restriction gives nonzero forms $u$, $v$ with $\ker u \times\ker v \subseteq L$. Fix one such separator for every component with the spanning property. A failure to separate a rational pair $w \in Y$ from $D_i$ implies $w \in D_i + L$. Choose one expression as a point of $D_i$ plus a rational combination of those period images for each candidate component and each $D_i$ whenever possible. Clear all these coefficients and the coordinates of $w$ by one positive integer multiple before selecting a component representing that multiple. Subtracting the resulting integer combination would put a point of $D_i$ in the component’s image under $A$, contradicting its containment in $Y$.

Proof. Lemma 5.1 computes the required presentation from the subspace generators. If a finite separating family exists, the sets $S_{u,v}$ indexed by its members cover $S$: every represented integer pair lies outside the subspaces and is separated by a member of the family. Lemma 5.2 makes their finite union stratifiable. Conversely, if $S$ is stratifiable, Lemma 5.3 supplies a finite family separating every rational pair outside the subspaces.

Proof of the Main Theorem

Proof of Theorem 1.1. Given the input polynomial $f \in\mathbb{Z}[x_1,\ldots,x_n]$, the standard reduction to quadratic systems [6 proof of Theorem 7.5, pp. 262–263] computes a finite system $\mathcal{E}$ of rational polynomial equations of degree at most two that has a rational solution if and only if $f$ has a rational zero.

Theorem 4.1 computes a family of rational subspaces admitting a finite separating family exactly when $\mathcal{E}$ has a rational solution. Theorem 5.4 then computes a finite semilinear presentation of a set $S$ that is stratifiable exactly when that separating family exists. Thus $S$ is stratifiable exactly when $f$ has a rational zero.

Proof. Under the stated hypothesis, rational polynomial solvability is undecidable. Apply Theorem 1.1, and then Theorem 3.1 for the language formulation.

Conclusion

We have given a computable many-one reduction from rational polynomial solvability to stratifiability of semilinear sets and, equivalently, to context-freeness of letter-bounded languages specified by semilinear exponent sets. If the undecidability claim in [9] is correct, both decision problems are undecidable.

Let $H_{10}(\mathbb{N})$ denote the problem of deciding whether a polynomial with integer coefficients has a zero in nonnegative integers. Stratifiability is computably enumerable: enumerate candidate stratifications and check equality with the input set in Presburger arithmetic. The Davis–Putnam–Robinson–Matiyasevich theorem [6] therefore gives a computable many-one reduction from stratifiability to $H_{10}(\mathbb{N})$. Can one prove an unconditional computable many-one reduction in the opposite direction, from $H_{10}(\mathbb{N})$ to stratifiability? This would establish undecidability independently of [9]. Adapting the proof of Lemma 4.3 to $H_{10}(\mathbb{N})$ would require a mechanism forcing the recovered coordinates to be nonnegative integers. A fixed system of polynomial equations with rational unknowns expressing membership in $\mathbb{N}$ would provide such a mechanism; finding one is equivalent to the longstanding open problem of existentially defining $\mathbb{Z}$ in $\mathbb{Q}$ [10].

Our result places no fixed bound on the dimension of the semilinear set. For which fixed dimensions is stratifiability decidable? Every semilinear subset of $\mathbb{N}^{2}$ is stratifiable, since both restrictions on periods hold automatically. Dimension three is the first nontrivial case: $\{(n,n,n): n \in\mathbb{N}\}$ is not stratifiable, since any nonzero period of a linear set contained in it has all three coordinates nonzero. Is stratifiability decidable for arbitrary semilinear subsets of $\mathbb{N}^{3}$?

If [9 Corollary 7.1] is correct, stratifiability and rational polynomial solvability are Turing equivalent: each can be decided using oracle queries to the other problem. This does not settle the stronger many-one converse, which the cited draft does not establish. Can one effectively associate a single integer polynomial $f_S$ with every semilinear presentation of a set $S$, so that $f_S$ has a rational zero exactly when $S$ is stratifiable?

AI disclosure. The ideas and writing in this paper were developed in conjunction with ChatGPT-6 Astra. The author takes full responsibility for the correctness and presentation of the work.

Proofs for the first reduction

We first prove the finite-subcollection lemma for an arbitrary finite family of rational subspaces. For the subsequent proofs, the subspaces, bases, and coefficient notation are those of Section 4: $\mathcal{L} = \{\Delta, M_1, \ldots, M_n, E\}$, $\mathcal{D} = \{\widehat{L} : L \in\mathcal{L}\} \cup\{H, K\}$ is its enlarged family, and $Y$ consists of the pairs outside $\bigcup_{D \in\mathcal{D}} D$.

Selecting finitely many separators

Proof of Lemma 4.2. For each separator $T = u \times v$ in the given collection, failure to separate from $D_i$ means membership in the rational subspace

Choose rational linear forms $\ell_{T,i,j}$ whose simultaneous vanishing defines $B_{T,i}$, and define the polynomial

A sum of rational squares is zero exactly when every summand is zero. Consequently, $h_T(z) \ne0$ exactly when $T$ separates $z$ from every $D_i$. If $B_{T,i}$ is the whole space, use no equations for it: the empty sum is zero, as required. For $k = 0$, the empty product is 1.

The polynomials $h_T$ have degree at most $2k$ in the pair coordinates, so their span is finite-dimensional. Choose a basis of this span from the polynomials $h_T$ themselves, and retain their separators. If all the retained polynomials vanish at a pair, every $h_T$ vanishes there; conversely, a nonzero retained value gives separation by a member of the given collection. These finitely many separators therefore separate exactly the same pairs. When the span is zero, the empty subcollection suffices. ◀

Recovering a root before enlargement

Proof of Lemma 4.3. Suppose $u \times v$ separates $e$. Its image is $(0, v[1])$, so $v[1] \ne0$ because every subspace image contains zero. The image of $\Delta$ is proper and contains $(u[1], v[1])$; it is therefore a line avoiding $(0, v[1])$. Hence $u[1] \ne0$, and every $(u[p], v[p])$ is proportional to $(u[1], v[1])$. Dividing $u$ and $v$ by their respective values at 1 gives a common form $\lambda$ with $\lambda[1] = 1$. This invertible rescaling of the two scalar coordinates preserves separation.

The proper image of $M_j$ contains $(1, \lambda[x_j])$, so

Put $c = (\lambda[x_1], \ldots, \lambda[x_n])$. Taking $p = x_k$ shows that $\lambda$ agrees with evaluation at $c$ on every quadratic monomial, hence on every polynomial of degree at most two. The image of $E$ contains $(1, 2)$ and $(f_i(c), f_i(c))$; their determinant is $-f_i(c)$, so properness forces $f_i(c) = 0$ for every $i$.

Conversely, evaluation at a rational solution gives a nonzero form $\lambda$ with $\lambda[1] = 1$. For $u = v = \lambda$, the images of $\Delta$, $M_j$, $E$ lie in lines of slopes $1$, $c_j$, $2$, respectively, all avoiding the image $(0, 1)$ of $e$.

Why $[x,1]$ cannot be separated before enlargement

Verification of Example 4.4. For $f=x^2-1$, consider the three subspaces

The separator $\lambda\times\lambda$, where $\lambda[p]=p(1)$, separates $e=[0,1]$ from this family, but the outside pair $[x,1]$ cannot be separated.

Indeed, $[x,1]$ is not in $\Delta$, its second entry is not $x$ times its first, and the first entry of every pair in $E$ has zero $x$ coefficient. Thus it lies outside all three spaces.

Suppose nonzero forms $u,v$ separated $[x,1]$. The image of $\Delta$ cannot be the whole plane, so $u,v$ are proportional. Both are nonzero; rescaling one of them therefore gives a common form $\lambda$ and preserves separation. Put

The image of $M$ is generated by $(a,b)$ and $(b,c)$, and the image of $E$ by $(a,2a)$ and $(c-a,c-a)$. Neither image can be the whole plane. Their determinants consequently give

If $a=0$, then $b=0$, so the image $(b,a)$ of $[x,1]$ is zero and belongs to every image. If $a\ne0$, then $c=a$ and $b=\pm a$. When $b=a$, $(b,a)$ belongs to the diagonal image of $\Delta$. When $b=-a$, it is the negative of $(a,b)$ and belongs to the image of $M$. Every case contradicts separation.

Recovery in the enlarged space

Proof of Lemma 4.5. A pair in $\widehat{L}$ with all added second coordinates zero has every generator coefficient zero, so it cannot equal $e$. In $H$, a nonzero constant term in the second entry comes with a nonzero coefficient of $t$ in the first; in $K$, the constant term in the second entry is zero. Thus $e$ lies outside every member of $D$.

Suppose $u\times v$ separates $e$. Its image is $(0,v[1])$, with $v[1]\ne0$. If $u[t]=0$, the generator $[t,1]\in H$ would have the same image, so $u[t]\ne0$. The image of $K$ therefore contains the nonzero horizontal vector $(u[t],0)$. Any nonzero $v[b_{L,d}]$ would make this image the whole plane, preventing separation. Consequently every $v[b_{L,d}]=0$, and

Thus $(u\times v)(\widehat{L})=(u\times v)(L)$ for every $L\in\mathcal{L}$. The restriction of $v$ to $\mathbb{Q}[x]_{\le2}$ is nonzero since $v[1]\ne0$. If $u[1]=0$, the generator $[1,1+b_{\Delta,0}]$ would have the same image as $e$; hence the restriction of $u$ is also nonzero. These restrictions separate $e$ from $\mathcal{L}$.

Why equal forms do not suffice

Verification of Example 4.6. A pair in $\widehat{L}$ with zero-valued added second coordinates must be zero, while the first entry of every pair in $H$ or $K$ has zero coefficient at $1$. Thus $[1,1]$ lies outside every member of $D$. If $u[b_{\Delta,0}]=0$, the generator $[1,1+b_{\Delta,0}]$ has the same image under $u\times u$ as $[1,1]$. If $u[b_{\Delta,0}]\ne0$, the image of $K$ contains the nonzero diagonal vector $(u[b_{\Delta,0}],u[b_{\Delta,0}])$, and hence the image $(u[1],u[1])$ of $[1,1]$. Neither case permits separation.

Separation by variable image slopes

We prove the preliminary classification (11) used in Lemma 4.7, including its restrictions on $\alpha,\beta,q$.

Proof. Under the standing assumption $1 \notin\operatorname{span}_{\mathbb{Q}}\{f_1,\ldots,f_m\}$, each coordinate projection of every $L \in\mathcal{L}$ is injective; this will let us recover generator coefficients from either entry of a pair. An element of $E$ can be written as $[a+h,2a+h]$, where $a \in\mathbb{Q}$ and $h \in\operatorname{span}_{\mathbb{Q}}\{f_1,\ldots,f_m\}$. If either entry is zero, then $h=-a$ or $h=-2a$ is constant. The only constant in the equation span is zero, so $h=0$ and $a=0$. Each coordinate projection of $E$ is therefore injective. The same property is immediate for $\Delta$ and for the first projection of $M_j$; the second projection of $M_j$ is injective because multiplication by $x_j$ is injective. Consequently, for each $L$, the coefficient vectors $[p_{L,d}]$ are linearly independent, as are the vectors $[q_{L,d}]$.

Pairs whose second entry has a nonzero coefficient of $t$. First take $u$ to extract the coefficient of $1$ and $v$ to extract the coefficient of $t$. Every pair in every member of $\mathcal{D}$ has zero coefficient of $t$ in its second entry, so these forms separate every pair whose second entry has a nonzero coefficient of $t$. Every pair whose second entry has zero coefficient of $t$ can be written as

Assigning slopes to the modified subspaces. To put the image of $K$ into the diagonal and the image of each $\widehat{L}$ into a line of slope $s_L$, choose the values of $u,v$ on the monomial basis of $\mathbb{Q}[x]_{\leq2}$ and the slopes $s_L$ as independent parameters, subject to $v[1]=1$, and extend $u,v$ by

Indeed, the modified generator has image $(u[p_{L,d}],s_Lu[p_{L,d}])$. In $K$, the generator $[t,0]$ maps to zero and every $[b_{L,d},b_{L,d}]$ maps to a diagonal vector. The image of $H$ is vertical. The value $v[t]$ does not affect any of these images or the image of $w$, since every second entry under consideration has zero coefficient of $t$.

To compute the image of $w$ in (15), put

For fixed $w$, denote its image by $(\rho,\sigma)$. These coordinates are polynomials in the values of $u,v$ on the monomial basis of $\mathbb{Q}[x]_{\leq2}$ and in the slopes $s_L$:

To keep $(\rho,\sigma)$ off the vertical axis, the diagonal, and the lines of slopes $s_J$, it suffices to require $\rho\ne0$, $\sigma-\rho\ne0$, and $\sigma-s_J\rho\ne0$ for every $J\in\mathcal{L}$. We identify the pairs for which one of these polynomials is zero for every parameter choice. Write $\widehat{J}+\mathbb{Q}[t,0]$ for the pairs $g+\alpha[t,0]$ with $g\in\widehat{J}$ and $\alpha\in\mathbb{Q}$. In the following identities, $\equiv0$ means that a polynomial is identically zero on the parameter space $v[1]=1$:

For (17), the coefficients of the independent $s_L$ give $p_L^\eta=0$, hence every $\eta_{L,d}=0$ by independence of the $p_{L,d}$; then $\rho=u[p]$ forces $p=0$. For (18), those coefficients give $\theta_{L,d}=\eta_{L,d}$ for every $L,d$, leaving $v[q]-u[p]$. Varying the values of $u$ on that monomial basis independently gives $p=0$, and then $q=0$. Indeed, if $v[q]=0$ for every form with $v[1]=1$, varying its values on the nonconstant monomials shows that every nonconstant coefficient of $q$ is zero; its constant coefficient must then also be zero. The conditions $p=q=0$ and $\theta_{L,d}=\eta_{L,d}$ for every $L,d$ say exactly that $w\in K$.

For (19), the coefficients of $s_J^2$ and $s_Js_L$ for $L\ne J$ first force all $p_L^\eta=0$, so every $\eta_{L,d}=0$. The remaining $s_L$ coefficients give $p_L^\theta=0$ for $L\ne J$ and $p_J^\theta=p$. Thus all $\theta_{L,d}$ with $L\ne J$ are zero. The term independent of the slopes is $v[q-q^\theta]$; its vanishing for every form with $v[1]=1$ gives $q=q^\theta$. These conditions say precisely that $w\in\widehat{J}+\mathbb{Q}[t,0]$. The reverse implications in all three identities follow by substitution.

Consequently, if $w\in Y$ has first entry not a scalar multiple of $[t]$ and lies in none of the spaces $\widehat{L}+\mathbb{Q}[t,0]$, then

is a nonzero polynomial. A nonzero rational polynomial has a rational tuple where it is nonzero: this follows by induction on the number of variables from the fact that a nonzero univariate polynomial has only finitely many roots. Choose such a tuple for (20). Then the image of $w$ lies outside every subspace image. The factor $\rho$ and the normalization $v[1]=1$ ensure that both forms are nonzero.

Making the image of $H$ zero. With $v[1]=1$ and $u[t]=0$, every pair whose first entry is $[\alpha t]$ maps into the vertical image of $H$, so these extensions cannot separate it. To separate such a pair, we instead make the image of $H$ zero. Choose new values of $u,v$ on the monomial basis of $\mathbb{Q}[x]_{\le2}$, subject to $u[1]=1$ and $v[1]=0$, and new slopes $s_L$; then recompute their values on the added basis vectors by (16). Consider a pair whose first entry is $[\alpha t]$ and whose second entry is not a scalar multiple of $[1]$. For these new extensions, the image $(\rho,\sigma)$ has $\rho=0$, and $H$ maps to zero. The polynomial $\sigma$ is nonzero: if it vanished identically, its $s_L$ coefficients would give $u[p_L^\theta]=0$ for all forms with $u[1]=1$, hence $p_L^\theta=0$ and every $\theta_{L,d}=0$. The remaining identity $v[q]\equiv0$ for forms satisfying $v[1]=0$ would make $q$ constant, a contradiction. Choose a rational solution of $\sigma\ne0$. The pair’s image $(0,\sigma)$ is nonzero and avoids the finite-slope lines containing the images of all $\widehat{L},K$. Both forms are nonzero, since $u[1]=1$ and $\sigma\ne0$.

The constructions above prove separation for every pair in $Y$ except possibly those described in (11). For $[\alpha t,\beta]\in Y$, membership outside $K$ gives $\beta\ne0$ and membership outside $H$ gives $\beta\ne\alpha$. If $w=g+\alpha[t,0]\in Y$ with $g\in\widehat{L}$, then $\alpha\ne0$ because $w\notin\widehat{L}$. Write the second entry of $g$ as $[q+\sum_d\theta_d b_{L,d}]$, with $q\in\mathbb{Q}[x]_{\le2}$. If $q=\sum_d\theta_d q_{L,d}=0$, injectivity of the second projection of $L$ would force every $\theta_d=0$. Then $g=0$ and $w\in K$, a contradiction.

Completing separation using a rational root

Proof of Lemma 4.8. Fix a rational root $c$. For a positive rational parameter $\tau$, define

Both forms are nonzero at $[1]$. The $\widehat{J}$ images lie in lines of slopes $1,c_1,\ldots,c_n,2$, while the image of $K$ is horizontal and $H$ maps to $\mathbb{Q}(\tau,1)$. Thus every nonzero multiple of $e$ has nonzero vertical image and is separated. For the other two lines in (10), the representatives have images

Both avoid the image of $K$, since their second coordinate is nonzero. Membership in the image $\mathbb{Q}(\tau,1)$ of $H$ would force $1=0$ or $\frac{1}{2}=0$, respectively. For a line of slope $s$ containing a $\hat{J}$ image, membership requires $1=s(1+\tau)$ or $1=s(\frac{1}{2}+\tau)$. If $s=0$, neither is possible; otherwise these equations exclude the two values

Choose one positive rational $\tau$ outside the finite set excluded by all the slopes $1,c_1,\ldots,c_n,2$. This separator separates both representatives and hence every nonzero rational multiple of either. It also preserves separation of every nonzero multiple of $e$, proved for every positive $\tau$. Lemma 4.7 supplies separators for the pairs in $Y$ off these three lines, proving the claim. ◀

Proofs for the second reduction

The subspaces $D_i$, map $A$, sets $Y$, $S$, and separators $u\times v$ are as in § 5. We first prove effective semilinearity of $S$, then extract finitely many separators from a stratification. Finally, we prove the weighted-sums lemma and apply it to the regions $S_{u,v}$.

Computing a semilinear presentation

Proof of Lemma 5.1. Gaussian elimination and denominator clearing compute integer matrices $M_i$ with $D_i=\{z\in\mathbb{Q}^{2r}:M_i z=0\}$. Since $A$ has integer entries, so does $C_i=M_iA$. If $C_i$ has $s_i$ rows, then for $n\in\mathbb{N}^{4r}$,

An empty disjunction is false and an empty conjunction is true. This is a Presburger formula, so the effective conversion recalled in § 3 produces a finite semilinear presentation. ◀

Period combinations with image zero

Put $d=2r$ and $K_A=\ker A=\{z\in\mathbb{Q}^{2d}:Az=0\}$. For nonzero rational forms $u,v$, define

Since $\ker(u\times v)=V(u,v)$, we have

Thus $Y_{u,v}$ is precisely the set of pairs separated by $u\times v$, and $Y_{u,v}\subseteq Y$. In the notation of (14),

To extract separators from a stratification of $S$, we first need a component whose nonnegative period combinations with image zero span $K_A$. For each outside integer pair, the following argument finds such a component containing one of its signed representations.

For $\mathbf{z} \in\mathbb{Q}^d$, the fiber of $\mathbf{A}$ over $\mathbf{z}$ is $\mathbf{A}^{-1}(\mathbf{z}) = \{\mathbf{n} \in\mathbb{Q}^{2d}: \mathbf{A}\mathbf{n} = \mathbf{z}\}$. To describe the part of a linear set in this fiber, we use the coordinatewise order on $\mathbb{N}^{\ell}$: $\mathbf{b} \le\mathbf{c}$ means $b_i \le c_i$ for every $i$.

Proof. Every infinite sequence in $\mathbb{N}$ has an infinite nondecreasing subsequence: either one value occurs infinitely often, or each bounded set of values occurs only finitely often and an increasing subsequence can be chosen. Apply this successively to the $\ell$ coordinates. Every infinite sequence in $\mathbb{N}^{\ell}$ then has two terms in coordinatewise nondecreasing order, so an infinite sequence of distinct minimal elements is impossible. For any $\mathbf{n}$ in the subset, the set of elements below $\mathbf{n}$ is finite and nonempty; a minimal member is also minimal in the original subset. The case $\ell= 0$ is immediate. ◀

For a finite period set $P = \{\mathbf{t}_1, \ldots, \mathbf{t}_{\ell}\} \subseteq\mathbb{N}^{2d}$, let $\mathbf{P}$ be the matrix with these columns. Define

Thus $K_P$ is spanned by the nonnegative period combinations that leave the represented pair unchanged. The next proof uses the minimal-element argument for linear-equation solution sets in Ginsburg and Spanier’s proof of Theorem 1.3 [2].

Proof. First fix one component $\mathbf{a} + P^*$ and put

By Lemma B.1, $E_{\mathbf{b}}$ has finitely many minimal elements $\mathbf{c}$. Every $\mathbf{n} \in E_{\mathbf{b}}$ is above one of them, and $\mathbf{n} - \mathbf{c} \in Z_P$; conversely, $\mathbf{c} + Z_P \subseteq E_{\mathbf{b}}$. Hence

It follows that $(\mathbf{a} + P^*) \cap\mathbf{A}^{-1}(\mathbf{z})$ lies in finitely many translates $\mathbf{a} + \mathbf{P}\mathbf{c} + K_P$.

Choose $\mathbf{n}_{\mathbf{z}} \in\mathbb{N}^{2d}$ with $\mathbf{A}\mathbf{n}_{\mathbf{z}} = \mathbf{z}$. For each of the $d$ coordinates of $\mathbb{Q}^d$, let $\mathbf{k}_i$ have a 1 in its positive and negative source positions and zeros elsewhere. The vectors $\mathbf{k}_1,\ldots,\mathbf{k}_d$ are a basis of $K_A$, and

If every component meeting this fiber had $K_{P_j} \ne K_A$, the preceding description would cover this grid by finitely many translates of proper subspaces of $K_A$. In the coordinates given by $\mathbf{k}_1,\ldots,\mathbf{k}_d$, each translate satisfies an equation $c_1t_1 + \cdots+ c_dt_d = b$ in which some $c_i$ is nonzero. It contains at most $(N+1)^{d-1}$ points of $\{0,\ldots,N\}^d$: fix all but a coordinate with nonzero coefficient, and the remaining coordinate has at most one possible value. Finitely many such translates cannot cover all $(N+1)^d$ points for arbitrarily large $N$.

For a period set $P$, let $P_0$ consist of the periods $t_i$ for which some $n \in\mathbb{Z}_P$ has $n_i > 0$. These are the periods that occur in a nonnegative combination with image zero. Put

Here $\mathcal{M}, \Gamma\subseteq\mathbb{Z}^d$, $L \leq\mathbb{Q}^d$, and $R \leq\mathbb{Q}^{2d}$. Both $\mathcal{M}$ and $\Gamma$ contain zero and are closed under addition.

Proof. For $t_i \in P_0$, choose $n \in\mathbb{Z}_P$ with $n_i > 0$. The relation $\sum_h n_h A t_h = 0$ gives

Every period with a positive coefficient on the right belongs to $P_0$. Thus the negative of each generator of $\Gamma$ belongs to $\Gamma$, which proves closure under negation. Also $\mathrm{A}(R) = \operatorname{span}\mathrm{A}(P_0) = L$. In every $P_n$ with $n \in\mathbb{Z}_P$, only periods in $P_0$ have positive coefficients, so $K_P \subseteq R$.

Since $\Gamma\subseteq\mathcal{M}$, adding or subtracting an element of $\Gamma$ preserves the image $Aa + \mathcal{M}$ of the linear component. These moves will turn a failure of separation into a point of $Aa + \mathcal{M}$ lying in a deleted subspace.

Two forms from the order of period supports

The support of a period $t$ is the set $\{i : t_i \ne0\}$ of positions of its nonzero coordinates. We next use the prohibition on alternating period supports to find $u,v$ with $V(u,v) \subseteq L$. The argument follows the structure of stratified period sets studied by Brough [7], Lemmas 3.6–3.7 and the proof of Proposition 3.8. We first record the graph property we need.

Proof. If $\{i,k\}$ is an edge with $i < k$, any other component meeting the open interval $(i,k)$ lies entirely inside that interval. Otherwise a path leaving the interval has an edge with one endpoint inside and one outside. Its endpoints are distinct from $i,k$, so the two edges have alternating endpoints.

Suppose distinct components $C,D$ contain $a,c$ and $b,d$ with $a < b < c < d$. A path in $C$ from $a$ to $c$ has an edge $\{i,k\}$ with $i < b < k$, so $D \subseteq(i,k)$. A path in $D$ from $b$ to $d$ has an edge $\{j,\ell\}$ with $j < c < \ell$, so likewise $C \subseteq(j,\ell)$. But $i < j < \ell< k$, contradicting $i \in C$.

Proof. Let $\mathcal{H}$ be the space of coefficient vectors of rational linear forms on $\mathbb{Q}^{2d}$ that vanish on $R$. Since these forms vanish on $K_A$, every vector in $\mathcal{H}$ can be written as

Construct a graph on the source coordinate positions, with an edge for each two-element support of a spanning period. For a period $t$ supported on $\{i,j\}$, vanishing means

Along an edge one coefficient determines the other. On a connected component, all coefficients are therefore determined by any one of them. The space of restrictions of $w \in\mathcal{H}$ to a component therefore has dimension at most one. This holds for isolated vertices as well.

Restricting $w$ to one graph component and setting its other coefficients to zero preserves membership in $\mathcal{H}$, because each spanning period has support in a single component. Call the two positions $x_i^{+}, x_i^{-}$, or $y_i^{+}, y_i^{-}$, signed partners. If a coefficient can be nonzero in $\mathcal{H}$, its position and its signed partner must belong to the same component. Otherwise, choose $w \in\mathcal{H}$ nonzero at that position and restrict $w$ to that graph component; the resulting vector violates (23).

All positions in the two $x$ blocks whose coefficients can be nonzero belong to one component. Indeed, two indices $i < j$ in distinct components would put $x_i^{+}, x_i^{-}$ in one and $x_j^{+}, x_j^{-}$ in the other. These four positions alternate in the source order, contrary to Lemma B.4. The same holds for the $y$ blocks. Thus the possible vectors $\alpha$ span a space of dimension at most one, as do the possible vectors $\beta$.

If the space of possible $\alpha$ is nonzero, choose a form $u$ whose coefficient vector spans it; otherwise choose any nonzero form on $\mathbb{Q}^{r}$. Choose $v$ in the same way from the possible $\beta$. Every rational form on $\mathbb{Q}^{d}$ that vanishes on $\mathrm{A}(R)$, when composed with $A$, has a coefficient vector in $\mathcal{H}$. The form on $\mathbb{Q}^{d}$ can therefore be written as

and vanishes on $V(u,v)$. This implies $V(u,v) \subseteq\mathrm{A}(R)$: if a vector were outside $\mathrm{A}(R)$, extending a basis of $\mathrm{A}(R)$ would give a form vanishing there but not at that vector. ◀

A stratification supplies separating forms

For a component of a stratification with $K_P = K_A$, the preceding lemmas give forms with $V(u,v) \subseteq L$. If these forms fail to separate a rational pair $w \in Y$ from $D_i$, then $w \in D_i + L$. To turn the $L$ contribution into an element of $\Gamma$ that can be subtracted within the component’s image, we clear denominators simultaneously for all candidate components before applying Lemma B.2 to select one representing the scaled pair.

Proof. Fix a stratification $S = \bigcup_{j=1}^{t}(a_j + P_j^{*})$, and let

For each $j \in J$, use the notation $\mathcal{M}_j, \Gamma_j, L_j, R_j$ defined above. Lemma B.3 gives $K_A \subseteq R_j$ and $\mathrm{A}(R_j) = L_j$. Since the periods spanning $R_j$ are a subset of $P_j$, they are stratified. Lemma B.5 supplies nonzero rational forms $u_j, v_j$ with

We show that these finitely many separators separate all of $Y$.

Fix $w \in Y$. For every index combination $(j,i)$ with $j \in J$ and $w \in L_j + D_i$, choose an expression

Such expressions exist because $L_j = \operatorname{span}\Gamma_j$. The fiber lemma will select a component only after we fix an integer multiple of $w$, so we clear denominators simultaneously for every candidate component. Choose one positive integer $N$ clearing the denominators of the coordinates of $w$ and all the coefficients $c_{jih}$. As $\Gamma_j$ is closed under addition and negation, while $D_i$ is a subspace, we obtain

Also $Nw \in Y \cap\mathbb{Z}^d$, since multiplication by a nonzero scalar preserves membership in each $D_i$ and its complement. Lemma B.2 gives $j \in J$ with $Nw \in A_{a_j} + M_j$. If $w \in L_j + D_i$, equation (25) gives $Nw = h + d'$ for $h \in\Gamma_j$ and $d' \in D_i$. Since $-h \in\Gamma_j \subseteq M_j$,

contradicting $d' \in D_i$. Therefore $w \notin L_j + D_i$ for every $i$. By (24), $w \in Y_{u_j,v_j}$, which proves the claim. ◀

Separating forms supply a stratification

For a source vector $\boldsymbol{n} = (x^+,x^-,y^+,y^-)$ and a fixed separator $u \times v$, membership of $A\boldsymbol{n}$ in $Y_{u,v}$ depends on the two sums $u(x^+ - x^-)$ and $v(y^+ - y^-)$. After clearing the coefficient denominators of $u,v$, these are integer-weighted sums over consecutive coordinate blocks. The following lemma proves that a Presburger condition on two such sums gives a context-free letter-bounded language.

For the reverse inclusion, cut a word when its balance first reaches $\epsilon$, then $2\epsilon$, and so on up to $n\epsilon$. Each intervening piece has balance $\epsilon$; append the remaining balanced suffix to the last piece. The case $n = 0$ is immediate. The same first-passage argument gives the descriptions of $B_1$ and $B_{-1}$ above.

Insert new marker letters $\#_1,\#_2$ before the two count blocks: add the start production $X_0 \to\#_1X$ and replace the terminal production by $X \to a^{c_1}\#_2b^{c_2}$. Use two disjoint copies of the signed alphabet. Substitute $B_0$ for each marker, $B_{\epsilon_1}$ for $a$, and $B_{\epsilon_2}$ for $b$, where $\epsilon_1,\epsilon_2$ are the chosen signs. By (26), the resulting language consists exactly of concatenations of a word over the first signed alphabet and a word over the second, whose balance pair is $(\epsilon_1n,\epsilon_2m)$ for some $(n,m)$ in the selected linear component. Take the union over components and coordinate-sign regions. Finally, for nonzero weights, map each $a_i$ to $|h_i|$ copies of the sign of $h_i$ in the first alphabet, and each $b_j$ to $|k_j|$ copies of the sign of $k_j$ in the second. Map each letter of weight zero to the empty word. Take the inverse image under this homomorphism and intersect it with the regular language $a_1^*\cdots a_s^*b_1^*\cdots b_t^*$. This is the required language. These constructions use closure of context-free languages under concatenation, finite union, substitution of context-free languages for letters, inverse homomorphism, and intersection with a regular language [8 Sections 3.4, 6.4, and 6.5]. ◀

Proof of Lemma 5.2. Multiplying each form by a positive integer to clear its coefficient denominators preserves separation: it applies the same invertible coordinate map to the image of each pair and each subspace. Membership in $S_{u,v}$ is therefore a Presburger condition on the two integer-weighted sums

The pair of sums must lie outside $\bigcup_i (u \times v)(D_i)$, a union of rational subspaces of $\mathbb{Q}^2$ defined by linear equations. All $\boldsymbol{x}$ positions precede all $\boldsymbol{y}$ positions. Lemma B.7 therefore shows that the associated letter-bounded language is context-free. Theorem 3.1 therefore makes $S_{u,v}$ stratifiable. Finite unions preserve stratifiability. ◀