Certified factorable convex relaxations on a box

A finite factorable expression DAG on a box $B$ has input variables, certified constants, affine nodes, product nodes, and optional unary nonlinear nodes. A certified convex relaxation of its constrained minimization problem consists of a convex-program representation in the form of Finite-dimensional convex program, Lagrangian dual, and Slater condition, with feasible set $R_B$ in lifted variables and convex objective ${\varphi }_B$ on $R_B$, and an exact-value embedding ${\iota }_B$ with these properties:

1. For every original feasible point $x\in B\cap C$, the exact value of each DAG node defines ${\iota }_B(x)\in R_B$.
2. The relaxed objective underestimates the original: ${\varphi }_B({\iota }_B(x))\le f(x)$.
3. Every product node $w=uv$ is represented by a McCormick polytope from McCormick envelope for a bilinear term on a box using operand bounds that enclose their exact ranges. Every other nonlinear node must use supplied convex and concave graph enclosures with verified domain hypotheses. If no such enclosure is supplied, no relaxation is defined.
4. Every interval bound and coefficient affected by finite precision carries an outward-rounded enclosure from Outward-rounded interval, rectangle and ball operations. A non-finite status or unverified coefficient makes the relaxation unavailable.

For a convex program represented in Finite-dimensional convex program, Lagrangian dual, and Slater condition, a dual certificate is a dual-feasible pair $(\lambda ,\nu )$ together with a verified real lower bound $\mathrm{\ell }$ for its Lagrangian dual value $q(\lambda ,\nu )$. The definition records a certificate interface only; it does not assert that a solver finds one.