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

source

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

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

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)

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)

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))

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

source

theorem NN.MLTheory.CROWN.Graph.CertSoundness.box_mul_elem_sound_real (n : ℕ) (lo1 hi1 lo2 hi2 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) {B : FlatBox ℝ} :

box_mul_elem { dim := n, lo := lo1, hi := hi1 } { dim := n, lo := lo2, hi := hi2 } = some B → EnclosesBox B { n := n, v := x.mulSpec y }

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

FlatBox and FlatVec 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