A budgeted polynomial Remez exchange terminates within its finite cap

At the start of each iteration the reference is ordered and distinct: it is so initially, and each permitted replacement preserves strict order. For an interior index the new node lies strictly between its neighboring reference nodes; at index $0$ it satisfies $a\le y<x_1$, and at index $n+1$ it satisfies $x_n<y\le b$, so endpoint equality still leaves all reference nodes distinct and ordered. Therefore [F2] supplies a unique solve on every entered iteration, and the termination hypothesis together with [F1] gives a terminating oracle call or one reference update.

The loop indices are exactly $0,\dots ,B$, a finite set of $B+1$ iterations. Each entered iteration makes one linear solve and at most one oracle call, so there are at most $B+1$ solves and $B+1$ oracle calls in total. Each iteration returns or advances once, so after at most $B+1$ iterations the procedure either has returned earlier or returns budget-exhausted.