LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

The four McCormick inequalities give the convex hull of a bilinear graph over a box

Statement

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 $R^{3}$ of the graph ${(x, y, x y) : x \in [l_{x}, u_{x}], y \in [l_{y}, u_{y}]}$ .

Facts & Assumptions

Given: Ordered finite real endpoints $l_{x} \leq u_{x}$ and $l_{y} \leq u_{y}$ , and the four inequalities defining the McCormick polytope.

[F1]

The four defining inequalities and box bounds are those in McCormick envelope for a bilinear term on a box.

[F2]

A set is convex when it contains every line segment between two of its points. A convex subset of $R^{m}$ contains every line segment between two of its points

[L1]

In this item, $conv (S)$ denotes all finite convex combinations $\sum_{j = 1}^{r} α_{j} s_{j}$ with $s_{j} \in S$ , $α_{j} \geq 0$ , and $\sum_{j} α_{j} = 1$ .

Proof

1.1givenF1algebra

On the graph $w = x y$ , subtracting the first lower plane from $x y$ gives $(x - l_{x}) (y - l_{y}) \geq 0$ , and subtracting the second lower plane gives $(u_{x} - x) (u_{y} - y) \geq 0$ . Subtracting $x y$ from the first upper plane gives $(u_{x} - x) (y - l_{y}) \geq 0$ , and subtracting it from the second upper plane gives $(x - l_{x}) (u_{y} - y) \geq 0$ . Thus every graph point satisfies all four inequalities.

1.2F1algebra

If both widths are positive, put $s = u_{x} - l_{x} > 0$ , $t = u_{y} - l_{y} > 0$ , $X = (x - l_{x}) / s$ , $Y = (y - l_{y}) / t$ , and $W = (w - l_{x} y - l_{y} x + l_{x} l_{y}) / (s t)$ . The inequalities become $0 \leq X, Y \leq 1$ , $W \geq 0$ , $W \geq X + Y - 1$ , $W \leq X$ , and $W \leq Y$ .

2.1F1F2L1step 1.1algebrainduction

Every defining bound and McCormick inequality is affine in $(x, y, w)$ . If two points satisfy one such affine inequality, their line segment also satisfies it by linearity, so the polytope is convex by [F2]. By step 1.1 every graph point lies in this polytope, and therefore each finite convex combination of graph points lies there by repeated segment closure [L1].

2.2F1F2step 1.1algebra

If $u_{x} = l_{x}$ , the first lower and first upper inequalities force $w = l_{x} y$ ; all graph points satisfy the other inequalities by step 1.1. For any $y, y^{'} \in [l_{y}, u_{y}]$ and $θ \in [0, 1]$ , the segment between $(l_{x}, y, l_{x} y)$ and $(l_{x}, y^{'}, l_{x} y^{'})$ is $(l_{x}, θ y + (1 - θ) y^{'}, l_{x} (θ y + (1 - θ) y^{'}))$ , again on the graph. If $u_{y} = l_{y}$ , the first lower and second upper inequalities force $w = x l_{y}$ , and the same calculation with $x, x^{'} \in [l_{x}, u_{x}]$ proves convexity. Thus either degenerate case gives the product graph itself.

2.3step 1.2algebraconstruct

In the nondegenerate case of step 1.2, set $λ_{11} = W$ , $λ_{10} = X - W$ , $λ_{01} = Y - W$ , and $λ_{00} = 1 - X - Y + W$ . Step 1.2 makes each coefficient nonnegative; their sum is $1$ , and $(X, Y, W) = λ_{00} (0, 0, 0) + λ_{10} (1, 0, 0) + λ_{01} (0, 1, 0) + λ_{11} (1, 1, 1)$ . Each vertex lies on $W = X Y$ , so every normalized polytope point is a convex combination of graph points.

3.1step 1.2step 2.1step 2.2step 2.3algebra∎

If either width is zero, step 2.2 gives equality directly. If both are positive, the affine map in step 1.2 is invertible, and steps 2.1 and 2.3 prove both inclusions after normalization. These cases exhaust the ordered endpoint choices, proving equality of the original polytope and graph convex hull.

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

A. Tsoukalas and A. Mitsos, Multivariate McCormick relaxations, §5 (standard reference, not scraped)
Arnold Neumaier, Complete Search in Continuous Global Optimization and Constraint Satisfaction, §16 (standard reference, not scraped)