Softplus and safeLog bounds

The executable transfers use elementary bounds on softplus, so they can handle large positive inputs without evaluating a large exponential. SafeLog then adds its scalar epsilon interval and checks that the whole logarithm argument is positive. This file connects those transfers to the real specifications, including the fact that epsilon may vary inside its own interval.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.softplus_tail_bounds_real {z : ℝ} (hz : z ≤ 0) : 0 ≤ Real.log (1 + Real.exp z) ∧ Real.log (1 + Real.exp z) ≤ 1

The logarithmic tail in the stable softplus branch lies between zero and one.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.softplus_envelope_real (x : ℝ) : max x 0 ≤ Activation.Math.softplusSpec x ∧ Activation.Math.softplusSpec x ≤ max x 0 + 1

Softplus differs from max x 0 by a nonnegative term of size at most one.

The proof follows the same sign branch as the executable specification. In each branch the exponential argument is nonpositive, which is why the resulting interval rule needs no large exponential at either endpoint.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.softplusBounds_sound_real {lo hi outLo outHi x : ℝ} (hB : NonlinearBoundOps.softplusBounds lo hi = some (outLo, outHi)) (hxlo : lo ≤ x) (hxhi : x ≤ hi) : outLo ≤ Activation.Math.softplusSpec x ∧ Activation.Math.softplusSpec x ≤ outHi

Every successful real softplus transfer encloses the source operation.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.log_reciprocal_bounds_real {x : ℝ} (hx : 0 < x) : 1 - 1 / x ≤ Real.log x ∧ Real.log x ≤ x - 1

The reciprocal fallback for logarithm is valid on the entire positive real axis.

It is deliberately coarse near zero. Its purpose is to give directed-arithmetic backends a usable enclosure even when they do not supply a correctly rounded logarithm transfer.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.safeLogBounds_sound_real {lo hi epsilonLo epsilonHi outLo outHi x epsilon : ℝ} (hB : NonlinearBoundOps.safeLogBounds lo hi epsilonLo epsilonHi = some (outLo, outHi)) (hxlo : lo ≤ x) (hxhi : x ≤ hi) (helo : epsilonLo ≤ epsilon) (hehi : epsilon ≤ epsilonHi) : outLo ≤ Activation.Math.safeLogSpec x epsilon ∧ Activation.Math.safeLogSpec x epsilon ≤ outHi

SafeLog encloses both its input and its scalar epsilon, without replacing epsilon by a default.

Successful transfer establishes positivity of the lower logarithm argument. The proof uses that check to apply monotonicity of the real logarithm; no positivity premise is added to the caller.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_boxUnaryEnclosure {f : ℝ → ℝ} {enclose : ℝ → ℝ → Option (ℝ × ℝ)} (hEnclose : ∀ {lo hi outLo outHi x : ℝ}, enclose lo hi = some (outLo, outHi) → lo ≤ x → x ≤ hi → outLo ≤ f x ∧ f x ≤ outHi) {B1 B : FlatBox ℝ} {v1 : Val} (h1 : EnclosesBox B1 v1) (hB : boxUnaryEnclosure? enclose B1 = some B) : EnclosesBox B { n := v1.n, v := TorchLean.Tensor.mapSpec f v1.v }

A scalar enclosure lifts coordinatewise to the flat tensor representation.

The transfer may fail on any coordinate. If it returns a box, traverseFin gives the corresponding successful scalar transfer at every index, so no unchecked default endpoints enter the proof.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_boxSoftplus {B1 B : FlatBox ℝ} {v1 : Val} (h1 : EnclosesBox B1 v1) (hB : boxSoftplus? B1 = some B) : EnclosesBox B { n := v1.n, v := Activation.softplusSpec v1.v }

The executable softplus box transfer encloses the real tensor specification.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.enclosesBox_boxSafeLog {B1 epsilonBox B : FlatBox ℝ} {v1 : Val} {epsilon : TorchLean.Tensor ℝ [1]} (h1 : EnclosesBox B1 v1) (he : EnclosesBox epsilonBox { n := 1, v := epsilon }) (hB : boxSafeLog? B1 epsilonBox = some B) : EnclosesBox B { n := v1.n, v := Activation.safeLogSpec v1.v (epsilon.getScalar 0) }

The executable safeLog transfer encloses a tensor and a shared scalar epsilon.

The epsilon value is read from its one-element flat tensor after aligning the parent box's dimension with that value. Thus the same epsilon interval is used for every input coordinate.