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) [Context α] : Type

Flattened interval bounds.

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

• dim : ℕ

  Flattened output dimension.

• lo : Spec.Tensor α (Spec.Shape.dim self.dim Spec.Shape.scalar)

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

• hi : Spec.Tensor α (Spec.Shape.dim self.dim Spec.Shape.scalar)

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

def NN.MLTheory.CROWN.FlatBox.getScalar {α : Type} {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (i : Fin n) : α

Extract the scalar entry at index i from a flat vector tensor.

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

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

This is a proof-facing 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} [Context α] {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : FlatBox α

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

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

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