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).
• A compact branch-and-bound splitter on the 1D input box to tighten bounds by subdividing the domain and taking the envelope across sub-boxes.

Notes:

• We intentionally keep this file numeric (Float) and specialized to this workflow.

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 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 chooses the tighter of the two classical McCormick upper planes.

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.

def NN.Verification.PINN.ResidualAffine.branchAndBound1D (x eps : Float) (maxDepth : ℕ) (minWidth : Float) (boundOn : Float → Float → IO (Float × Float)) : IO (Float × Float)

Basic one-dimensional branch-and-bound over $[x-\varepsilon,x+\varepsilon]$.

It recursively splits the box up to maxDepth or until its width is at most minWidth. On each sub-box it calls boundOn, which returns (lo, hi). The result is the tightest global pair (min lo, max hi) across the sub-boxes.

def NN.Verification.PINN.ResidualAffine.branchAndBound1D.go (minWidth : Float) (boundOn : Float → Float → IO (Float × Float)) (a b : Float) (d : ℕ) : IO (Float × Float)