Array predicates for verification artifacts

Small checkers often receive vector data as JSON float arrays before converting anything into shape-indexed tensors. This module keeps the common pointwise predicates in one place.

def NN.Verification.Util.Array.floatLe (x y : Float) : Bool

Boolean ≤ on floats, for executable artifact checks.

def NN.Verification.Util.Array.floatLt (x y : Float) : Bool

Boolean < on floats, for executable artifact checks.

def NN.Verification.Util.Array.boxWithin (rootLo rootHi lo hi : Array Float) : Bool

Check pointwise containment [lo, hi] ⊆ [rootLo, rootHi] for JSON-style float arrays.

The helper is strict about lengths through all2: mismatched arrays are rejected.

def NN.Verification.Util.Array.refutesThreshold (lowerBound threshold : Array Float) : Bool

Check whether a lower-bound vector refutes a threshold vector at some coordinate.

This is the executable form of ∃ i, threshold[i] < lowerBound[i].

def NN.Verification.Util.Array.refutesThresholdAt (lowerBound threshold : Array Float) (witnessIdx : Nat) : Bool

Check a supplied witness coordinate for threshold refutation.

Out-of-range witnesses are rejected instead of silently falling back to another coordinate.