皮索特序列所满足线性递推的自动证明（或证伪）

皮索特序列（序列 $a_n$ 初项为 $a_0=x, a_1=y$，且对 $n>1$ 定义为 $a_n= \lfloor a_{n-1}^2/a_{n-2} + \frac{1}{2} \rfloor$）通常满足对所有 $n \geq 0$ 都成立的常系数线性递推，但也存在警示性例子：某个线性递推在 $n$ 的初始值范围内成立，但超出该点后不再满足，这进一步说明了理查德·盖伊著名的“小数定律”。在本文中，我们提出了一个决策算法，该算法在随附的 Maple 程序（{\tt Pisot.txt}）中完整实现，它先搜索假定的线性递推，然后判定其是否对所有 $n$ 值成立。我们还解释了失败发生的原因（在某些情况下，‘伪’线性递推可能对数千项都成立）。最后，我们定义并研究了皮索特序列的高阶类比，指出类似现象虽发生频率低得多，但依然存在。本文献给理查德·K·盖伊（生于1916年9月30日）以庆祝其百岁寿辰。