We prove Lang-Weil type bounds for the number of rational points of difference varieties over finite difference fields, in terms of the transformal dimension of the variety and assuming the existence of a smooth rational point. It follows that in (certain) non-principal ultraproducts of finite difference fields the coarse dimension of a quantifier free type equals its transformal transcendence degree.
The proof uses a strong form of the Lang-Weil estimates and, as key ingredient to obtain equidimensional Frobenius specializations, the recent work of Dor and Hrushovski on the non-standard Frobenius acting on an algebraically closed non-trivially valued field, in particular the pure stable embeddedness of the residue difference field in this context.
This is joint work with Ehud Hrushovski, Jinhe Ye and Tingxiang Zou.