Gevrey regularity for the formally linearizable billiard of Treschev

Treschev made the remarkable discovery that there exists formal power series describing a billiard with locally linearizable dynamics. We show that if the frequency for the linear dynamics is Diophanine, the Treschev example is $(1+ \alpha)$-Gevrey for some $\alpha > 0$. Our proof is based on an iterative scheme that further clarifies the structure and symmetries underlying the original Treschev construction. Hopefully, Our result sheds a light on the more important question of whether this example is convergent.