ResidualAffine

Helpers for assembling PDE residual bounds using affine CROWN relaxations where available.

This module provides:

• Evaluation of affine upper/lower bounds on the network output u(x).
• McCormick-style linear upper/lower envelopes for scalar products over independent intervals (for Burgers-type residuals).

These calculations use host Float arithmetic. The exact-real McCormick inequalities do not by themselves prove that the rounded coefficients and endpoints enclose the exact residual.

References:

• CROWN / DeepPoly-style affine bounds: https://arxiv.org/abs/1811.00866
• alpha,beta-CROWN (context): https://arxiv.org/abs/2103.06624

def NN.Verification.PINN.ResidualAffine.crownUBoundsForward (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (ibp : Array (Option (MLTheory.CROWN.FlatBox Float))) : Option (Float × Float)

Forward CROWN/DeepPoly bounds for the scalar output u (or sum of outputs).

def NN.Verification.PINN.ResidualAffine.crownUBoundsBackward (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (ibp : Array (Option (MLTheory.CROWN.FlatBox Float))) : Option (Float × Float)

Objective-dependent (backward/dual) CROWN bounds for the scalar output u (or the sum of outputs).

def NN.Verification.PINN.ResidualAffine.mccormickUpper (lx ux ly uy : Float) : Float × Float × Float

Scalar product upper envelope over rectangles using McCormick.

Given $u\in[l_x,u_x]$ and $v\in[l_y,u_y]$, this returns coefficients $(a_x,a_y,c)$ for the affine upper bound

$$ uv\le a_xu+a_yv+c. $$

It selects the plane with the smaller value at the rectangle midpoint. That need not be the tighter plane at every point of the rectangle.

def NN.Verification.PINN.ResidualAffine.mccormickLower (lx ux ly uy : Float) : Float × Float × Float

Scalar product lower envelope over rectangles using McCormick.

Given $u\in[l_x,u_x]$ and $v\in[l_y,u_y]$, this returns an affine lower bound $uv\ge a_xu+a_yv+c$.

def NN.Verification.PINN.ResidualAffine.evalAffine2DOnBox (ax ay c ul uh vl vh : Float) : Float × Float

Evaluate $a_xu+a_yv+c$ on the box $u\in[u_{\mathrm{lo}},u_{\mathrm{hi}}]$, $v\in[v_{\mathrm{lo}},v_{\mathrm{hi}}]$ to produce a numeric interval bound.