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

Automated Proof (or Disproof) of Linear Recurrences Satisfied by Pisot Sequences
By Shalosh B. Ekhad, N. J. A. Sloane and Doron Zeilberger
.pdf .ps .tex

(Exclusively published in the Personal Journal of Shalosh B. Ekhad and Doron Zeilberger, Neil Sloane's website, and arxiv.org )
Written: Sept. 18, 2016

Dedicated to Richard K. Guy (b. 30 Sept., 1916) on his (100-ε)-th birthday

As far as I know, Richard Guy is the longest-living mathematician of all time (in the sense of Paul Erdős, where you die when you stop doing math), since at almost one hundred years of age, he keeps producing great new math. This tribute, joint with Neil Sloane, is dedicated to him. Keep up the good work, Richard!

Added Sept. 21, 2016: Tomas Oliveira e Silva sent us many more dramatic instances of Pisot sequences that satisfy linear recurrences that break down after a VERY long time, and he kindly permitted us to post it here .

Added Oct. 6, 2016: Tomas Oliveira e Silva sent us even more dramatic instances of Pisot sequences that satisfy linear recurrences that break down after a VERY long time, and he kindly permitted us to post it here .

Added Oct. 5, 2016: Here is Richard Guy's response to this paper that has been dedicated to him.
Dear Neil & Doron,
What a magnificent present! Sorry I haven't replied earlier. But I haven't replied to the Queen, nor the Lieutenant-Governor, nor Justin Trudeau, either! All the best! R.

Added Nov. 10, 2016: Tomas Oliveira e Silva broke yet another record the linear recurrence with a₀=605, a₁=36312, and with r=1/2, fails for a_13138671

Added Sept. 25, 2017: Robert Dougherty-Bliss, wrote a Python version, and here is the documentation.

Maple package

Pisot.txt, a Maple package to discover, prove, and disprove, linear recurrence relations satisfied by Pisot sequences, first discovered and discussed by David Boyd, D.G. Cantor, and his student P. Galyean.

Sample Input and Output Files for the Maple package Pisot.txt

If you want to see linear recurrences, with COMPLETE proofs of Pisot sequenes of the form PISOT(a,b) (with parameter 1/2) for 2<=a<20, and a+2<=b<40
the input file generates the output file.

If you want to see PROVED linear recurrences, (w/o proofs, to save disk-space) of Pisot sequenes of the form PISOT(a,b) (with parameter 1/2) for 2<=a<30, and a+2<=b<600
the input file generates the output file.

If you want to see PROVED linear recurrences, (w/o proofs, to save disk-space) of Pisot sequenes of the form PISOT(a,b) (with parameter 1/2) for 2<=a<40, and a+2<=b<1000
the input file generates the output file.

If you want to see a detailed, fully rigorous proof that the Pisot Sequence E(4,7), alias OEIS sequence A010901 does indeed satisfy (for ALL n, not just ≤ 50000) the recurrence
a(n) = 2a(n-1) - a(n-2) + a(n-3)
the input file generates the output file.

If you want to see several examples of Generalized Pisot sequences that satisfy linear recurrences, along with their terse proofs
the input file generates the output file.

If you want to see many infinite families of Pisot sequenes that satisfy linear recurrences
the input file generates the output file.

If you want to see the same output, but in TeX
the input file generates the output file.

Personal Journal of Shalosh B. Ekhad and Doron Zeilberger
Doron Zeilberger's Home Page