Boxes that enclose a real vector

The engine in NN.MLTheory.CROWN.Graph.Engine.Base propagates boxes; this file relates a box to the real vector it is supposed to contain, and shows that a lawful scalar transfer stays sound when it is applied coordinatewise to a flat box.

The relation is stated in ℝ, which is why it is not part of the engine: the IBP and CROWN passes, the certificate checker, and everything above them run on backend endpoints only.

def NN.MLTheory.CROWN.Graph.EnclosesReal {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (B : FlatBox α) (x : TorchLean.Tensor ℝ [B.dim]) : Prop

The real value represented by each coordinate of x lies between the interpreted endpoints of B. This is the semantic relation used to connect executable endpoint arithmetic to the real graph semantics.

def NN.MLTheory.CROWN.Graph.EnclosesRealValue {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} (B : FlatBox α) (x : TorchLean.Tensor ℝ [n]) : Prop

Dimension-aware enclosure of a real vector by a backend box.

theorem NN.MLTheory.CROWN.Graph.boxUnaryEnclosure?_enclosesReal {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] (f : ℝ → ℝ) (enclose : α → α → Option (α × α)) (henclose : UnaryEnclosure f enclose) (B : FlatBox α) (x : TorchLean.Tensor ℝ [B.dim]) (hx : EnclosesReal B x) {out : FlatBox α} (hout : boxUnaryEnclosure? enclose B = some out) : EnclosesRealValue out (TorchLean.Tensor.mapSpec f x)

A lawful scalar transfer remains sound when applied coordinatewise to a flat graph box.