ResidualAffine

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

This module provides:

• Eval of an affine upper/lower bound on the network output u(x) using runAffine and AffineVec.eval_on_box, given the current input box.
• 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.castBoxDimEq {n n' : ℕ} (h : n = n') (B : MLTheory.CROWN.Box Float (Spec.Shape.dim n Spec.Shape.scalar)) : MLTheory.CROWN.Box Float (Spec.Shape.dim n' Spec.Shape.scalar)

Cast a dimension-indexed vector box across definitional equality of Nats.

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.affineUBounds (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore Float) (ibp : Array (Option (MLTheory.CROWN.FlatBox Float))) : Option (Float × Float)

Backwards-compatible name used by the PINN CLI: treat "affine" u-bounds as objective-dependent CROWN.

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

Scalar product upper envelope over rectangles using McCormick. Given u∈[lx,ux], v∈[ly,uy], returns an affine upper bound of the form uv ≤ axu + ayv + c, as coefficients (ax, ay, c). We pick 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∈[lx,ux], v∈[ly,uy], returns an affine lower bound of the form uv ≥ axu + ayv + c.

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

Evaluate an affine axu + ayv + c on intervals u∈[ul,uh], v∈[vl,vh] to produce a numeric interval bound.

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

Basic 1D branch-and-bound over the input box [x-ε,x+ε]. Recursively splits the box up to maxDepth or until width ≤ minWidth. On each sub-box it calls the provided bounding function boundOn which must return (lo, hi). Returns the tightest global (min lo, max hi) across sub-boxes.

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