Nonlinear IBP Soundness Lemmas

Monotonicity and Lipschitz facts for the nonlinear graph operations handled by the IBP certificate soundness theorem.

Soundness of Runtime.Ops.IBP.map_minmax for monotone scalar functions

Runtime.Ops.IBP.sigmoid and Runtime.Ops.IBP.tanh are defined using map_minmax. If the activation is monotone, then the min/max of the endpoints is a correct enclosure.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.map_minmax_sound_real {n : ℕ} (f : ℝ → ℝ) (hf : Monotone f) (xB : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : xB.contains x) : (Runtime.Ops.IBP.mapMinmax f xB).contains (Spec.Tensor.mapSpec f x)

Soundness of the 1-Lipschitz sin/cos enclosures

Runtime.Ops.IBP.sin / Runtime.Ops.IBP.cos use a midpoint enclosure with radius r=(u-l)/2, clamped to [-1,1]. This avoids periodic case splits while remaining sound.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.sin_lipschitz_real (x y : ℝ) : |Real.sin x - Real.sin y| ≤ |x - y|

theorem NN.MLTheory.CROWN.Graph.CertSoundness.cos_lipschitz_real (x y : ℝ) : |Real.cos x - Real.cos y| ≤ |x - y|

theorem NN.MLTheory.CROWN.Graph.CertSoundness.ibp_sin_sound_real {n : ℕ} (xB : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : xB.contains x) : (Runtime.Ops.IBP.sin xB).contains (Spec.Tensor.mapSpec Real.sin x)

theorem NN.MLTheory.CROWN.Graph.CertSoundness.ibp_cos_sound_real {n : ℕ} (xB : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (x : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (hx : xB.contains x) : (Runtime.Ops.IBP.cos xB).contains (Spec.Tensor.mapSpec Real.cos x)