above verification and compute the bounds rigorously, as well as the code for setting up the semidefinite programs, using a custom semidefinite programming specification library.

Proof of Theorem \[thmpaircorreltation\]
----------------------------------------

To obtain the first part of Theorem \[thmpaircorreltation\] from Theorem \[thmsmallgapszerosofxi\] we need to minimize the function ${\mathcal{P}}$ over the space $\mathcal A_{LP}$. We can formulate this as a bilevel optimization problem in which we optimize over $R \geq 1$ in the outer problem. In the inner problem we perform a binary search over $\Lambda$ to find the smallest $\Lambda$ for which there exists a function $f \in \mathcal A_{LP}(d)$ that satisfies $f(R) = 0$, $f(x) \leq 0$ for $|x| \geq R$, and $p_f(\Lambda) \geq 0$.

To get a bound whose correctness we can verify rigorously we replace the constraints $f(0)=1$, ${\widehat}f(0) = 1$, and $p_f(\Lambda) \geq 0$ by $f(0) = 1-10^{-10}$, ${\widehat}f(0) = 1+10^{-10}$, and $p_f(\Lambda) \geq 10^{-10}$. We then use the above optimization approach to find good values for $R$ and $\Lambda$. We then add $10^{-6}$ to $\Lambda$ and solve the feasibility problem again to get the strictly feasible matrices $X_2,X_3$, and $X_4$. By performing the same procedure as in \[sec:rig\] we can verify that the Fourier transform 