TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A spatial branch-and-bound gap certificate proves global epsilon-optimality

Statement

Suppose Finite-budget certified spatial branch and bound returns a feasible witness $\hat{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 \leq ε$ , then $\hat{x}$ is globally epsilon-optimal: $f (\hat{x}) - \inf_{x \in C} f (x) \leq ε .$ If instead every terminal leaf has a certified empty-box proof, then $C = \emptyset$ .

Facts & Assumptions

Given: A box instance $(D_{0}, C, f)$ , the algorithm's split/closure ledger, a feasible witness, valid leaf lower bounds, and $ε > 0$ .

[F1]

The root leaf is $D_{0}$ ; replacing a leaf by its two midpoint children preserves their union as that leaf. A leaf is marked empty only with a proof of emptiness and is retained in the ledger, but excluded from lower-bound comparisons, closure tests, and split candidates. Finite-budget certified spatial branch and bound

[F2]

Every leaf lower bound satisfies $ℓ_{B} \leq f (x)$ for every $x \in B \cap C$ , with validity vacuous on an empty feasible intersection. Certified lower, upper, and emptiness bounds on a box

[F3]

The returned witness satisfies $\hat{x} \in C$ and $f (\hat{x}) \leq U$ . Certified lower, upper, and emptiness bounds on a box

Proof

1.1givenF1induction

By induction on the finite number of splits, the union of terminal leaves is $D_{0}$ : it holds at initialization, and each split replaces one leaf by two children whose union is the parent by [F1]. Every feasible point is therefore in a terminal leaf that is not certified empty.

2.1step 1.1F2algebra

For any $x \in C$ , choose a terminal leaf $B$ containing $x$ using step 1.1. Its lower-bound report is valid by [F2], so $L \leq ℓ_{B} \leq f (x)$ . Since this holds for every feasible $x$ , $L \leq \inf_{x \in C} f (x)$ .

3.1givenstep 2.1F3algebra∎

The witness bound [F3] and $U - L \leq ε$ give $f (\hat{x}) \leq U \leq L + ε \leq \inf_{x \in C} f (x) + ε$ , proving the global gap claim. If every leaf is certified empty, step 1.1 covers $D_{0}$ by leaves disjoint from $C$ , so $C = \emptyset$ .

Depends on

Used by

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Arnold Neumaier, Complete Search in Continuous Global Optimization and Constraint Satisfaction, §12 (standard reference, not scraped)
Thomas Hübner, Akshay Gupte, and Steffen Rebennack, Spatial branch-and-bound for nonconvex separable piecewise linear optimization, §4 (standard reference, not scraped)