Tensor helpers for verification artifacts

Verification tools often sit at the boundary between Lean tensors and external JSON artifacts. Flat payloads are checked against the requested tensor shape; nested matrix payloads also check each row. Once loaded, the checkers work with tensors rather than serialized arrays.

def NN.Verification.Util.Tensor.boundsOrdered {n : ℕ} (lo hi : TorchLean.Tensor Float [n]) : Bool

Pointwise ordering of equally shaped bounds. NaN comparisons fail.

def NN.Verification.Util.Tensor.boxWithin {n : ℕ} (rootLo rootHi lo hi : TorchLean.Tensor Float [n]) : Bool

Check ordered leaf bounds contained in an equally shaped root box.

def NN.Verification.Util.Tensor.refutesThreshold {n : ℕ} (lowerBound threshold : TorchLean.Tensor Float [n]) : Bool

A strict lower-bound witness refutes its corresponding threshold.

def NN.Verification.Util.Tensor.refutesThresholdAt {n : ℕ} (lowerBound threshold : TorchLean.Tensor Float [n]) (witnessIdx : ℕ) : Bool

Check the supplied coordinate; out-of-range witnesses and NaN comparisons fail.

def NN.Verification.Util.Tensor.ofArray? {α : Type} [TorchLean.Storage α] (shape : Spec.Shape) (xs : Array α) : Option (TorchLean.Tensor α shape)

Read a row-major artifact into the requested tensor shape; reject a length mismatch.

def NN.Verification.Util.Tensor.ofRows? {α : Type} [TorchLean.Storage α] (rows cols : ℕ) (xs : Array (Array α)) : Option (TorchLean.Tensor α [rows, cols])

Read a nested row-major artifact into a matrix tensor.

Both the row count and every row length are checked before the tensor is built.

def NN.Verification.Util.Tensor.requireArray (ctx : String) (shape : Spec.Shape) (xs : Array Float) : IO (TorchLean.Tensor Float shape)

Read a JSON float array into the requested shape, or raise a schema error.