We consider two decision problems for linear recurrence sequences (LRS)
over the integers, namely the Positivity Problem (are all terms of a given
LRS positive?) and the Ultimate Positivity Problem (are all but finitely
many terms of a given LRS positive?). We show decidability of both
problems for LRS of order 5 or less, and for simple LRS (i.e. whose
characteristic polynomial has no repeated roots) of order 9 or less. Our
results rely on on tools from Diophantine approximation, including Baker's
Theorem on linear forms in logarithms of algebraic numbers. By way of
hardness, we show that extending the decidability of either problem to LRS
of order 6 would entail major breakthroughs on Diophantine approximation
of transcendental numbers.
This is joint with work with Joel Ouaknine and Matt Daws.