= Solution
Maintain that all positive $h<\mathrm{lo}$ fail $rh^2\geq i^2$, while `hi` satisfies that inequality; its least satisfying integer lies in $[\mathrm{lo},\mathrm{hi}]$. Monotonicity of $rk^2$ in positive $k$ validates both updates. At exit the endpoints agree and identify exactly that least integer.
The <loop variant> `hi-lo` decreases on every iteration and is at least halved up to rounding. Starting with at most $i$ candidates therefore needs \b[$O(\log(i+1))$ arithmetic operations], conventionally $O(\log i)$ for $i\geq2$. For $i=1$ the loop is empty. The final upper-bound check proves the returned Boolean is the required membership answer.
Back to article page
