Rational polynomial solvability reduces to stratifiability of semilinear sets

A semilinear set is stratifiable if it is a finite union of linear sets whose periods have at most two nonzero coordinates, with no two periods in one component connecting alternating pairs of coordinates. We give a computable many-one reduction from the existence of a rational zero of an integer polynomial to deciding stratifiability. After the classical reduction to quadratic systems, we reduce rational solvability of these systems to a problem we call finite separation by Cartesian products of rational linear forms. Its input consists of rational subspaces $D_1,\dots ,D_k\le {\mathbb{Q}}^r\times {\mathbb{Q}}^r$. A separator is a map $(\mathit{x},\mathit{y})\mapsto (u(\mathit{x}),v(\mathit{y}))$, where $u,v\text{\hspace{0.17em}⁣}:{\mathbb{Q}}^r\to \mathbb{Q}$ are nonzero rational linear forms. The problem asks whether finitely many separators suffice so that every pair outside ${\bigcup }_i{D}_i$ receives, from some separator, a value attained at no pair in that union. We then reduce this problem to stratifiability. Ginsburg and Spanier’s characterization of letter-bounded context-free languages} also induces a reduction from rational polynomial solvability to context-freeness of letter-bounded languages specified by semilinear exponent sets. An OpenAI preprint claims undecidability of rational polynomial solvability; if correct, our result settles the decidability of general stratifiability, a problem open since 1966.