CROWN Graph Theorems

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

Helper lemmas about shapes/dimensions of basic constructions

theorem NN.MLTheory.CROWN.Graph.toFlatBox_dim {α : Type} [Context α] (n : ℕ) (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : (toFlatBox n B).dim = n

toFlatBox creates a box whose dim matches the given n.

theorem NN.MLTheory.CROWN.Graph.Theorems.ibp_linear_output_dim {α : Type} [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) (ibp_linear 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} [Context α] [BoundOps α] (B1 B2 : FlatBox α) : (box_add 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} [Context α] [BoundOps α] (B1 B2 : FlatBox α) : (box_sub B1 B2).dim = B1.dim

box_sub 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} [Context α] (B : FlatBox α) : (box_relu B).dim = B.dim

box_relu preserves dim.

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

box_square preserves dim.

Canonical forms for box_add/box_sub when dimensions match

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

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

Canonical form for box_sub 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} [Context α] [LE α] (B : FlatBox α) (x : Spec.Tensor α (Spec.Shape.dim B.dim Spec.Shape.scalar)) : 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} [Context α] [LE α] (n : ℕ) (lo1 hi1 lo2 hi2 : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (add_mono : ∀ {a b c d : α}, a ≤ b → c ≤ d → a + c ≤ b + d) (x y : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (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} [Context α] [LE α] (n : ℕ) (lo1 hi1 lo2 hi2 : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (sub_mono : ∀ {a b c d : α}, a ≤ b → d ≤ c → a - c ≤ b - d) (x y : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (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} [Context α] [LE α] (n : ℕ) (lo hi : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (relu_mono : ∀ {a b : α}, a ≤ b → Activation.Math.reluSpec a ≤ Activation.Math.reluSpec b) (x : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (hx : encloses { dim := n, lo := lo, hi := hi } x) : encloses (box_relu { dim := n, lo := lo, hi := hi }) (castDimScalar ⋯ (Activation.reluSpec x))

Enclosure for box_relu: if x ∈ B then ReLU(x) ∈ box_relu B.

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

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

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