Punctured point spectrum of a four-regular bipartite Cayley graph

Let \(G=\langle a,t\mid a^3=t^2=1\rangle\) and \(S=\{a^ita^j:1\le i,j\le2\}\). The Cayley graph \(\Gamma=\operatorname{Cay}(G,S)\) is infinite, connected, simple, four-regular, bipartite and vertex-transitive. Its adjacency operator on \(\mathbb C^G\) has point spectrum exactly \(\mathbb C\setminus\{0\}\). We give its inverse as a sum of nine translations and construct an eigenfunction for every nonzero complex number using two-dimensional representations of \(G\). In particular, \(\Gamma\) answers Kourovka Problem 15.89 negatively. The graph properties, inverse and complete point-spectrum statement are formalised in Lean 4.