Exact Sturm bisection isolates every distinct real root of a nonzero rational polynomial

Clearing denominators and dividing by the nonzero integer content preserves every root and its multiplicity. By [F1], the active squarefree product has exactly the distinct roots of $p$, and its factors assign each such root its unique multiplicity label.

If the initial squarefree polynomial has degree at least two, the coefficient-height bound in [F3] places every root strictly inside $(-B,B)$ because $B=H+2>H+1$. In degree one, write $S(x)=a_{1}x+a_0$ with nonzero integer $a_1$. Its unique root is $-a_0\mathrm{/}{a}_1$, whose absolute value is at most $\mathrm{\mid }{a}_0\mathrm{\mid }\le H<B$ since $\mathrm{\mid }{a}_1\mathrm{\mid }\ge 1$. Thus the initial endpoints are nonroots in either case. Bisection endpoints are midpoints tested exactly: a root midpoint is recorded and removed before its open halves are queued, while a nonroot midpoint leaves both endpoints nonroots for the active product.

In each queued interval with nonroot endpoints, [F2] makes the computed variation difference exactly its number of active roots. A zero count safely discards the interval. A count of one gives an isolating interval; the Sturm counts of the pairwise coprime $Q_k$ identify exactly one factor and hence the multiplicity label. If a midpoint is a root, exact division by $x-m$ removes it from that factor and the singleton record carries its multiplicity; otherwise the two open halves partition the parent interval. If removal leaves a nonzero constant active product, it has no remaining roots; the immediate complete-return branch safely clears the root-free queue without requesting another Sturm sequence.

Whenever an interval has at least two distinct active roots, their separation [F3] forces its width to be at least $\sigma$. At bisection depth $n$ the width is $2B(1\mathrm{/}2{)}^n$. Since $(1\mathrm{/}2{)}^n\to 0$ by [F4], some finite depth has width below $\sigma \mathrm{/}4$; such an interval cannot still contain two roots, so each branch stops with count zero or one. The branching factor is at most two and the depth is bounded, so the entire queue tree is finite. For degree one, the initial Sturm count is already zero or one. An earlier constant-active-product branch terminates immediately and cannot prolong the queue tree.

At each split, the roots in the parent are partitioned between the open children and, when the midpoint is a root, its exact singleton; a nonroot midpoint contributes no root. Every discarded interval is root-free, and every one-root interval is emitted once. The finite tree therefore accounts for every real root exactly once with the correct multiplicity.