Punctured point spectrum of a four-regular bipartite Cayley graph

Let \(G= a,t a^3=t^2=1\) and \(S=\{a^ita^j:1≤ i,j≤2\}\). The Cayley graph \(Γ=Cay(G,S)\) is infinite, connected, simple, four-regular, bipartite and vertex-transitive. Its adjacency operator on \( C^G\) has point spectrum exactly \( C\{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, \(Γ\) answers Kourovka Problem 15.89 negatively. The graph properties, inverse and complete point-spectrum statement are formalised in Lean 4.