## Formalized Name
Constructive Intermediate Value Theorem from Bisection Data
## Formalized Statement
Let $f:[a,b]\to\mathbb{R}$ be a uniformly continuous function on a located compact interval, with a displayed modulus of uniform continuity. Suppose there are nested rational intervals $[u_k,v_k]\subseteq[a,b]$ such that $u_k\le u_{k+1}\le v_{k+1}\le v_k$, $v_k-u_k\le 2^{-k}$, $f(u_k)\le 2^{-k}$, and $f(v_k)\ge -2^{-k}$ for every $k$. Then the midpoints of these intervals determine a Cauchy real $z\in[a,b]$ and $f(z)=0$.
## Proof
[proofplan]
Use the shrinking nested intervals to construct the point $z$. The interval lengths give a Cauchy modulus for the midpoint sequence. The approximate sign bounds at the endpoints, together with uniform continuity, force both $f(z)\le 0$ and $0\le f(z)$.
[/proofplan]
[step:Construct the candidate zero]
Let
\begin{align*}
m_k:=\frac{u_k+v_k}{2}.
\end{align*}
If $j\ge k$, then $m_j$ and $m_k$ both lie in $[u_k,v_k]$, because the intervals are nested. Hence
\begin{align*}
|m_j-m_k|\le v_k-u_k\le 2^{-k}.
\end{align*}
Thus $(m_k)$ is a Cauchy sequence with the displayed modulus, and it determines a Cauchy real $z$. Since each $m_k$ lies in $[a,b]$ and the interval is closed in the Cauchy-real presentation, $z\in[a,b]$.
[/step]
[step:Show that endpoint sequences converge to the same point]
For each $k$, the points $u_k$, $m_k$, and $v_k$ all lie in $[u_k,v_k]$. Therefore
\begin{align*}
|u_k-m_k|\le 2^{-k}
\end{align*}
and
\begin{align*}
|v_k-m_k|\le 2^{-k}.
\end{align*}
Since $m_k$ represents $z$, both endpoint sequences converge to the same real $z$.
[/step]
[step:Prove the upper bound on the value]
Let $\varepsilon>0$ be rational. Choose $k$ large enough that $2^{-k}<\varepsilon/2$ and the modulus of uniform continuity ensures
\begin{align*}
|x-y|\le 2^{-k}\quad\Longrightarrow\quad |f(x)-f(y)|<\varepsilon/2.
\end{align*}
Using $x=u_k$ and $y=z$, the previous step gives $|u_k-z|\le 2^{-k}$, so
\begin{align*}
f(z)\le f(u_k)+\varepsilon/2\le 2^{-k}+\varepsilon/2<\varepsilon.
\end{align*}
Since this holds for every positive rational $\varepsilon$, $f(z)\le 0$.
[/step]
[step:Prove the lower bound on the value]
With the same choice of $k$, use $x=v_k$ and $y=z$. The previous step gives $|v_k-z|\le 2^{-k}$, so uniform continuity gives
\begin{align*}
f(z)\ge f(v_k)-\varepsilon/2\ge -2^{-k}-\varepsilon/2>-\varepsilon.
\end{align*}
Since this holds for every positive rational $\varepsilon$, $0\le f(z)$.
[/step]
[step:Conclude that the value is zero]
The two inequalities $f(z)\le 0$ and $0\le f(z)$ give $f(z)=0$. The constructed Cauchy real $z$ lies in $[a,b]$, so $z$ is the required zero.
[/step]
[step:Summarize the bisection argument]
The midpoint sequence is Cauchy because all later midpoints remain inside an earlier interval whose length is small. Uniform continuity transfers the endpoint sign estimates to the limit point, giving both inequalities needed for equality to zero.
[guided]
The midpoint sequence is Cauchy because all later midpoints remain inside an earlier interval whose length is small. Uniform continuity transfers the endpoint sign estimates to the limit point, giving both inequalities needed for equality to zero.
[/guided]
[/step]
