Phase retrieval from a uniformly discrete point set

We prove that for every window $w$ of the form $w(x)=e^{-\pi \mathrm{\mid }x{\mathrm{\mid }}^2}h(x)$, where $h$ is a polynomial, there exists a uniformly discrete set of points $\mathcal{S}\subset {\mathbb{R}}^{2d}$ such that the magnitude of the short-time Fourier transform $V_{w}f$ on $\mathcal{S}$ determines every $f\in L^2({\mathbb{R}}^d)$ up to a constant phase factor. The separation distance can be chosen independent of the degree of $h$ and proportional to the square root of the dimension. The proof combines a discrete norming inequality, based on a multidimensional Remez inequality and VC-dimension bounds, with tail estimates for the reproducing kernel. A formalization of our main result in Lean 4 is also provided.