NF Elementwise Bounds: Softplus and Safe Log

softplusR rounds the constant, exponential, addition, and clamped logarithm separately. In contrast, safeLogSoftplusR rounds the entire exact smooth activation once. These are different numerical schedules; neither definition executes a native kernel.

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.

theorem Proofs.RuntimeApprox.NFBackend.oneEps_nonneg {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] : 0 ≤ oneEps

oneEps is a half ulp, hence nonnegative.

theorem Proofs.RuntimeApprox.NFBackend.abs_toSpec_one_sub_one_le {β : FloatLib.Numerics.Radix} {fexp : ℤ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidExp fexp] {rnd : ℝ → ℤ} [FloatLib.Floats.Formats.Flocq.ValidRndToNearest rnd] : |toSpec 1 - 1| ≤ oneEps

The rounded constant 1 : NF is within oneEps of the real 1.

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.

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.map Activation.Math.softplusSpec xS) (TorchLean.Tensor.map 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

Rounded-real model of log (softplus x + ε), with one rounding of the entire expression. This is not the staged composition of softplusR, addition, and safeLogR.

theorem Proofs.RuntimeApprox.NFBackend.approx_safeLogSoftplus_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 safeLogSoftplusR (defined as NF.ofReal (safeLogSpec ...));
• 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 safeLogSoftplusR.

This is the elementwise lifting of approx_safeLogSoftplus_nf's bound.

theorem Proofs.RuntimeApprox.NFBackend.approxTensor_safeLogSoftplus_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.map (fun (x : ℝ) => Activation.Math.safeLogSpec x ε) xS) (TorchLean.Tensor.map (safeLogSoftplusR ε) xR) (linfNorm (safeLogSoftplusBoundTensor ε eps xR))

approxTensor bound for the smooth safeLogSpec lifted to arbitrary tensor shapes.

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