NF Elementwise Bounds: Softplus and Safe Log

NFBackend.safeLog is a clamped log surrogate $\log(\max(x,\varepsilon))$ with an unconditional forward bound.

For smooth activations that use log (notably softplus and safeLog), we route the outer log through safeLog at a known lower bound:

• $\operatorname{softplus}(x)=\log(1+\exp x)$ and $1+\exp x\ge 1$, so $\operatorname{softplus}(x)=\operatorname{safeLog}(1,1+\exp x)$;
• $\operatorname{safeLog}(x)=\log(\operatorname{softplus}(x)+\varepsilon)$ and $\operatorname{softplus}(x)+\varepsilon\ge\varepsilon$, so $\operatorname{safeLog}(x) =\operatorname{safeLog}(\varepsilon,\operatorname{softplus}(x)+\varepsilon)$.

This avoids needing a separate log approximation lemma while remaining extensionally equal on ℝ for the intended arguments.

noncomputable def Proofs.RuntimeApprox.NFBackend.oneEps {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] : ℝ

Half-ULP rounding budget at the scalar value 1, used in the softplus helper bounds.

noncomputable def Proofs.RuntimeApprox.NFBackend.oneHat {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} : ℝ

Rounded representation of the scalar constant 1 at the NF backend.

noncomputable def Proofs.RuntimeApprox.NFBackend.expHat {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (a : ℝ) : ℝ

Rounded representation of exp a at the NF backend.

noncomputable def Proofs.RuntimeApprox.NFBackend.addHatSoftplus {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (a : ℝ) : ℝ

Rounded surrogate for the inner 1 + exp a term appearing in softplus.

noncomputable def Proofs.RuntimeApprox.NFBackend.addBoundSoftplus {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (a eps : ℝ) : ℝ

Forward-error envelope for the rounded 1 + exp a subexpression used by softplus.

noncomputable def Proofs.RuntimeApprox.NFBackend.softplusBoundScalar {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (a eps : ℝ) : ℝ

Unconditional scalar forward-error bound for softplus, via the safeLog factorization.

noncomputable def Proofs.RuntimeApprox.NFBackend.softplusR {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (xR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) : FloatLib.Floats.Formats.Flocq.NF β fexp rnd

softplus implemented by safeLog 1 (1 + exp x) at the NF backend.

softplus_spec_eq_log_one_add_exp lives in Proofs.Gradients.Activation, which this file imports. This namespace is nested inside Proofs, so the uses below resolve to it without qualification and without an open. The private copy that used to sit here proved the same statement.

theorem Proofs.RuntimeApprox.NFBackend.approx_softplus_nf {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {x : ℝ} {xR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd} {eps : ℝ} (hx : |toSpec xR - x| ≤ eps) : |toSpec (softplusR xR) - Activation.Math.softplusSpec x| ≤ softplusBoundScalar (toSpec xR) eps

Forward approximation bound for softplus in NF.

We treat softplus(x) = log(1 + exp x) as safeLog 1 (1 + exp x) (since 1 + exp x ≥ 1) and then compose the scalar bounds for exp, +, and safeLog.

noncomputable def Proofs.RuntimeApprox.NFBackend.softplusBoundTensor {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (eps : ℝ) (xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) : Spec.SpecTensor s

Per-entry bound tensor for softplusR.

This is the elementwise lifting of softplusBoundScalar, used with linfNorm in approxTensor_softplus_spec.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_softplus_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {eps : ℝ} : approxTensor toSpec xS xR eps → approxTensor toSpec (TorchLean.Tensor.mapSpec Activation.Math.softplusSpec xS) (TorchLean.Tensor.mapSpec softplusR xR) (linfNorm (softplusBoundTensor eps xR))

approxTensor bound for softplus lifted to arbitrary tensor shapes.

This is the tensor-level wrapper around approx_softplus_nf, built via approxTensor_map_spec_of_scalar_bound.

noncomputable def Proofs.RuntimeApprox.NFBackend.safeLogSoftplusR {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} (ε : ℝ) (xR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd) : FloatLib.Floats.Formats.Flocq.NF β fexp rnd

Runtime implementation of safeLog as a single rounded primitive.

theorem Proofs.RuntimeApprox.NFBackend.approx_safe_log_nf {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {x : ℝ} {xR : FloatLib.Floats.Formats.Flocq.NF β fexp rnd} {eps ε : ℝ} (hε : 0 < ε) (hx : |toSpec xR - x| ≤ eps) : |toSpec (safeLogSoftplusR ε xR) - Activation.Math.safeLogSpec x ε| ≤ 1 / ε * eps + FloatLib.Floats.Formats.Flocq.ulp β fexp (Activation.Math.safeLogSpec (toSpec xR) ε) / 2

Forward approximation bound for the smooth safeLog activation in NF.

safeLog is defined as log(softplus(x) + ε), which is globally well-defined for ε > 0. The proof combines:

• one rounding step for safeLogR (defined as NF.ofReal (safe_log_spec ...));
• a (1/ε) Lipschitz bound for the spec function (via mean value theorem + derivative bound).

noncomputable def Proofs.RuntimeApprox.NFBackend.safeLogSoftplusBoundTensor {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (ε eps : ℝ) (xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s) : Spec.SpecTensor s

Per-entry bound tensor for safeLog.

This is the elementwise lifting of approx_safe_log_nf's bound.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_safe_log_spec {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] {s : Spec.Shape} (ε : ℝ) (hε : 0 < ε) {xS : Spec.SpecTensor s} {xR : TorchLean.Tensor (FloatLib.Floats.Formats.Flocq.NF β fexp rnd) s} {eps : ℝ} : approxTensor toSpec xS xR eps → approxTensor toSpec (TorchLean.Tensor.mapSpec (fun (x : Spec.SpecScalar) => Activation.Math.safeLogSpec x ε) xS) (TorchLean.Tensor.mapSpec (safeLogSoftplusR ε) xR) (linfNorm (safeLogSoftplusBoundTensor ε eps xR))

approxTensor bound for safeLog lifted to arbitrary tensor shapes.

This is the tensor-level wrapper around approx_safe_log_nf, built via approxTensor_map_spec_of_scalar_bound.