Flattened interval bounds (FlatBox)

FlatBox α is a small container for interval bounds on a flattened tensor value.

It is used by the graph-based LiRPA/CROWN development (NN.MLTheory.CROWN.Graph) and by some operator-level transfer rules that operate on flattened vectors (e.g. slice/reduce rules).

dim is the flattened size, and lo/hi are tensors of shape .dim dim .scalar.

structure NN.MLTheory.CROWN.FlatBox (α : Type) [TorchLean.Storage α] [Context α] : Type

Flattened interval bounds.

dim is the flattened size (number of scalar components).

• dim : ℕ

  Flattened output dimension.

• lo : TorchLean.Tensor α [self.dim]

  Lower bound vector (shape .dim dim .scalar).

• hi : TorchLean.Tensor α [self.dim]

  Upper bound vector (shape .dim dim .scalar).

theorem NN.MLTheory.CROWN.FlatBox.ext {α : Type} [TorchLean.Storage α] [Context α] {B1 B2 : FlatBox α} (hDim : B1.dim = B2.dim) (hLo : B1.lo ≍ B2.lo) (hHi : B1.hi ≍ B2.hi) : B1 = B2

Extensionality for the dependent record FlatBox: equal dimension and heterogeneously equal endpoints. Stated by hand because the endpoint types depend on dim, so the ext tactic has no automatically generated lemma to use.

theorem NN.MLTheory.CROWN.FlatBox.ext_iff {α : Type} [TorchLean.Storage α] [Context α] {B1 B2 : FlatBox α} : B1 = B2 ↔ B1.dim = B2.dim ∧ B1.lo ≍ B2.lo ∧ B1.hi ≍ B2.hi

def NN.MLTheory.CROWN.FlatBox.Valid {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : Prop

Componentwise validity of a flat interval box: lo ≤ hi for every coordinate.

This is a proof layer predicate; it uses the order carried by Context α, which keeps all CROWN box predicates in the same scalar universe as the executable operators.

def NN.MLTheory.CROWN.FlatBox.ofTensor {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (t : TorchLean.Tensor α [n]) : FlatBox α

Build a singleton FlatBox from an exact vector tensor t (set lo = hi = t).

theorem NN.MLTheory.CROWN.FlatBox.valid_ofTensor {α : Type} [TorchLean.Storage α] [Context α] (le_refl : ∀ (a : α), a ≤ a) {n : ℕ} (t : TorchLean.Tensor α [n]) : (ofTensor t).Valid

A singleton flat box is always valid (over any preorder).