Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers

We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., "x(n) is an element of Q" and "x(n) is an element of Z." Our decision procedure combines computation over real algebraic cells with the rational root theorem and witness construction via algebraic number density arguments.