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 $\pi$ 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.

翻译：本文研究$\exists\mathbb{R}(r^{\mathbb{Z}})$，即通过添加表示固定可计算实数$r > 0$整数幂的一元谓词$r^{\mathbb{Z}}$所扩展的实数存在性理论。若仅能访问计算$r$的图灵机，则无法判定该理论中任意输入公式的可满足性。然而，我们证明在以下情形存在判定该问题的算法：1. $r$已知为超越数；2. $r$为给定整数多项式的根（即$r$为代数数）。换言之，掌握$r$的代数性足以规避不可判定性。进一步地，我们在$r$满足所谓多项式根屏障的条件下建立了复杂度结果。运用此概念，我们证明$\exists\mathbb{R}(r^{\mathbb{Z}})$的可满足性问题：1. 当$r$为自然数时属于NEXPTIME；2. 当$r$为代数数时属于EXPSPACE；3. 当$r$属于包含$\pi$和欧拉数$e$的超越数族时属于3EXP。作为本研究的副产品，我们能够从具有有理概率、奖励与阈值的随机博弈的熵风险阈值问题可判定性证明中移除对沙努尔猜想的依赖[Baier等人，MFCS'23]：当熵风险基数为欧拉数$e$且风险厌恶因子为固定代数数时，该问题属于EXP。