Global optimization and certified branch and bound

Let $x\in [l_x,u_x]$ and $y\in [l_y,u_y]$, where all four endpoints are finite and ordered, and let $w$ be an additional real variable representing the product $xy$. The McCormick polytope for this box is the set of $(x,y,w)$ satisfying the box bounds and $w\ge l_{x}y+l_{y}x-l_x{l}_y,w\ge u_{x}y+u_{y}x-u_x{u}_y$ $w\le u_{x}y+l_{y}x-u_x{l}_y,w\le l_{x}y+u_{y}x-l_x{u}_y$ The term McCormick envelope will mean this polytope. Its exact relation to the convex hull of the product graph is established by the local bilinear-hull result.

A box in ${\mathbb{R}}^n$ is $D_0={\prod }_{j=1}^n[a_j,b_j]$ with finite real endpoints $a_j\le b_j$. Here $n\ge 1$. The box is closed and bounded, hence compact by Heine-Borel in ${\mathbb{R}}^n$: with the Euclidean metric a subset of ${\mathbb{R}}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line. An optimization instance on a compact box consists of this $D_0$, a continuous objective $f:D_0\to \mathbb{R}$ (continuity in the inherited Euclidean metric, as in Continuity of a map between metric spaces, at a point and globally, in the $\epsilon$-$\delta$ form), and a feasible set $C\subseteq D_0$. The unconstrained instance has $C=D_0$. A constrained instance may specify $C=\{x\in D_0:g_i(x)\le 0,1\le i\le m\}$ for a finite list of real functions $g_i$.

When $C\mathrm{\ne }\mathrm{\varnothing }$, the set $f[C]$ is nonempty and bounded below: $D_0$ is compact by Heine-Borel in ${\mathbb{R}}^n$: with the Euclidean metric a subset of ${\mathbb{R}}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, its continuous image $f[D_0]$ is compact in the usual metric on $\mathbb{R}$ by The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset and therefore bounded by A compact subset of a metric space is closed and bounded. Thus $f[D_0]$ lies in a real interval $(c-r,c+r)$ for some $c\in \mathbb{R}$ and $r>0$, by Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space and The absolute value makes $\mathbb{R}$ a metric space: $d(x,y)=\mathrm{\mid }x-y\mathrm{\mid }$ is a metric, its open balls are the intervals $(x-r,x+r)$, and it is unbounded; hence $c-r$ is a lower bound of $f[C]\subseteq f[D_0]$. Therefore Every nonempty set bounded below has an infimum gives the real number $f^{\ast }=\inf f[C]$, using Greatest lower bound (infimum). No attainment is assumed for a general $C$. Statements about finite empty-set detection require a separate constraint certificate or a stated separation margin; objective continuity alone does not certify infeasibility.

Let $n\ge 1$, let $K\in {\mathbb{R}}^{n\times n}$ be symmetric positive semidefinite, let ${\sigma }^2\ge 0$, and put $C=K+{\sigma }^{2}I$. If ${\sigma }^2>0$, then $C$ is symmetric positive definite, even when $K$ is singular. If ${\sigma }^2=0$, then $C$ is positive definite exactly when $K$ is positive definite; zero noise is not guaranteed to make the solve available.

Input a candidate list $X=(c_1,\dots ,c_M)$, a horizon $N$, an initial-list length $s$, a real-mean candidate $m$, a kernel candidate $k$, an observation-variance candidate ${\sigma }^2$, coefficients $(b_t{)}_{0\le t<N}$, an initial data list $(x_i,y_i{)}_{i=1}^s$, an observation oracle $O$, and a selector that is either the exact rule below or a certified approximate rule below. For $N=0$, the coefficient list is empty. First validate that $X$ is nonempty, finite, and ordered; $N$ and $s$ are integers with $N\ge 0$ and $0\le s\le N$; every initial site lies in $X$; all mean, kernel, noise, coefficient, and initial-observation values are finite reals; the kernel matrix on $X$ is symmetric positive semidefinite; ${\sigma }^2\ge 0$; and each required $b_t$ is defined and nonnegative. If any validation fails, return inadmissible-model before computing a posterior. The observation oracle must finish each call in finite time and return either a finite real observation or observation-unavailable. For a true-posterior interpretation, the initial sites are fixed before their observations and each observation is $f(x_i)+{\xi }_i$ under this model, with errors independent centered Gaussian variables of variance ${\sigma }^2$ and independent of the entire process. In this interpretation, whether a call returns a value or observation-unavailable must be a deterministic measurable function of the already observed history and selected site, decided without inspecting the unobserved process or the fresh noise; thus availability conveys no additional information. Otherwise the procedure computes only the all-data-vector posterior kernel for the specified surrogate and makes no claim that it is the conditional law of an externally supplied data-generating process. The Axiom of Choice is included as required by Finite Gaussian-process posterior and predictive laws.

Denote the sites in the accumulated observation trace, in observation order, by $x_1,\dots ,x_t$; these are not the candidate-list indices and may repeat. Write $X_t=(x_1,\dots ,x_t)$, $y=(y_1,\dots ,y_t)$, $m_{X_t}=(m(x_i){)}_{i\le t}$, and $k_t(x)=(k(x_i,x){)}_{i\le t}$. Initialize the trace with the given data and let its length be $t=s$. If $t=0$, the current state is the prior with ${\mu }_0(x)=m(x)$ and $v_0(x)=k(x,x)$, without a matrix solve. If $t\ge 1$, form $K_t=(k(x_i,x_j){)}_{i,j\le t}$ and $C_t=K_t+{\sigma }^{2}I$. If $C_t$ is not certified positive definite, or its Cholesky factorization or required solves are unavailable, return posterior-solve-unavailable with the initial trace and no posterior state. Otherwise compute the current posterior by the formulas below. At every later history length $t\ge 1$, use the same rule to compute its state immediately after the new observation is appended. Never use a pseudoinverse or clip a negative variance. In particular, this state update is performed after the final observation at history length $N$, before a complete return.

If the initialized history already has length $t=N$, return complete with the initial trace, its computed posterior state, and the empty list of acquisition errors. Otherwise $t<N$, and for each candidate compute ${\mu }_t(x)=m(x)+k_t(x{)}^T{C}_t^{-1}(y-m_{X_t})$ $v_t(x)=k(x,x)-k_t(x{)}^T{C}_t^{-1}{k}_t(x),s_t(x)=\sqrt{v_t(x)}$ where the observed covariance and solves satisfy the hypotheses of Finite Gaussian-process posterior and predictive laws. At $t=0$, use the prior formulas above. At $t\ge 1$, its conditional covariance is positive semidefinite, so $v_t(x)\ge 0$; Square roots exist: a unique $\sqrt{a}\ge 0$ with $(\sqrt{a}{)}^2=a$; the positives are $\{x^2:x\mathrm{\ne }0\}$ supplies the unique nonnegative square root used here. If nonnegativity of a computed $v_t(x)$ cannot be verified, return posterior-solve-unavailable with the current trace and last valid state. Form $a_t(x)={\mu }_t(x)+b_t{s}_t(x)$ and inspect all $M$ candidates. The exact selector returns the least-index maximizer with ${\delta }_t=0$. A certified approximate selector must be a deterministic measurable function of the finite observation history and return a candidate $c_{j_t}$ with verified ${\delta }_t\ge 0$ satisfying $a_t(c_{j_t})\ge {\max }_{x\in X}{a}_t(x)-{\delta }_t$. If no such comparison certificate is available, return acquisition-inconclusive with the current trace and state. Record every ${\delta }_t$.

Call $O$ at the selected candidate. If it returns observation-unavailable, return that status with the current trace and state, without appending a value. If it returns a finite real, append the pair $(x_{t+1},y_{t+1})=(c_{j_t},O(c_{j_t}))$, using the value from this single call, increment $t$ by one, and compute the new posterior state by the rule above; if this solve is unavailable, return posterior-solve-unavailable with the updated trace and last valid state. If $t=N$, return complete with the full trace, posterior state at history length $N$, and recorded acquisition errors. Otherwise continue to the next acquisition stage. For a deterministic simulator or a misspecified prior, these formulas describe only the chosen surrogate model; the algorithm asserts no generic regret, global-optimality, or model-truth result.

Fix an instance $(D_0,C,f)$ from Compact-box global minimization problems and a closed subbox $B\subseteq D_0$. A certified box report may contain any combination of the following fields:

• A feasible witness $(x_B,U_B)$, with $x_B\in B\cap C$ and a verified upper bound $f(x_B)\le U_B$.
• A lower bound ${\mathrm{\ell }}_B\in \mathbb{R}$ satisfying ${\mathrm{\ell }}_B\le f(x)$ for every $x\in B\cap C$. This pointwise condition is vacuous when $B\cap C=\mathrm{\varnothing }$; when $B\cap C\mathrm{\ne }\mathrm{\varnothing }$, it is equivalent to ${\mathrm{\ell }}_B\le {\inf }_{x\in B\cap C}f(x)$.
• An empty-box proof establishing $B\cap C=\mathrm{\varnothing }$.
• A non-finite or unavailable status, which makes no feasibility, lower-bound, or optimality claim.

A box is closed for a requested tolerance $\epsilon >0$ only when it has a lower bound and ${\mathrm{\ell }}_B\ge U-\epsilon$, where $U$ is the best currently verified feasible upper bound. Closing a box stops further subdivision but retains its lower bound in the global ledger. A report lacking a required field is not repaired by a numerical guess.

For every finite box $[l_x,u_x]\times [l_y,u_y]$, the McCormick polytope from McCormick envelope for a bilinear term on a box is exactly the convex hull in ${\mathbb{R}}^3$ of the graph $\{(x,y,xy):x\in [l_x,u_x],y\in [l_y,u_y]\}$.

Input a compact-box instance $(D_0,C,f)$ from Compact-box global minimization problems, a tolerance $\epsilon >0$, a positive integer node budget $N$, and a deterministic box-report oracle implementing Certified lower, upper, and emptiness bounds on a box. Every oracle call must finish in finite time or return an unavailable status. The budget counts each oracle call, including the root and both children after every split. The oracle may request higher precision on a repeated box; each such refinement is another counted call.

Initialize a leaf ledger with the root box $D_0$, no incumbent ($U=+\mathrm{\infty }$), and zero calls. Evaluate the root first. Before every oracle call, if the call counter is already $N$, return the complete current ledger with budget-exhausted; otherwise call the oracle and increment the counter by one. Store every returned field. A feasible witness $(x,U_x)$ updates the incumbent upper bound to $U=\min U_x$. An empty-box proof marks that leaf empty; retain the leaf and its proof in the ledger, but exclude it from lower-bound comparisons, closure tests, and split candidates. For constraints $g_i(x)\le 0$, a sound interval lower bound ${\underset{‾}{g}}_i(B)>0$ is an empty-box proof. Store every valid lower bound ${\mathrm{\ell }}_B$ even if the leaf is later closed. Every evaluated leaf not certified empty requires a finite lower bound; if that field is missing, non-finite, or unavailable, return inconclusive. A certified-empty leaf requires no lower bound.

Whenever all current leaves have been evaluated, first return infeasible if they are all certified empty. Otherwise put $L=\min \{{\mathrm{\ell }}_B:B\text{ is not certified empty}\}$. If $U<+\mathrm{\infty }$, $L$ is finite, and $U-L\le \epsilon$, return a feasible witness and the epsilon-global certificate $(L,U)$. Mark any leaf not certified empty with ${\mathrm{\ell }}_B\ge U-\epsilon$ closed while retaining its lower bound.

If no certificate is returned and no pending child awaits evaluation, split the nonclosed leaf not certified empty with least lower bound; ties use creation order. In a box with positive widths, bisect a longest coordinate at its exact midpoint, using the least coordinate index among ties. Replace the parent by its two closed subboxes, which cover it. Create and evaluate the child with the lower half of the split coordinate first, then the upper-half child. Pending children are evaluated in that order before the next all-leaves check or split. In the unconstrained mode, the oracle returns the exact midpoint as a feasible witness and exact objective value; the termination theorem uses this mode. For a zero-width singleton that has not been certified, request a deterministic higher-precision report for that same point; each refinement consumes one call. If refinement is unavailable, return inconclusive. When no certificate or infeasibility result has been established and another oracle call is needed after $N$ calls, the pre-call guard returns the complete current ledger with no optimality claim. This finite-budget procedure is global-search bookkeeping: a local stationary point or a solver tolerance is not a lower-bound certificate.

Assume AC; let $f_X$ have a fixed real Gaussian-process prior with mean $m$ and symmetric positive-semidefinite covariance matrix on a nonempty finite ordered candidate set $X$. Let the observation errors be independent $N(0,{\sigma }^2)$ variables, independent of the entire process. The initial observation sites, if any, are fixed before their observations and their values are generated by $y_i=f(x_i)+{\xi }_i$ under this same model. At every valid history length $t$, assume $C_t=K_t+{\sigma }^{2}I$ is positive definite when $t\ge 1$ (which holds for every possibly singular $K_t$ when ${\sigma }^2>0$ by Positive Gaussian observation noise makes the observed covariance positive definite, and holds for zero noise when $K_t$ itself is positive definite). Assume observation availability is a deterministic measurable function of the already observed history and selected site, decided without inspecting the unobserved process or fresh noise, as required by the algorithm's true-posterior interpretation. Use the exact least-index maximizer, or a deterministic approximate selector that is measurable with respect to the observed history and supplies its verified error ${\delta }_t$. Then after any finite history for which Finite-candidate Gaussian-process acquisition search with explicit statuses computes a posterior state, the conditional law of $f_X$ given that history is the posterior supplied by Finite Gaussian-process posterior and predictive laws, with mean and covariance computed from the actually selected observation list. This includes the updated state at the final horizon. An unavailable solve or observation ends the assertion at the last history with a computed posterior state. This theorem proves a sequential posterior update, not a regret or global-search guarantee.

For a nonempty finite candidate list of length $M\ge 1$, a horizon $N\ge 0$, and an initial-list length $s$ with $0\le s\le N$, the procedure in Finite-candidate Gaussian-process acquisition search with explicit statuses terminates after at most $N-s$ observation calls. It returns complete with the posterior state at history length $N$, or one of its explicit inadmissible-model, posterior-solve-unavailable, acquisition-inconclusive, or observation-unavailable statuses. Assume every validation, positive-definiteness check, Cholesky factorization, triangular solve, acquisition-certificate check, and observation call finishes in finite time or reports failure.

For every admissible finite oracle call and every positive integer budget $N$, Finite-budget certified spatial branch and bound terminates after at most $N$ calls and returns exactly one of: a verified epsilon-global certificate, a certified infeasibility result, or an inconclusive budget/oracle status.

Consider an unconstrained instance $C=D_0$ from Compact-box global minimization problems, with continuous $f$ on the compact box $D_0$. Run the unlimited continuation of Finite-budget certified spatial branch and bound with exact midpoint objective evaluations and finite exact lower bounds. Assume either $D_0$ has positive diameter, or a singleton root report gives the exact value as both lower and upper bound. Assume the lower-bound oracle is consistent: on every nested sequence of nonclosed boxes $B_k$ with diameters tending to zero and unique limit $x$, its lower bounds satisfy $\mathrm{\ell }(B_k)\to f(x)$. Midpoint evaluations then give upper bounds converging to $f(x)$. The algorithm reaches $U-L\le \epsilon$ after finitely many calls for every $\epsilon >0$. Consequently, any finite budget exceeding that finite call count returns the epsilon-global certificate.

Suppose Finite-budget certified spatial branch and bound returns a feasible witness $\widehat{x}$ with a verified upper bound $U$, and its complete terminal-leaf ledger contains a valid lower bound for every nonempty leaf. Let $L$ be the least such lower bound. If $U-L\le \epsilon$, then $\widehat{x}$ is globally epsilon-optimal: $f(\widehat{x})-{\inf }_{x\in C}f(x)\le \epsilon \mathrm{.}$ If instead every terminal leaf has a certified empty-box proof, then $C=\mathrm{\varnothing }$.

Input a box $B={\prod }_j[a_j,b_j]\subseteq D_0$ with arbitrary finite ordered real endpoints, a finite real expression DAG from Real intervals, complex rectangles and ball enclosures using addition, subtraction, multiplication, and division, a precision $p\ge 2$, and a dyadic format with fixed exponent bounds. Round each input endpoint outward at precision $p$, replacing $[a_j,b_j]$ by $[{\mathrm{rd}}_p(a_j),{\mathrm{ru}}_p(b_j)]$; if an endpoint rounding overflows, return overflow. Thus every interval passed to an interval operation has dyadic endpoints and contains the original box coordinate interval. The same rule applies to a singleton input, including a midpoint point-evaluation path. The DAG must define a real-valued function at every point of $B$; for each division node its denominator range on $B$ must exclude zero. Each constant is either an exact dyadic, enclosed by $[{\mathrm{rd}}_p(c),{\mathrm{ru}}_p(c)]$, or is accompanied by a precision-indexed certified interval containing it whose width tends to zero as $p\to \mathrm{\infty }$. If any constant enclosure overflows or is unavailable, return that status with no finite bound claim. Traverse the finite DAG in topological order. Enclose each input by its outward-rounded interval, each constant by its certified interval at precision $p$, and apply the corresponding outward-rounded operation from Outward-rounded interval, rectangle and ball operations at precision $p$. Return the root enclosure $I_p(B)=[a_{-},a_{+}]$, its lower and upper endpoints, and the exact midpoint of $B$ as a candidate point. If any operation returns overflow, split-domain, domain-error, entire, or inconclusive, return that status with no finite bound claim.

For a continuous objective on an unconstrained box, the midpoint is feasible and $a_{+}$ is a verified upper bound for its objective value. On a constrained box, the midpoint is only a candidate: a separate feasibility witness is required. To refine arithmetic error, callers increase $p$ along any sequence of shrinking boxes. Fixed exponent bounds must be chosen so no exact intermediate on the certified domain overflows; otherwise the procedure returns an explicit failure status.

A finite factorable expression DAG on a box $B$ has input variables, certified constants, affine nodes, product nodes, and optional unary nonlinear nodes. A certified convex relaxation of its constrained minimization problem consists of a convex-program representation in the form of Finite-dimensional convex program, Lagrangian dual, and Slater condition, with feasible set $R_B$ in lifted variables and convex objective ${\varphi }_B$ on $R_B$, and an exact-value embedding ${\iota }_B$ with these properties:

1. For every original feasible point $x\in B\cap C$, the exact value of each DAG node defines ${\iota }_B(x)\in R_B$.
2. The relaxed objective underestimates the original: ${\varphi }_B({\iota }_B(x))\le f(x)$.
3. Every product node $w=uv$ is represented by a McCormick polytope from McCormick envelope for a bilinear term on a box using operand bounds that enclose their exact ranges. Every other nonlinear node must use supplied convex and concave graph enclosures with verified domain hypotheses. If no such enclosure is supplied, no relaxation is defined.
4. Every interval bound and coefficient affected by finite precision carries an outward-rounded enclosure from Outward-rounded interval, rectangle and ball operations. A non-finite status or unverified coefficient makes the relaxation unavailable.

For a convex program represented in Finite-dimensional convex program, Lagrangian dual, and Slater condition, a dual certificate is a dual-feasible pair $(\lambda ,\nu )$ together with a verified real lower bound $\mathrm{\ell }$ for its Lagrangian dual value $q(\lambda ,\nu )$. The definition records a certificate interface only; it does not assert that a solver finds one.

Input a bounded factorable optimization problem on a box $B$, its objective DAG $F$, a finite list of inequality-constraint DAGs $G_i$ representing $g_i(x)\le 0$, a finite rule table, a precision $p\ge 2$, and a dyadic interval format with fixed exponent bounds. For each non-product nonlinear node, the table must supply certified convex and concave graph bounds ${\psi }^{-}\le w\le {\psi }^{+}$ on its certified operand domain, with proof that they contain the exact graph and that the imposed epigraph/hypograph inequalities form a convex relation. The table must also supply a convex underestimator ${\varphi }_B$ for the objective DAG's final value, verified to satisfy ${\varphi }_B({\iota }_B(x))\le f(x)$ for every exact input $x\in B$. All domain hypotheses and interval/coefficient enclosures must be certified. For each interval call, pass the same declared precision and format to Outward-rounded interval enclosures for factorable expression DAGs on boxes. Traverse the union of the objective and constraint DAGs in topological order, using a lifted variable for each node. For an affine node, add its exact affine relation. For a product node $w=uv$, add the four McCormick inequalities from McCormick envelope for a bilinear term on a box using certified operand bounds; The four McCormick inequalities give the convex hull of a bilinear graph over a box proves this relation is a convex outer enclosure of the product graph. For every other nonlinear node, add its certified convex and concave graph bounds; if its domain hypotheses, interval bounds, graph containment, or convexity cannot be verified, return unsupported-relaxation or inconclusive. For each constraint DAG, require its final lifted value to be at most zero.

Return the resulting convex feasible region $R_B$ and the certified objective underestimator ${\varphi }_B$ only when every lifted relation is convex, every original feasible point has its exact node values in the lifted region, and all coefficient enclosures preserve the declared inequalities. These checks make the construction a relaxation of both the objective and all listed constraints in the sense of Certified factorable convex relaxations on a box. Optionally pass this relaxation to a finite convex-bound routine. A dual-feasible pair and a verified lower bound on its Lagrangian dual value produce a dual-certificate record; if no such record is available, return bound-unavailable. The procedure asserts no solver convergence or polynomial running-time bound.

Input a compact-box instance $(D_0,C,f)$, a finite arithmetic expression DAG representing $f$, a closed box $B={\prod }_{j=1}^n[a_j,b_j]\subseteq D_0$, a nonnegative certified constant $L$, a precision $p\ge 2$, a dyadic interval format with fixed exponent bounds, a certificate that the midpoint $m$ is in $C$ (automatic when $C=D_0$), and a validated inequality $\mathrm{\mid }f(x)-f(y)\mathrm{\mid }\le L{\max }_j\mathrm{\mid }{x}_j-y_j\mathrm{\mid }(x,y\in B)\mathrm{.}$ Let $m_j=(a_j+b_j)\mathrm{/}2$ and $r={\max }_j(b_j-a_j)\mathrm{/}2$. Apply Outward-rounded interval enclosures for factorable expression DAGs on boxes to the supplied DAG at the singleton $\{m\}$ with the supplied precision and format to obtain $I_p(\{m\})=[q_{-},q_{+}]$; its endpoint-rounding rule encloses a possibly non-dyadic midpoint. Compute a directed-rounding upper bound $r^{+}\ge r$ and a downward-rounded lower endpoint ${\mathrm{\ell }}_B\le q_{-}-L{r}^{+}$. Return the pointwise lower-bound report ${\mathrm{\ell }}_B$ and the feasible midpoint candidate $(m,q_{+})$. If the feasibility certificate or either interval or arithmetic calculation is unavailable or non-finite, return inconclusive without a feasible-witness claim.

Suppose Finite McCormick convex relaxation construction for factorable box problems returns a certified convex relaxation $(R_B,{\varphi }_B)$ of an original problem on a box $B$ with $B\cap C\mathrm{\ne }\mathrm{\varnothing }$, and a dual-feasible pair $(\lambda ,\nu )$ with a verified lower bound $\mathrm{\ell }\le q(\lambda ,\nu )$. Then $\mathrm{\ell }$ is a valid lower bound for the original box problem: $\mathrm{\ell }\le {\inf }_{x\in B\cap C}f(x)\mathrm{.}$ This certificate applies only to the stated relaxation and its verified coefficient/domain enclosures. A solver residual or an approximate dual objective without a verified lower bound is not a certificate.

Assume a finite arithmetic expression DAG uses $+$, $-$, $\times$, and division only where the exact denominator is bounded away from zero on the box. Each constant is an exact dyadic or has certified enclosures at precision $p$ whose widths tend to zero as $p\to \mathrm{\infty }$. Assume all operation results are finite. For every precision $p$, the enclosure returned by Outward-rounded interval enclosures for factorable expression DAGs on boxes contains the exact range $f[B]$; hence its lower and upper endpoints are valid bounds for every point in $B$. If $B_k$ is a nested sequence of boxes with diameters tending to zero, their limit point is $x$, and the precisions $p_k$ tend to infinity in one fixed exponent range large enough to avoid overflow, then the interval endpoints tend to $f(x)$. Under the Lipschitz hypothesis in Validated Lipschitz midpoint lower bounds on boxes, its lower bounds are valid on $B$ and tend to $f(x)$ on every such shrinking sequence.

Input a nonempty box $D_0$ from Compact-box global minimization problems, a finite nonempty list of constraints $g_i(x)\le 0$, a positive integer query budget $N$, and a deterministic oracle returning a sound lower bound ${\mathrm{\ell }}_i(B)\le {\inf }_{x\in B}{g}_i(x)$ for every queried box. The oracle returns explicit unavailable or non-finite statuses when it cannot certify a finite bound. For a valid arithmetic-DAG oracle as in Outward interval and Lipschitz midpoint bounds are sound and consistent under refinement, choose one fixed exponent range large enough to avoid overflow and set the query precision to $p_0+d+r$, where $p_0\ge 2$, $d$ is the split depth, and $r\ge 0$ is a singleton-refinement index.

Initialize a FIFO queue with $(D_0,0,0)$ and an empty ledger. Each oracle query consumes one unit, including a singleton precision refinement. Before a query, if the budget is exhausted, return the current queue and ledger with budget-exhausted. Query all $g_i$, in index order, on the oldest queued box at precision $p_0+d+r$; this one box query requests the vector of constraint bounds and consumes one budget unit. If any reported bound is unavailable or has a non-finite status, return inconclusive with the current queue and ledger, without an emptiness claim. Otherwise record the finite lower bounds and remove that entry from the queue. If some ${\mathrm{\ell }}_i(B)>0$, record the box as certified empty. If no lower bound is positive and $B$ has positive width, bisect a longest coordinate at its exact midpoint, using the least coordinate index to break ties, and enqueue the two closed children, lower half first and upper half second, at depth $d+1$ with refinement index $0$. If $B$ is a singleton with no positive lower bound, enqueue the same point with split depth $d$ and refinement index $r+1$, so its next query uses strictly higher precision. When the queue is empty, return infeasible with the complete ledger. This procedure has no termination claim without an additional separation condition; it returns infeasible only from a finite cover by certified-empty boxes.

Input a finite-dimensional compact continuous box $X={\prod }_{j=1}^n[{\alpha }_j,{\beta }_j]$ with $n\ge 0$ and finite ordered endpoints, a finite integer box $Z={\prod }_{j=1}^r([a_j,b_j]\cap \mathbb{Z}),r\ge 0,a_j,b_j\in \mathbb{Z},a_j\le b_j,$ a continuous objective and its inequality constraints on $X\times Z$ represented by finite factorable expression DAGs, tolerance $\epsilon >0$, positive integer node budget $N$, a verified interval/relaxation rule table, precision $p\ge 2$, a dyadic interval format with fixed exponent bounds, and deterministic verified bound oracles. Every relaxation rule must meet Finite McCormick convex relaxation construction for factorable box problems, and every bound used for pruning or a gap certificate must satisfy A verified dual certificate for a McCormick relaxation is a valid global lower bound on each nonempty feasible node. The integer set $Z$ is finite by boundedness of every coordinate interval. Every main-tree node evaluation consumes one unit of the budget and each oracle call returns in finite time or gives an explicit unavailable status.

When $r=0$, the empty product defining $Z$ is the singleton assignment with no integer coordinates. When $n=0$, $X$ is the singleton empty tuple. Before any oracle or supplier call, represent it instead by a dummy continuous coordinate in $[0,0]$ and make every objective and constraint DAG ignore that coordinate. Run all instructions below on this one-dimensional box; on return, delete the dummy coordinate from every witness and ledger box. This bijective representation preserves all objective and constraint values and admits every spatial subcall without excluding purely integer inputs.

A main-tree node is $(J,B)$, where $J$ is a product of bounded integer intervals and $B\subseteq X$ is a continuous box. Relax each integer interval to its real hull and call Finite McCormick convex relaxation construction for factorable box problems on the objective DAG and all constraint DAGs over $B$ times those hulls, passing the declared precision and interval format. A verified dual lower bound is valid on the original integer-feasible node by A verified dual certificate for a McCormick relaxation is a valid global lower bound. The oracle may also return a feasible mixed-integer witness with a verified objective upper bound, a proof of emptiness, or an unavailable status. The latter never supplies a finite lower bound. Store lower bounds for terminal nodes. Retain certified-empty nodes and their proofs in the terminal ledger, excluding them from lower-bound comparisons, closure tests, and split selection; they require no lower bound. Close a node not certified empty only when its lower bound is at least $U-\epsilon$, retaining that bound in the global ledger.

Initialize the terminal ledger with the root $(Z,X)$, a FIFO queue containing that unevaluated root, remaining budget $N$, incumbent $U=+\mathrm{\infty }$, and no incumbent witness. Each returned feasible witness with verified upper bound $U_x<U$ replaces the incumbent and sets $U=U_x$; retain the earlier witness on an equal bound. Keep unevaluated nodes in the FIFO queue ordered by creation. Generate lower integer children before upper integer children, and lower-half continuous children before upper-half children, appending children in this order. Before each node evaluation, if no call remains, return the current ledger with budget-exhausted; otherwise evaluate the oldest pending node and charge one call. When no node is pending, return infeasible if every terminal node is certified empty. If every terminal node not certified empty has a valid lower bound, let $L$ be the least such bound; when $U$ is finite and $U-L\le \epsilon$, return the feasible witness and global epsilon certificate. Retain bounds for closed nodes in this calculation. Otherwise choose an evaluated nonclosed node not certified empty with least lower bound, breaking ties by creation order. If an integer interval has at least two values, choose the least-index such coordinate and split at $m=\lfloor (a+b)\mathrm{/}2\rfloor$ into the disjoint children $[a,m]\cap \mathbb{Z}$ and $[m+1,b]\cap \mathbb{Z}$. Otherwise, if a continuous width is positive, split a longest continuous side at its exact midpoint, using least coordinate index ties. Children replace the parent in the coverage frontier and are evaluated before another split. A mixed singleton node that is neither certified empty nor closed by the gap test returns inconclusive.

If a mixed relaxation bound is unavailable or non-finite on a node not certified empty, stop the main tree and, if at least one call remains for each assignment, enumerate every $z\in Z$ in lexicographic order. Substitute $z$ into the objective and constraint DAGs to form $f_z$ and $C_z=\{x\in X:g_i(x,z)\le 0\text{ for all }i\}$, then invoke Finite-budget certified spatial branch and bound on $(X,C_z,f_z)$ with the continuous budget allocated to that assignment. Explicitly, with $M=\mathrm{\mid }Z\mathrm{\mid }$ and remaining integer budget $R\ge M$, set $q=\lfloor R\mathrm{/}M\rfloor$ and $h=R-Mq$. Give the first $h$ assignments $q+1$ calls each and the remaining $M-h$ assignments $q$ calls each. These are positive integer budgets summing to $R$. If any assignment has an oracle failure, a pending or missing report, or a terminal leaf not certified empty without a valid finite lower bound, return inconclusive. If every assignment is certified infeasible, return infeasible before taking any minimum. Otherwise the complete assignment ledgers have a nonempty finite collection of terminal leaves not certified empty. Let $L$ be the minimum of their lower bounds. Let $U$ be the minimum of the feasible upper bounds returned by these ledgers if there are any, and set $U=+\mathrm{\infty }$ if there is no feasible witness. Return a global epsilon certificate only when $U$ is finite and $U-L\le \epsilon$; otherwise return inconclusive. If enumeration does not fit in the remaining budget, return inconclusive. This fallback is finite because $Z$ is finite. The method makes no polynomial-complexity claim.

Let $D_0$ be a nonempty compact box and let $g_1,\dots ,g_m:D_0\to \mathbb{R}$ be continuous, with $m\ge 1$. Assume the constraint oracle in Certified constraint-emptiness search with a finite query budget returns finite-time sound lower bounds, and these bounds converge to $g_i(x)$ along every nested shrinking sequence with limit $x$ when the precision tends to infinity. If there is a uniform margin $\delta >0$ such that ${\max }_{1\le i\le m}{g}_i(x)\ge \delta$ for every $x\in D_0$, then the unlimited continuation of the procedure certifies every leaf empty and returns infeasible after finitely many oracle calls. Consequently, a finite query budget at least that call count returns the same result. Conversely, if $\{x\in D_0:g_i(x)\le 0(1\le i\le m)\}=\mathrm{\varnothing }$, then such a uniform margin exists. The margin condition is separate from continuity of the objective; objective continuity alone does not certify constraint emptiness.