[proofplan]
Run rational bisection while maintaining endpoints $l_r\leq u_r$ with $f(l_r)\leq 0\leq f(u_r)$. At each midpoint, the approximate sign procedure either directly gives a point where $|f|<2^{-N}$, or supplies a sign that chooses the next half interval. Stop once the interval length is at most $2^{-\mu(N)}$. [Uniform continuity](/page/Uniform%20Continuity) then shows $|f(u_r)-f(l_r)|\leq 2^{-N}$, and the opposite endpoint signs imply both endpoint values have absolute value at most $2^{-N}$.
[/proofplan]
[step:Initialize the bisection invariant]
Set $l_0=a$ and $u_0=b$. These are rational points of $[a,b]$, and the endpoint hypothesis gives
\begin{align*}
f(l_0)\leq 0\leq f(u_0).
\end{align*}
Thus the interval $[l_0,u_0]$ satisfies the invariant: its endpoints are rational, lie in $[a,b]$, and have opposite weak signs.
[guided]
The initial interval is $[a,b]$. Since $a<b$ are rational, both endpoints are rational. With $l_0=a$ and $u_0=b$, the hypothesis $f(a)\leq 0\leq f(b)$ becomes $f(l_0)\leq 0\leq f(u_0)$, which is exactly the sign invariant needed for bisection.
[/guided]
[/step]
[step:Perform one constructive bisection step]
Suppose $[l_r,u_r]$ satisfies the invariant. Let
\begin{align*}
q_r=\frac{l_r+u_r}{2}.
\end{align*}
Apply the approximate sign procedure to $q_r$ with precision $N+1$. If it returns $|f(q_r)|<2^{-(N+1)}$, stop and output $x_N=q_r$.
If it returns $f(q_r)\leq 0$, set $l_{r+1}=q_r$ and $u_{r+1}=u_r$. If it returns $0\leq f(q_r)$, set $l_{r+1}=l_r$ and $u_{r+1}=q_r$. In either sign case, the new endpoints are rational points of $[a,b]$, the weak sign invariant is preserved, and the interval length is halved.
[guided]
At stage $r$, the midpoint $q_r=(l_r+u_r)/2$ is rational. The sign procedure gives one of three certificates. A near-zero certificate $|f(q_r)|<2^{-(N+1)}$ already implies the target bound. A certificate $f(q_r)\leq 0$ lets us keep the right endpoint $u_r$ and replace the left endpoint by $q_r$. A certificate $0\leq f(q_r)$ lets us keep the left endpoint $l_r$ and replace the right endpoint by $q_r$. In both sign cases, the new interval has rational endpoints, keeps $f(l_{r+1})\leq 0\leq f(u_{r+1})$, and has half the previous length.
[/guided]
[/step]
[step:Choose a modulus-controlled stopping time]
If the construction has not already stopped with a near-zero midpoint, repeat the sign-case bisection step for $K$ stages, where $K$ is chosen so that
\begin{align*}
\frac{b-a}{2^K}\leq 2^{-\mu(N)}.
\end{align*}
Then the final interval $[l_K,u_K]$ satisfies
\begin{align*}
|u_K-l_K|\leq 2^{-\mu(N)}
\end{align*}
and still has $f(l_K)\leq 0\leq f(u_K)$.
[guided]
Choose $K$ large enough that $(b-a)/2^K\leq 2^{-\mu(N)}$. Each non-stopping bisection halves the interval length, so after $K$ such steps we have $|u_K-l_K|\leq 2^{-\mu(N)}$. The invariant from the previous step is preserved at every stage, hence $f(l_K)\leq 0\leq f(u_K)$ remains true.
[/guided]
[/step]
[step:Extract a small value from the final bracket]
By the modulus of uniform continuity and the bound on the final interval length,
\begin{align*}
|f(u_K)-f(l_K)|\leq 2^{-N}.
\end{align*}
Since $f(l_K)\leq 0\leq f(u_K)$, we have
\begin{align*}
|f(l_K)|=-f(l_K)\leq f(u_K)-f(l_K)\leq 2^{-N}.
\end{align*}
Thus, in the non-stopping case, $x_N=l_K$ is a rational point of $[a,b]$ with $|f(x_N)|\leq 2^{-N}$.
[guided]
The final endpoints are within $2^{-\mu(N)}$, so uniform continuity gives $|f(u_K)-f(l_K)|\leq 2^{-N}$. Because the signs satisfy $f(l_K)\leq 0\leq f(u_K)$, the difference $f(u_K)-f(l_K)$ is at least $-f(l_K)=|f(l_K)|$. Therefore $|f(l_K)|\leq 2^{-N}$, and the rational endpoint $l_K$ is an acceptable output.
[/guided]
[/step]
[step:Conclude the algorithmic intermediate value statement]
The procedure either stops early at a rational midpoint $q_r$ with $|f(q_r)|<2^{-(N+1)}\leq 2^{-N}$, or it reaches the final bracket and outputs $l_K$ with $|f(l_K)|\leq 2^{-N}$. In both cases it computes a rational $x_N\in[a,b]$ from the displayed data and satisfies $|f(x_N)|\leq 2^{-N}$.
[/step]
