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.

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 α] (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.

def NN.MLTheory.CROWN.Graph.Theorems.Semantics.sqLower {α : Type} [Context α] (l u : α) : α

Lower bound for v * v on [l, u].

Squaring is not monotone, so the sign matters here: an interval straddling zero attains 0, and otherwise the minimum sits at the endpoint nearer the origin.

def NN.MLTheory.CROWN.Graph.Theorems.Semantics.sqUpper {α : Type} [Context α] (l u : α) : α

Upper bound for v * v on [l, u]: the larger of the two squared endpoints.

Unlike sqLower there is no case split on the sign, because squaring is maximized at whichever endpoint is farther from the origin whether or not the interval straddles zero.

theorem NN.MLTheory.CROWN.Graph.Theorems.Semantics.box_square_sound {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) (sq_bound : ∀ {l u v : α}, l ≤ v → v ≤ u → sqLower l u ≤ v * v ∧ v * v ≤ sqUpper l u) (x : TorchLean.Tensor α [B.dim]) (hx : encloses B x) : encloses (boxSquare B) (castDimScalar ⋯ (x.mulSpec x))

Coordinatewise squaring of a box encloses the elementwise product of an enclosed tensor.

The scalar bound is taken as a hypothesis rather than proved here, since it is the one step that depends on the ordered-field structure of α; every instance discharges it separately.