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

TL;DR

This paper proves that the problem of deciding properties of univariate real algebra involving predicates for rational and integer powers is decidable, using a novel combination of algebraic and number-theoretic techniques.

Contribution

It introduces a decision procedure for univariate real algebra with predicates for rational and integer powers, combining algebraic cell computation with number theory.

Findings

Decidability of univariate real algebra with power predicates established.

Decision procedure effectively combines algebraic and number-theoretic methods.

Framework applicable to related algebraic decision problems.

Abstract

We prove decidability of univariate real algebra extended with predicates for rational and integer powers, i.e., $(x^n \in \mathbb{Q})$ and $(x^n \in \mathbb{Z})$. Our decision procedure combines computation over real algebraic cells with the rational root theorem and witness construction via algebraic number density arguments.