On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number

Abstract

This paper investigates $\exists\mathbb{R}(r^{\mathbb{Z}})$, that is the extension of the existential theory of the reals by an additional unary predicate $r^{\mathbb{Z}}$ for the integer powers of a fixed computable real number $r > 0$. If all we have access to is a Turing machine computing $r$, it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when: 1. $r$ is known to be transcendental, or 2. $r$ is a root of some given integer polynomial (that is, $r$ is algebraic). In other words, knowing the algebraicity of $r$ suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that $r$ enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of $\exists\mathbb{R}(r^{\mathbb{Z}})$ is 1. in NEXPTIME if $r$ is a natural number, 2. in EXPSPACE if $r$ is an algebraic number, and 3. in 3EXP if $r$ belongs to a family of transcendental numbers including $π$ and Euler's $e$. As a by-product of our results, we are able to remove the appeal to Schanuel's conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS'23]: when the base of the entropic risk is Euler's $e$ and the aversion factor is a fixed algebraic number, the problem is in EXP.