Iteration count: $r(N) = \lfloor \pi/(4\arcsin(1/\sqrt N))\rfloor \le \lceil \frac{\pi}{4}\sqrt N\rceil$

Let $N \ge 1$ and $t = \arcsin(1/\sqrt N)$. The number of Grover iterations $r(N) = \lfloor \pi/(4t)\rfloor$ satisfies

Together with the error bound for this choice of $r$ (milestone Algebraic proof — stopping at $r = \lfloor\pi/(4t)\rfloor$), this is the source's statement that the correctly chosen number of iterations is at most $\lceil\frac{\pi}{4}\sqrt N\rceil$, i.e. $O(\sqrt N)$ applications of the oracle.

Formalization Note The source does not fix a rounding convention for "$r = \pi/4t$"; the mission uses the integer part $\lfloor\pi/(4t)\rfloor$.