Return Probability for the Switch--Walk--Switch Lamplighter Walk on a Regular Tree

We derive the sharp return-probability asymptotic for the switch–walk–switch lamplighter walk with lamp group ${\mathbb{Z}}_2$ over the infinite $d$-regular tree: $$p_{2n}(e,e)={\rho }_d^{2n}\exp [-({\pi }^2(\log (d-1){)}^2+o(1))\frac{n}{{\log }^{2}n}]\mathrm{.}$$ The proofs were generated by QED, a multi-agent system co-developed by the authors, without human intervention beyond the specification of the problem. This provides a test case for the ability of AI systems to produce rigorous mathematical proofs.