Ultimate Positivity is Decidable for Simple Linear Recurrence Sequences

TL;DR

This paper proves that determining whether all but finitely many terms of a simple linear recurrence sequence are positive is decidable in polynomial space, with fixed order cases solvable in polynomial time, and establishes its complexity lower bounds.

Contribution

It introduces a polynomial-space decision procedure for the Ultimate Positivity Problem for simple LRS and provides complexity bounds, including fixed order polynomial-time algorithms and co∃R-hardness.

Findings

Decidability in polynomial space for simple LRS

Polynomial-time decision for fixed order simple LRS

Complexity lower bound: co∃R-hardness

Abstract

We consider the decidability and complexity of the Ultimate Positivity Problem, which asks whether all but finitely many terms of a given rational linear recurrence sequence (LRS) are positive. Using lower bounds in Diophantine approximation concerning sums of S-units, we show that for simple LRS (those whose characteristic polynomial has no repeated roots) the Ultimate Positivity Problem is decidable in polynomial space. If we restrict to simple LRS of a fixed order then we obtain a polynomial-time decision procedure. As a complexity lower bound we show that Ultimate Positivity for simple LRS is hard for co$\exists\mathbb{R}$, i.e., the class of problems solvable in the universal theory of the reals (which lies between coNP and PSPACE).