Finite McCormick convex relaxation construction for factorable box problems

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.