GraphIBPBasicTheorems

Basic theorems about the graph-level IBP engine:

• A Valid predicate for interval boxes (lo ≤ hi componentwise).
• Preservation of validity for core interval ops (add/sub/relu) and runtime monotone-activation IBP.
• Validity of the linear/matmul IBP rules (derived from the existing ibp_linear_sound_real proof).

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

Extract the underlying scalar value at index i from a vector tensor.

def NN.MLTheory.CROWN.Box.Valid {n : ℕ} (B : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) : Prop

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

theorem NN.MLTheory.CROWN.Box.valid_of_contains {n : ℕ} (B : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : B.contains x) : B.Valid

If a box contains any point, then it is componentwise valid (lo ≤ hi).

theorem NN.MLTheory.CROWN.Box.contains_lo_of_valid {n : ℕ} (B : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hB : B.Valid) : B.contains B.lo

A valid box contains its lower endpoint lo.

theorem NN.MLTheory.CROWN.Box.valid_castBoxDim {n n' : ℕ} (h : n = n') (B : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hB : B.Valid) : (Graph.castBoxDim h B).Valid

Validity is preserved by (definitional) casts of the vector dimension.

theorem NN.MLTheory.CROWN.Graph.FlatBoxTheorems.valid_toFlatBox_real {n : ℕ} (B : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hB : B.Valid) : (toFlatBox n B).Valid

Converting a valid Box into a FlatBox preserves validity.

theorem NN.MLTheory.CROWN.Graph.FlatBoxTheorems.valid_ofFlatBox_real (B : FlatBox ℝ) (hB : B.Valid) : (ofFlatBox B).Valid

Converting a valid FlatBox into a Box preserves validity.

theorem NN.MLTheory.CROWN.Graph.FlatBoxTheorems.valid_box_add_real (B1 B2 : FlatBox ℝ) (h1 : B1.Valid) (h2 : B2.Valid) : (box_add B1 B2).Valid

Validity is preserved by interval addition on FlatBox (over ℝ).

theorem NN.MLTheory.CROWN.Graph.FlatBoxTheorems.valid_box_sub_real (B1 B2 : FlatBox ℝ) (h1 : B1.Valid) (h2 : B2.Valid) : (box_sub B1 B2).Valid

Validity is preserved by interval subtraction on FlatBox (over ℝ).

theorem NN.MLTheory.CROWN.Graph.FlatBoxTheorems.valid_box_relu_real (B : FlatBox ℝ) (hB : B.Valid) : (box_relu B).Valid

Validity is preserved by ReLU-IBP on FlatBox (over ℝ).

theorem NN.MLTheory.CROWN.Graph.Theorems.ibp_linear_valid_real {m n : ℕ} (W : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (xB : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (bB : Box ℝ (Spec.Shape.dim m Spec.Shape.scalar)) (hxB : xB.Valid) (hbB : bB.Valid) : (IBP.linear W xB bB).Valid

Validity of the IBP.linear transfer rule (over ℝ).

theorem NN.MLTheory.CROWN.Graph.Theorems.graph_ibp_linear_valid_real (id : ℕ) (ps : ParamStore ℝ) (Xin : FlatBox ℝ) (hXin : Xin.Valid) : match ibp_linear id ps Xin with | none => True | some Bout => Bout.Valid

Validity of the graph-level linear IBP rule (over ℝ), if the parameters are present.

theorem NN.MLTheory.CROWN.Graph.Theorems.graph_ibp_matmul_valid_real (id : ℕ) (ps : ParamStore ℝ) (Xin : FlatBox ℝ) (hXin : Xin.Valid) : match ibp_matmul id ps Xin with | none => True | some Bout => Bout.Valid

Validity of the graph-level matmul IBP rule (over ℝ), if the parameters are present.