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 verified dual certificate for a McCormick relaxation is a valid global lower bound

Statement

Suppose Finite McCormick convex relaxation construction for factorable box problems returns a certified convex relaxation $(R_{B}, ϕ_{B})$ of an original problem on a box $B$ with $B \cap C \neq \emptyset$ , and a dual-feasible pair $(λ, ν)$ with a verified lower bound $ℓ \leq q (λ, ν)$ . Then $ℓ$ is a valid lower bound for the original box problem: $ℓ \leq \inf_{x \in B \cap C} f (x) .$ 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.

Facts & Assumptions

Given: A certified relaxation from Certified factorable convex relaxations on a box with $B \cap C \neq \emptyset$ , a dual-feasible pair, a verified $ℓ \leq q (λ, ν)$ , and finite outward-rounded arithmetic.

[F1]

For every original feasible $x$ , the exact DAG values define an embedded relaxed point $ι_{B} (x) \in R_{B}$ and $ϕ_{B} (ι_{B} (x)) \leq f (x)$ . Certified factorable convex relaxations on a box

[F2]

Every exact bilinear graph point over its operand box lies in the McCormick polytope; the four inequalities give its convex hull. The four McCormick inequalities give the convex hull of a bilinear graph over a box

[F3]

Every exact finite arithmetic-DAG node value lies in its finite outward-rounded enclosure; a non-finite status makes no enclosure claim. Outward-rounded operations are inclusion-isotone and enclose DAG evaluations

[F4]

For a primal-feasible point and dual-feasible pair, the Lagrangian dual value satisfies $q (λ, ν) \leq f_{0} (y)$ . Every Lagrangian dual feasible pair is a lower-bound certificate

Proof

1.1givenF1F2F3constructinduction

Fix $x \in B \cap C$ . Traverse its finite expression DAG in topological order and assign each lifted variable its exact node value. Affine equalities hold by construction. At each product node the exact operands lie within their certified ranges by [F3], and the exact product graph lies in its McCormick polytope by [F2]. Every other nonlinear relation is included only with a verified outer graph enclosure by the algorithm definition. Thus the constructed lifted point $ι_{B} (x)$ lies in $R_{B}$ , and the relaxed objective satisfies $ϕ_{B} (ι_{B} (x)) \leq f (x)$ by [F1].

2.1givenF1F4step 1.1algebra

Weak duality [F4], applied to the relaxed primal point $ι_{B} (x)$ from step 1.1, gives $q (λ, ν) \leq ϕ_{B} (ι_{B} (x))$ . Since the verified certificate satisfies $ℓ \leq q (λ, ν)$ , we obtain $ℓ \leq ϕ_{B} (ι_{B} (x)) \leq f (x)$ .

3.1step 2.1algebra∎

The inequality in step 2.1 holds for every $x \in B \cap C$ , so taking the infimum over that set yields $ℓ \leq \inf_{x \in B \cap C} f (x)$ .

Depends on

Used by

Dependency tree · two levels

18 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, §§16 and 20 (standard reference, not scraped)