Budgeted range evaluation terminates and certifies only sound enclosures

The initial admission checks terminate: the format's subnormal index range, exponent range and significand ranges are finite, and each equality comparison of exact dyadics is decided by clearing powers of two and comparing integers. Their enumeration is exactly the selected representable set, so a passing endpoint test establishes membership, including for zero and subnormals. Invalid initial data stop before an evaluator call. For admitted data, every endpoint of the initial box belongs to that format. Inductively, a split enqueues children only after the exact midpoint passes the same membership test; all other endpoints are inherited from the parent. The DAG, output, constants, format and $N$ are unchanged. Hence every queued box satisfies the elementary evaluator's input conditions. Each such call terminates through its finite DAG, finite series, finite bisection and finite bin/cell/quadrant lists, or returns a specified failure. The membership guard also terminates and can stop immediately with inconclusive. There are at most $B$ admitted splits and therefore at most $2B+1$ processed boxes. Thus the entire procedure terminates, including every guard-stop branch.

Before a box is processed, the completed leaf boxes together with the queued boxes cover $X$. Removing a current box preserves this cover when that box is counted as the current unresolved parent. Completing it transfers it to the completed leaves; an admitted split replaces it by two closed children whose union is the parent by [L1]. A failed midpoint test retains the parent as unresolved and therefore discards no part of the cover. This proves the coverage invariant by induction. By step 1.1, each completed leaf was evaluated on admissible input. In its finite typed DAG, input and certified constant nodes contain their exact values. Induct in the evaluator's topological order: arithmetic nodes and square roots preserve pointwise enclosure by [L4], real elementary nodes do so by [L2], and complex exponential and principal-logarithm nodes do so by [L3]. Finiteness of the call means that all domain guards passed and all intermediate results are finite. Thus every designated output, including a purely arithmetic output, contains the exact range on that leaf. If the queue empties without an early return, all covering leaves are completed; their enclosure hull therefore contains the exact range on all of $X$. On an early return, the completed-leaf hull is not asserted to cover the unresolved parent or remaining queue.

A certified return occurs only after the queue is empty without an admission, evaluator, split-guard or budget stop, and after the completed-leaf hull passes the final global width test. Step 2.1 then proves enclosure of the whole range, and the exact width comparison proves the requested tolerance. A failed midpoint membership instead returns inconclusive with the completed-leaf hull, unresolved parent, remaining queue and actual guard status; that partial hull is not a full-domain certificate. The other non-finite, exhausted-budget, unsplittable-coordinate and failed global-width branches likewise make no tolerance-success claim. Thus the finite guard preserves the stated certified-range, coverage and failure conclusions.