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.

source

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.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.add_mono_real {a b c d : ℝ} :

a ≤ b → c ≤ d → a + c ≤ b + d

Addition is monotone in both operands.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.sub_mono_real {a b c d : ℝ} :

a ≤ b → d ≤ c → a - c ≤ b - d

Subtraction is monotone in the minuend and antitone in the subtrahend.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.if_lt_eq_min (a b : ℝ) :

(if a < b then a else b) = min a b

The runtime if a < b then a else b is min.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.if_gt_eq_max (a b : ℝ) :

(if a > b then a else b) = max a b

The runtime if a > b then a else b is max.

The implementations branch on a comparison rather than calling min/max, so these two lemmas are what let the interval proofs use the Mathlib lattice lemmas at all.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.mul_const_bounds {a ly uy y : ℝ} (hy : ly ≤ y) (hy' : y ≤ uy) :

min (a * ly) (a * uy) ≤ a * y ∧ a * y ≤ max (a * ly) (a * uy)

Multiplying an interval by a constant: the product lies between the two endpoint products.

Stated with min/max instead of a case split on the sign of a, so the caller never has to know which endpoint is which.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.mul_var_bounds {lx ux x y : ℝ} (hx : lx ≤ x) (hx' : x ≤ ux) :

min (lx * y) (ux * y) ≤ x * y ∧ x * y ≤ max (lx * y) (ux * y)

The same, with the interval on the left and the constant on the right.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.interval_mul_bounds {lx ux ly uy x y : ℝ} (hx : lx ≤ x) (hx' : x ≤ ux) (hy : ly ≤ y) (hy' : y ≤ uy) :

min (min (lx * ly) (lx * uy)) (min (ux * ly) (ux * uy)) ≤ x * y ∧ x * y ≤ max (max (lx * ly) (lx * uy)) (max (ux * ly) (ux * uy))

Interval multiplication: the product of two bounded values lies between the min and the max of the four endpoint products.

This is the classical four-corner rule. All four products are needed because signs can differ, and taking min and max of the corners is exactly tight for real multiplication.

Helpers: our bound propagation uses BoundOps.min2/max2, which are defined via decide (a > b). For ℝ these coincide with min/max.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.min2_eq_min (a b : ℝ) :

BoundOps.min2 a b = min a b

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.max2_eq_max (a b : ℝ) :

BoundOps.max2 a b = max a b

The bound-arithmetic max2 is max over ℝ.

source

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.

Coordinatewise this is interval_mul_bounds; the box wrapper adds the dimension check, which is why the conclusion is about whatever box boxMulElem actually returned.

Casting lemmas (avoid `cases` on `B.dim = v.n`) #

FlatBox and FlatTensor carry their dimensions in dependent types, so it is tempting to cases equalities like h : B.dim = v.n to “align” types. In Lean this can easily trigger dependent elimination failures when the equality mentions fields of dependent records.

Instead, we keep such equalities as data and move tensors/boxes across them using castDimScalar / castBoxDim. The following small lemmas are proved once (by cases on fresh Nat equalities) and then used throughout the main proof without ever cases-ing on B.dim = v.n directly.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.castDimScalar_trans {n n' n'' : ℕ} (h₁ : n = n') (h₂ : n' = n'') (t : TorchLean.Tensor ℝ [n]) :

castDimScalar ⋯ t = castDimScalar h₂ (castDimScalar h₁ t)

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.castDimScalar_map_spec {n n' : ℕ} (h : n = n') (f : ℝ → ℝ) (t : TorchLean.Tensor ℝ [n]) :

castDimScalar h (TorchLean.Tensor.mapSpec f t) = TorchLean.Tensor.mapSpec f (castDimScalar h t)

Dimension casts commute with elementwise maps.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.castDimScalar_add_spec {n n' : ℕ} (h : n = n') (x y : TorchLean.Tensor ℝ [n]) :

castDimScalar h (x.addSpec y) = (castDimScalar h x).addSpec (castDimScalar h y)

Dimension casts commute with addition.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.castDimScalar_sub_spec {n n' : ℕ} (h : n = n') (x y : TorchLean.Tensor ℝ [n]) :

castDimScalar h (x.subSpec y) = (castDimScalar h x).subSpec (castDimScalar h y)

Dimension casts commute with subtraction.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.castDimScalar_mul_spec {n n' : ℕ} (h : n = n') (x y : TorchLean.Tensor ℝ [n]) :

castDimScalar h (x.mulSpec y) = (castDimScalar h x).mulSpec (castDimScalar h y)

Dimension casts commute with elementwise multiplication.

source

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.

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.encloses_castDim {B : FlatBox ℝ} {n' : ℕ} (h : B.dim = n') (x : TorchLean.Tensor ℝ [B.dim]) :

encloses B x → encloses { dim := n', lo := castDimScalar h B.lo, hi := castDimScalar h B.hi } (castDimScalar h x)

Enclosure survives a dimension cast, which is how a box proved for one layer width is reused at the next one without ever eliminating the equality itself.

source

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.

source