Hilbert's tenth problem for systems of diagonal quadratic forms, and Büchi's problem

In this paper we complete Büchi’s proof that there is no decision algorithm for the solubility in integers of arbitrary systems of diagonal quadratic form equations, by proving the assertion that whenever $x_1^2,\cdots ,x_5^2$ are five squares such that the second differences satisfy $$x_{k+2}^2-2x_{k+1}^2+x_k^2=2$$ for $k=1,2,3$, then they must be consecutive. This answers a question of J.~Richard~Büchi.