Automated Proof (or Disproof) of Linear Recurrences Satisfied by Pisot Sequences

TL;DR

This paper introduces an algorithm and Maple implementation to determine whether linear recurrences hold for all terms of Pisot sequences, addressing cases where initial validity does not extend indefinitely, and explores higher-order analogs.

Contribution

The paper presents a decision algorithm for verifying the universal validity of linear recurrences in Pisot sequences, including implementation details and analysis of failure cases.

Findings

Algorithm effectively distinguishes true from false recurrences.

Failures can occur after thousands of valid initial terms.

Higher-order Pisot analogs exhibit similar phenomena, less frequently.

Abstract

Pisot sequences (sequences $a_n$ with initial terms $a_0=x, a_1=y$, and defined for $n>1$ by $a_n= \lfloor a_{n-1}^2/a_{n-2} + \frac{1}{2} \rfloor$) often satisfy linear recurrences with constant coefficients that are valid for all $n \geq 0$, but there are also cautionary examples where there is a linear recurrence that is valid for an initial range of values of $n$ but fails to be satisfied beyond that point, providing further illustrations of Richard Guy's celebrated "Strong Law of Small Numbers". In this paper we present a decision algorithm, fully implemented in an accompanying Maple program ({\tt Pisot.txt}), that first searches for a putative linear recurrence and then decides whether or not it holds for all values of $n$. We also explain why the failures happen (in some cases the `fake' linear recurrence may be valid for thousands of terms). We conclude by defining, and studying, higher-order analogs of Pisot sequences, and point out that similar phenomena occur there, albeit far less frequently. This article is dedicated to Richard K. Guy (b. Sept. 30, 1916) on his 100th birthday.