Nonlinear IBP Soundness Lemmas

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

Sigmoid monotonicity (via Mathlib’s Real.sigmoid)

Our Activation.Math.sigmoid_spec definition over ℝ is exactly the Mathlib sigmoid function. So we can reuse its monotonicity lemma.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.sigmoid_mono_real : Monotone Activation.Math.sigmoidSpec

Monotonicity of the real sigmoid used by graph IBP certificates.

Tanh monotonicity (proved from calculus in Mathlib)

Mathlib does not expose a Real.tanh_monotone lemma under that name. We prove it here:

1. Use the identity tanh x = sinh x / cosh x.
2. Differentiate the quotient, using d/dx sinh = cosh and d/dx cosh = sinh.
3. Simplify the derivative using cosh^2 - sinh^2 = 1.
4. Conclude strict monotonicity from deriv > 0, hence monotonicity.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.hasDerivAt_tanh_real (x : ℝ) : HasDerivAt Real.tanh (1 / Real.cosh x ^ 2) x

Derivative of real tanh, stated in the form needed for monotonicity.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.tanh_strictMono_real : StrictMono Real.tanh

theorem NN.MLTheory.CROWN.Graph.CertSoundness.tanh_mono_real : Monotone Real.tanh

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)