CROWN Graph Theorems

Shape, dimension, and enclosure lemmas for the graph CROWN engine. Keeping these proof layer facts separate from the executable propagation passes makes the implementation files easier to browse.

@[simp]

theorem NN.MLTheory.CROWN.Graph.ConcatLayout.concat_get {α : Type} [TorchLean.Storage α] (layout : ConcatLayout) (values : (parent : Fin layout.lengths.length) → TorchLean.Tensor α [(layout.parentShape parent).size]) (parent : Fin layout.lengths.length) (index : Fin (layout.parentShape parent).size) : (layout.concat values).getScalar (layout.flatEquiv ⟨parent, index⟩) = (values parent).getScalar index

Concatenation preserves the scalar at each embedded parent coordinate.

@[simp]

theorem NN.MLTheory.CROWN.Graph.ConcatLayout.split_concat {α : Type} [TorchLean.Storage α] (layout : ConcatLayout) (values : (parent : Fin layout.lengths.length) → TorchLean.Tensor α [(layout.parentShape parent).size]) (parent : Fin layout.lengths.length) : layout.split (layout.concat values) parent = values parent

Splitting recovers each occurrence, including repeated parents and zero-length segments.

@[simp]

theorem NN.MLTheory.CROWN.Graph.ConcatLayout.concat_split {α : Type} [TorchLean.Storage α] (layout : ConcatLayout) (value : TorchLean.Tensor α [layout.outputShape.size]) : layout.concat (layout.split value) = value

Concatenating all coordinate slices recovers the original objective.

theorem NN.MLTheory.CROWN.Graph.ConcatLayout.concat_encloses {α : Type} [TorchLean.Storage α] [Context α] (layout : ConcatLayout) (lower upper values : (parent : Fin layout.lengths.length) → TorchLean.Tensor α [(layout.parentShape parent).size]) (h : ∀ (parent : Fin layout.lengths.length) (index : Fin (layout.parentShape parent).size), (lower parent).getScalar index ≤ (values parent).getScalar index ∧ (values parent).getScalar index ≤ (upper parent).getScalar index) (index : Fin layout.outputShape.size) : (layout.concat lower).getScalar index ≤ (layout.concat values).getScalar index ∧ (layout.concat values).getScalar index ≤ (layout.concat upper).getScalar index

Parent interval enclosure is preserved by concat without any scalar arithmetic.

theorem NN.MLTheory.CROWN.Graph.Theorems.ibp_linear_output_dim {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (p : LinParams α) (Xin : FlatBox α) (h : Xin.dim = p.n) (ps : ParamStore α) (id : ℕ) (hstore : ps.linearWB[id]? = some p) : Option.map (fun (x : FlatBox α) => x.dim) (ibpLinear id ps Xin) = some p.m

Dimension lemma: linear IBP returns an output box with the expected dimension.

theorem NN.MLTheory.CROWN.Graph.Theorems.box_add_dim {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B1 B2 : FlatBox α) : (boxAdd B1 B2).dim = B1.dim

Simple shape-preservation facts for FlatBox combinators used by IBP.

theorem NN.MLTheory.CROWN.Graph.Theorems.box_sub_dim {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B1 B2 : FlatBox α) : (boxSub B1 B2).dim = B1.dim

boxSub preserves the left operand’s dim (even when the right operand has a mismatched dim).

theorem NN.MLTheory.CROWN.Graph.Theorems.box_relu_dim {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : (boxRelu B).dim = B.dim

boxRelu preserves dim.

theorem NN.MLTheory.CROWN.Graph.Theorems.box_square_dim {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B : FlatBox α) : (boxSquare B).dim = B.dim

boxSquare preserves dim.

Canonical forms for boxAdd/boxSub when dimensions match

theorem NN.MLTheory.CROWN.Graph.Theorems.box_add_on_eq {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (n : ℕ) (lo1 hi1 lo2 hi2 : TorchLean.Tensor α [n]) : boxAdd { dim := n, lo := lo1, hi := hi1 } { dim := n, lo := lo2, hi := hi2 } = { dim := n, lo := TorchLean.Tensor.map2Spec BoundOps.addDown lo1 lo2, hi := TorchLean.Tensor.map2Spec BoundOps.addUp hi1 hi2 }

theorem NN.MLTheory.CROWN.Graph.Theorems.box_sub_on_eq {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (n : ℕ) (lo1 hi1 lo2 hi2 : TorchLean.Tensor α [n]) : boxSub { dim := n, lo := lo1, hi := hi1 } { dim := n, lo := lo2, hi := hi2 } = { dim := n, lo := TorchLean.Tensor.map2Spec BoundOps.subDown lo1 hi2, hi := TorchLean.Tensor.map2Spec BoundOps.subUp hi1 lo2 }

Canonical form for boxSub when both boxes have the same dimension.

Declarative enclosure predicates used by downstream graph-soundness statements.

def NN.MLTheory.CROWN.Graph.Theorems.Semantics.encloses {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) (x : TorchLean.Tensor α [B.dim]) : Prop

encloses B x means vector x lies componentwise between B.lo and B.hi.

theorem NN.MLTheory.CROWN.Graph.Theorems.Semantics.box_add_sound {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) (lo1 hi1 lo2 hi2 : TorchLean.Tensor α [n]) (add_mono : ∀ {a b c d : α}, a ≤ b → c ≤ d → a + c ≤ b + d) (x y : TorchLean.Tensor α [n]) (hx : encloses { dim := n, lo := lo1, hi := hi1 } x) (hy : encloses { dim := n, lo := lo2, hi := hi2 } y) : encloses { dim := n, lo := lo1.addSpec lo2, hi := hi1.addSpec hi2 } (x.addSpec y)

If x is enclosed in [lo1,hi1] and y is enclosed in [lo2,hi2], then x+y is enclosed in [lo1+lo2, hi1+hi2].

The scalar order fact is passed as add_mono: from a ≤ b and c ≤ d, derive a + c ≤ b + d.

theorem NN.MLTheory.CROWN.Graph.Theorems.Semantics.box_sub_sound {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) (lo1 hi1 lo2 hi2 : TorchLean.Tensor α [n]) (sub_mono : ∀ {a b c d : α}, a ≤ b → d ≤ c → a - c ≤ b - d) (x y : TorchLean.Tensor α [n]) (hx : encloses { dim := n, lo := lo1, hi := hi1 } x) (hy : encloses { dim := n, lo := lo2, hi := hi2 } y) : encloses { dim := n, lo := lo1.subSpec hi2, hi := hi1.subSpec lo2 } (x.subSpec y)

If x is enclosed in [lo1,hi1] and y is enclosed in [lo2,hi2], then x-y is enclosed in [lo1-hi2, hi1-lo2].

The scalar order fact is passed as sub_mono: from a ≤ b and d ≤ c, derive a - c ≤ b - d.

theorem NN.MLTheory.CROWN.Graph.Theorems.Semantics.box_relu_sound {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) (lo hi : TorchLean.Tensor α [n]) (relu_mono : ∀ {a b : α}, a ≤ b → Activation.Math.reluSpec a ≤ Activation.Math.reluSpec b) (x : TorchLean.Tensor α [n]) (hx : encloses { dim := n, lo := lo, hi := hi } x) : encloses (boxRelu { dim := n, lo := lo, hi := hi }) (castDimScalar ⋯ (Activation.reluSpec x))

Enclosure for boxRelu: if $x\in B$, then $\operatorname{ReLU}(x)$ belongs to the resulting box.