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 {n : ℕ} (f : ℝ → ℝ) (hf : Monotone f) (xB : Box ℝ (Spec.Shape.dim n Spec.Shape.scalar)) (x : TorchLean.Tensor ℝ [n]) (hx : xB.contains x) : (Runtime.Ops.IBP.mapMinmax f xB).contains (TorchLean.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|

Cosine is 1-Lipschitz, proved from the sum-to-product identity.

The interval rules for sin and cos fall back on this whenever the input interval is too wide for a monotone branch: a Lipschitz constant of one turns the input width directly into an output width.

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

Interval bound propagation through sin is sound over ℝ.

The implementation checks whether the interval is short enough to contain no critical point and uses the monotone endpoints if so, falling back to [-1, 1] otherwise; both branches are covered here.

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

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