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.

Consistent bounds and exhaustive longest-side branching give eventual epsilon termination

Statement

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 $ℓ (B_{k}) \to f (x)$ . Midpoint evaluations then give upper bounds converging to $f (x)$ . The algorithm reaches $U - L \leq ε$ after finitely many calls for every $ε > 0$ . Consequently, any finite budget exceeding that finite call count returns the epsilon-global certificate.

Facts & Assumptions

Given: $C = D_{0}$ , a continuous real-valued $f$ on the finite closed box $D_{0}$ , a tolerance $ε > 0$ , consistent lower/upper box bounds as stated, and the deterministic longest-side midpoint split.

[F1]

A closed finite box in $R^{n}$ is compact. Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $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

[F2]

A continuous image of a compact metric space is compact, and a compact subset of a metric space is closed and bounded. The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset, A compact subset of a metric space is closed and bounded

[F3]

Every nonempty subset of $R$ bounded below has an infimum, and for every $η > 0$ some member lies below the infimum plus $η$ . Every nonempty set bounded below has an infimum, Epsilon characterisation of the infimum

[F4]

A point belongs to the closure of a set exactly when every open ball around it meets the set; a closed set contains its closure. The closure of a nonempty $A$ is ${x : d (x, A) = 0}$ , equals $A$ together with its limit points, and is the smallest closed superset

[F5]

Open balls in the usual metric on $R$ are the intervals $(v - η, v + η)$ , and a bounded subset lies in some such ball. The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space

[F6]

At each split checkpoint, after all current leaves have been evaluated and the closure test has been applied, every nonclosed leaf has lower bound strictly below the current $U - ε$ . A leaf closes only when its lower bound is at least $U - ε$ at a closure test. Finite-budget certified spatial branch and bound

[F7]

Nested closed real intervals whose lengths tend to zero have a unique common point. A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$

[A1]

The lower-bound oracle is consistent on every nested shrinking nonclosed branch, and exact midpoint witnesses provide the upper bounds specified in the Statement.

[A2]

The unconstrained oracle reports the exact midpoint objective as a feasible witness on every queried box; if the root is a singleton, it also reports the exact point lower bound.

Proof

1.1givenF1F2F3F4F5

The box $D_{0}$ is nonempty (its left-endpoint vector belongs to it) and compact by [F1]. Therefore $f [D_{0}]$ is nonempty and compact by [F2], hence closed and bounded. By the boundedness definition and [F5], there are $c \in R$ and $r > 0$ such that $f [D_{0}] \subseteq (c - r, c + r)$ , so $c - r$ is a lower bound. Let $f^{*} = \inf f [D_{0}]$ , which exists by [F3]. For every $η > 0$ , [F3] gives $y \in f [D_{0}]$ with $f^{*} \leq y < f^{*} + η$ ; by [F5] every open ball around $f^{*}$ meets $f [D_{0}]$ . Thus $f^{*} \in \overline{f [D_{0}]}$ by [F4], and closedness gives $f^{*} \in f [D_{0}]$ . So $f$ attains its minimum on $D_{0}$ , and every feasible objective value is at least $f^{*}$ .

2.1givenstep 1.1A2algebraconstruct

The incumbent upper bounds $U_{k}$ are nonincreasing, and each is at least the attained minimum $f^{*}$ by step 1.1 and [A2]. If the unlimited continuation did not terminate, it would expand infinitely many boxes. The expansion tree is binary, so there is an infinite nested branch: recursively take the left child if it has infinitely many expanded descendants and otherwise take the right child. This rule is deterministic and requires no choice principle.

3.1givenF1F7step 2.1algebra

Along this branch, longest-side bisection makes every side length tend to zero. Fix $η > 0$ . Each coordinate can be halved only finitely many times while its side length is at least $η$ , because each halving divides a finite initial length by two and never increases it. There are finitely many coordinates, and every split whose box has a side of length at least $η$ halves one such longest side, so only finitely many such splits occur. Thus the maximum side length tends to zero. The nested closed coordinate intervals have a unique common point in each coordinate by [F7], giving $x \in D_{0}$ .

4.1givenA1A2F6step 3.1algebra

Let $U_{k}$ be the incumbent at the split checkpoint at which branch box $B_{k}$ is expanded. The closure test has already been applied, so [F6] gives $ℓ (B_{k}) < U_{k} - ε$ . That box was previously evaluated at its midpoint $m_{k}$ , so [A2] and the incumbent update give $U_{k} \leq f (m_{k})$ . By step 3.1, $m_{k} \to x$ ; continuity and consistency [A1] imply $f (m_{k}) \to f (x)$ and $ℓ (B_{k}) \to f (x)$ . Thus $ℓ (B_{k}) < f (m_{k}) - ε$ for every $k$ , whose limit gives $f (x) \leq f (x) - ε$ , contradicting $ε > 0$ .

5.1step 2.1step 3.1step 4.1discharge-contradiction∎

Thus the unlimited continuation cannot expand infinitely many boxes without meeting $U - L \leq ε$ . It reaches that certificate after finitely many calls, so any larger finite call budget returns it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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, §2.1 (standard reference, not scraped)