Proof of Theorem 6 — with $s=\lceil\log_2(2\pi/\Delta)\rceil$, every phase $\theta\in[\Delta/2,\pi-\Delta/2]$ has $|\langle0^s|\omega\rangle|\le1/2$

Let $0<\Delta\le\pi$ and $s=\lceil\log_2(2\pi/\Delta)\rceil$. For every $\theta$ with $\Delta/2\le\theta\le\pi-\Delta/2$,

By Theorem 5, the left side is the amplitude on $|0^s\rangle$ after phase estimation of an eigenvector with eigenvalue $e^{2i\theta}$. The range of $\theta$ covers the eigenvalues $e^{2i\theta}$ and $e^{-2i\theta}=e^{2i(\pi-\theta)}$ with $\Delta(P)/2\le\theta<\pi/2$ and also the eigenvalue $-1$ ($\theta=\pi/2$), which are the eigenvalues of $W(P)$ on the part of $\mathcal A+\mathcal B$ orthogonal to $|\pi\rangle$. This is the single-copy step of the proof of Theorem 6.

Formalization Note The paper's sentence lists only $\Delta(P)/2\le\theta<\pi/2$ and the phases $e^{\pm2i\theta}$; the eigenvalue $-1$, which Theorem 4 part 3 allows on $\mathcal A+\mathcal B$, is included here. $\lceil\cdot\rceil$ is Nat.ceil, $\log_2$ is Real.logb 2.