A positive constraint-separation margin permits finite certified empty-box detection

Define $h(x)={\max }_{1\le i\le m}{g}_i(x)$. This maximum exists and is one of the $m$ values by [F3]. For any $x,y\in D_0$, $\mathrm{\mid }h(x)-h(y)\mathrm{\mid }\le {\max }_i\mathrm{\mid }{g}_i(x)-g_i(y)\mathrm{\mid }$; the right-hand side tends to zero as $y\to x$ because there are finitely many continuous $g_i$. Thus $h$ is continuous.

The box $D_0$ is nonempty and compact by [F1]. Hence $h[D_0]$ is nonempty and compact by [F2], and therefore closed and bounded. By the boundedness definition and [F6], there are $c\in \mathbb{R}$ and $r>0$ such that $h[D_0]\subseteq (c-r,c+r)$, so $c-r$ is a lower bound. Let ${\delta }_{\ast }=\inf h[D_0]$, which exists by [F4]. For every $\eta >0$, [F4] gives $y\in h[D_0]$ with ${\delta }_{\ast }\le y<{\delta }_{\ast }+\eta$; by [F6] every open ball around ${\delta }_{\ast }$ meets $h[D_0]$. Thus ${\delta }_{\ast }\in \overline{h[D_0]}$ by [F5], and closedness gives ${\delta }_{\ast }\in h[D_0]$. So $h$ attains its minimum ${\delta }_{\ast }$ on $D_0$.

Suppose the unlimited procedure split infinitely many boxes. The split tree is binary and finitely branching, so it has an infinite nested branch: at each node choose its first child with infinitely many split descendants, if one exists, and otherwise its second child. This rule is deterministic. Along this branch, longest-side bisection makes every coordinate width tend to zero: for any $\eta >0$, each coordinate can be halved while its width is at least $\eta$ only finitely many times, and each split of a box with maximum width at least $\eta$ halves one such longest coordinate. Hence all coordinate widths, and the box diameters, tend to zero. The nested interval property gives a unique point $x$ in the intersection of the branch boxes.

If $C=\mathrm{\varnothing }$, then every $x\in D_0$ has some $g_i(x)>0$, so $h(x)>0$. Since $h$ attains its minimum, ${\delta }_{\ast }=h(x_{\ast })>0$ at a minimizing point $x_{\ast }$. This is the required uniform margin and proves the converse.

By the margin hypothesis and [F3], choose an index $i$ with $g_i(x)=h(x)\ge \delta$. The interval soundness and consistency result [F8], under the valid-DAG and precision hypotheses [A1], gives ${\mathrm{\ell }}_i(B_k)\to g_i(x)$ along the branch. Thus for some finite $k$ the lower bound is positive. The procedure would then certify $B_k$ empty and would not generate its branch child, contradicting the infinite branch.

The finite split tree has finitely many generated leaves. Every unpruned positive-width leaf is split by [F7], so any remaining unpruned leaf is a singleton. At such a point $x$, the margin gives some $g_i(x)\ge \delta$ by [F3]; repeated singleton queries use strictly increasing precision by the schedule in Certified constraint-emptiness search with a finite query budget. Their lower bounds converge to this value by [A1] and [F8], so after finitely many singleton queries one is positive. Every leaf is therefore certified empty after finitely many finite-time oracle calls. The queue empties, and the certified-empty leaf cover of $D_0$ proves infeasibility.

Let $K$ be the finite total number of oracle calls established in step 3.1. A budget of at least $K$ does not exhaust before the queue empties, so Certified constraint-emptiness search with a finite query budget returns the same infeasibility certificate; a smaller budget may return only its explicit budget-exhausted status.