Interval Soundness Lemmas

Scalar interval arithmetic, box-cast lemmas, and point-box facts used by the graph IBP soundness induction.

Op-level soundness lemmas (enclosure for each supported step)

These lemmas are the building blocks for the final “certificate ⇒ semantics enclosure” theorem.

This proof reuses the following existing components:

• Linear IBP soundness over ℝ is already proved in NN.MLTheory.CROWN.mlp as NN.MLTheory.CROWN.Theorems.ibp_linear_sound_real.
• For add/sub/relu on FlatBox, the graph file already contains enclosure lemmas in NN.MLTheory.CROWN.Graph.Theorems.Semantics.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.relu_mono_real {a b : ℝ} : a ≤ b → Activation.Math.reluSpec a ≤ Activation.Math.reluSpec b

Monotonicity of real ReLU, used by interval enclosure proofs.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.box_mulElem_sound_real (n : ℕ) (lo1 hi1 lo2 hi2 x y : TorchLean.Tensor ℝ [n]) (hx : encloses { dim := n, lo := lo1, hi := hi1 } x) (hy : encloses { dim := n, lo := lo2, hi := hi2 } y) {B : FlatBox ℝ} : boxMulElem { dim := n, lo := lo1, hi := hi1 } { dim := n, lo := lo2, hi := hi2 } = some B → EnclosesBox B { n := n, v := x.mulSpec y }

Elementwise interval multiplication of two boxes is sound.

FloatLib bounds each coordinate by the four endpoint products. The box wrapper also checks the dimensions, so the conclusion concerns the box actually returned by boxMulElem.

Casting and containment

Boxes and values carry their dimensions in dependent types. Transporting both along the same equality preserves containment; the box conversion lemmas let operator proofs reuse Box bounds without unfolding the flattened representation.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.contains_castBoxDim_iff {n n' : ℕ} (h : n = n') (B : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (x : TorchLean.Tensor ℝ [n]) : (castBoxDim h B).contains (castDimScalar h x) ↔ B.contains x

Casting a box and a point along the same equality does not change containment.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.encloses_of_contains {n : ℕ} (B : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (x : TorchLean.Tensor ℝ [n]) : B.contains x → encloses (toFlatBox n B) x

Box.contains implies encloses on the flattened box; the two are definitionally the same, and the lemma exists so proofs can change vocabulary without unfolding.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.contains_of_encloses (B : FlatBox ℝ) (x : TorchLean.Tensor ℝ [B.dim]) : encloses B x → (ofFlatBox B).contains x

The converse direction, for the same reason.

Point Boxes Always Enclose Their Point

This is used in the .const case, where a constant node certifies a point box [v,v] and the semantics returns exactly the same v.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.encloses_point_self_real {n : ℕ} (x : TorchLean.Tensor ℝ [n]) : Theorems.Semantics.encloses { dim := n, lo := x, hi := x } x