NF Elementwise Bounds: Softplus and Safe Log

NFBackend.safeLog is a clamped log surrogate log (max x ε) with an unconditional forward bound.

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

• softplus(x) = log(1 + exp x) and 1 + exp x ≥ 1, so softplus = safeLog 1 (1 + exp x);
• safe_log(x) = log(softplus(x) + ε) and softplus(x) + ε ≥ ε, so safe_log = safeLog ε (softplus(x) + ε).

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

noncomputable def Proofs.RuntimeApprox.NFBackend.oneEps {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] : ℝ

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

noncomputable def Proofs.RuntimeApprox.NFBackend.expBoundScalar {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] (a eps : ℝ) : ℝ

Scalar forward-error envelope for exp.

This packages the exact value, the perturbed value at a + eps, and the final rounding budget into one reusable bound for the later softplus/safe-log proofs.

noncomputable def Proofs.RuntimeApprox.NFBackend.oneHat {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} : ℝ

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

noncomputable def Proofs.RuntimeApprox.NFBackend.expHat {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (a : ℝ) : ℝ

Rounded representation of exp a at the NF backend.

noncomputable def Proofs.RuntimeApprox.NFBackend.addHatSoftplus {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (a : ℝ) : ℝ

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

noncomputable def Proofs.RuntimeApprox.NFBackend.addBoundSoftplus {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (a eps : ℝ) : ℝ

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

noncomputable def Proofs.RuntimeApprox.NFBackend.softplusBoundScalar {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (a eps : ℝ) : ℝ

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

noncomputable def Proofs.RuntimeApprox.NFBackend.softplusR {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (xR : TorchLean.Floats.NF β fexp rnd) : TorchLean.Floats.NF β fexp rnd

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

theorem Proofs.RuntimeApprox.NFBackend.approx_softplus_nf {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {x : ℝ} {xR : TorchLean.Floats.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 {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (eps : ℝ) (xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s) : Spec.SpecTensor s

Per-entry bound tensor for softplusR.

This is the elementwise lifting of softplus_bound_scalar, used with linf_norm in approxT_softplus_spec.

theorem Proofs.RuntimeApprox.NFBackend.approxT_softplus_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.mapSpec Activation.Math.softplusSpec xS) (Spec.Tensor.mapSpec softplusR xR) (linfNorm (softplusBoundTensor eps xR))

approxT bound for softplus lifted to arbitrary tensor shapes.

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

noncomputable def Proofs.RuntimeApprox.NFBackend.safeLogSoftplusR {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} (ε : ℝ) (xR : TorchLean.Floats.NF β fexp rnd) : TorchLean.Floats.NF β fexp rnd

Runtime implementation of safe_log as a single rounded primitive.

theorem Proofs.RuntimeApprox.NFBackend.approx_safe_log_nf {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {x : ℝ} {xR : TorchLean.Floats.NF β fexp rnd} {eps ε : ℝ} (hε : 0 < ε) (hx : |toSpec xR - x| ≤ eps) : |toSpec (safeLogSoftplusR ε xR) - Activation.Math.safeLogSpec x ε| ≤ 1 / ε * eps + TorchLean.Floats.neuralUlp β fexp (Activation.Math.safeLogSpec (toSpec xR) ε) / 2

Forward approximation bound for the smooth safe_log activation in NF.

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

• one rounding step for safe_logR (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 {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {s : Spec.Shape} (ε eps : ℝ) (xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s) : Spec.SpecTensor s

Per-entry bound tensor for safe_log.

This is the elementwise lifting of approx_safe_log_nf's bound.

theorem Proofs.RuntimeApprox.NFBackend.approxT_safe_log_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {s : Spec.Shape} (ε : ℝ) (hε : 0 < ε) {xS : Spec.SpecTensor s} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) s} {eps : ℝ} : approxT toSpec xS xR eps → approxT toSpec (Spec.Tensor.mapSpec (fun (x : Spec.SpecScalar) => Activation.Math.safeLogSpec x ε) xS) (Spec.Tensor.mapSpec (safeLogSoftplusR ε) xR) (linfNorm (safeLogSoftplusBoundTensor ε eps xR))

approxT bound for safe_log lifted to arbitrary tensor shapes.

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