Validated Lipschitz midpoint lower bounds on boxes

Input a compact-box instance $(D_0,C,f)$, a finite arithmetic expression DAG representing $f$, a closed box $B={\prod }_{j=1}^n[a_j,b_j]\subseteq D_0$, a nonnegative certified constant $L$, a precision $p\ge 2$, a dyadic interval format with fixed exponent bounds, a certificate that the midpoint $m$ is in $C$ (automatic when $C=D_0$), and a validated inequality $\mathrm{\mid }f(x)-f(y)\mathrm{\mid }\le L{\max }_j\mathrm{\mid }{x}_j-y_j\mathrm{\mid }(x,y\in B)\mathrm{.}$ Let $m_j=(a_j+b_j)\mathrm{/}2$ and $r={\max }_j(b_j-a_j)\mathrm{/}2$. Apply Outward-rounded interval enclosures for factorable expression DAGs on boxes to the supplied DAG at the singleton $\{m\}$ with the supplied precision and format to obtain $I_p(\{m\})=[q_{-},q_{+}]$; its endpoint-rounding rule encloses a possibly non-dyadic midpoint. Compute a directed-rounding upper bound $r^{+}\ge r$ and a downward-rounded lower endpoint ${\mathrm{\ell }}_B\le q_{-}-L{r}^{+}$. Return the pointwise lower-bound report ${\mathrm{\ell }}_B$ and the feasible midpoint candidate $(m,q_{+})$. If the feasibility certificate or either interval or arithmetic calculation is unavailable or non-finite, return inconclusive without a feasible-witness claim.