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.mapMinmax for monotone scalar functions

Runtime.Ops.IBP.sigmoid and Runtime.Ops.IBP.tanh are defined using mapMinmax. 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 {s : Spec.Shape} (f : ℝ → ℝ) (hf : Monotone f) (xB : Box ℝ s) (x : TorchLean.Tensor ℝ s) (hx : xB.contains x) : (Runtime.Ops.IBP.mapMinmax f xB).contains (TorchLean.Tensor.map 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: the Lipschitz constant one (Real.abs_sin_sub_sin_le, Real.abs_cos_sub_cos_le) turns the input half-width directly into an output half-width.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.ibp_sin_sound_real {s : Spec.Shape} (xB : Box ℝ s) (x : TorchLean.Tensor ℝ s) (hx : xB.contains x) : (Runtime.Ops.IBP.sin xB).contains (TorchLean.Tensor.map Real.sin x)

Interval bound propagation through sin is sound over ℝ.

Each component uses the midpoint Lipschitz enclosure, intersected with [-1, 1].

theorem NN.MLTheory.CROWN.Graph.CertSoundness.ibp_cos_sound_real {s : Spec.Shape} (xB : Box ℝ s) (x : TorchLean.Tensor ℝ s) (hx : xB.contains x) : (Runtime.Ops.IBP.cos xB).contains (TorchLean.Tensor.map Real.cos x)

Interval bound propagation through cos is sound over ℝ, by the same argument.