The Bellaterra graphs are Ramanujan

The Bellaterra automaton gives three involutions of every set of binary words of a fixed length. We identify their Schreier graph at level $n$ with a cubic arithmetic graph over \Q(\sqrt{17}), and prove that every nonconstant adjacency eigenvalue satisfies the Ramanujan bound. In particular, this proves Malyshev-Pak's Conjecture that the Bellaterra graphs form a family of two-sided expanders.