Functional transcendentals + scalar-affine: proofs and runtime regression checks

Positive / negative example for the nn.functional.{exp, log, scale, shift, affine} ops added for scientific forward models — e.g. the soil-moisture retrieval that combines SMAP (Soil Moisture Active Passive) and NISAR (NASA–ISRO Synthetic Aperture Radar) observations through the AVS (Attenuation–Volume–Surface) model, whose surface term is $\exp(-2b\,\mathrm{NDVI})\,c\,|R|^2$.

The point is that these ops are differentiated by the autograd engine, so a forward model written once yields its gradient with no hand-coded derivative. This file has two layers:

• a proof layer handle for the real-valued exp op, using Proofs.Autograd.OpSpecFDerivCorrect.exp and the generic backward_eq_adjoint_fderiv theorem;
• runtime regression checks that differentiate tiny Float functions and compare the autograd gradient to the closed form.

The runtime checks below are not the proof. They make sure the executable tape path used by scientific examples still follows the expected derivative numerically. The proof layer declarations show where the corresponding theorem-backed op-spec story lives.

Each runtime check differentiates a tiny function and compares the autograd gradient to the closed form:

• positive controls — the gradient matches the analytic value;
• negative controls — a deliberately wrong analytic value (notably the wrong-sign gradient of $\exp(-2x)$) does not match. That is exactly the defect class — a sign/factor error in a hand-coded Jacobian — that deriving the gradient by autograd eliminates.

checkAll runs as a compiled executable — lake exe transcendentals_check — and exits non-zero on any regression. It is deliberately not an #eval check: autograd uses the native tape externs, which the interpreter cannot load (see the main entry point below).

Proof objects and runtime checks

noncomputable def NN.Examples.Functional.Transcendentals.expProofSurface : Proofs.Autograd.OpSpecFDerivCorrect 1 1

The theorem-backed real-valued exp op used by the proof layer.

This is the actual proof layer object: it packages the forward op, its JVP, a Fréchet-derivative candidate, and the theorem that the JVP is the true derivative. The runtime checks below exercise the executable Float tape; this declaration points to the corresponding real-valued theorem.

theorem NN.Examples.Functional.Transcendentals.expBackward_eq_adjoint_fderiv (x δ : Spec.Tensor ℝ (Spec.Shape.dim 1 Spec.Shape.scalar)) : Proofs.Autograd.toVecE (expProofSurface.correct.op.backward x δ) = (Proofs.Autograd.vjp expProofSurface.forwardVec (Proofs.Autograd.toVecE x)) (Proofs.Autograd.toVecE δ)

For scalar exp over ℝ, the proved backward rule is the adjoint of the Fréchet derivative.

This is the theorem-level statement that the executable regression check is meant to complement.

Functions under test (written once; gradients come from autograd)

def NN.Examples.Functional.Transcendentals.expFn : TorchLean.autograd.func.Fn Spec.Shape.scalar Spec.Shape.scalar

$f(x)=e^x$.

def NN.Examples.Functional.Transcendentals.expNegativeTwoFn : TorchLean.autograd.func.Fn Spec.Shape.scalar Spec.Shape.scalar

$f(x)=e^{-2x}$ — the shape of the AVS canopy two-way transmittance as a function of the attenuation parameter.

def NN.Examples.Functional.Transcendentals.affineFn : TorchLean.autograd.func.Fn Spec.Shape.scalar Spec.Shape.scalar

$f(x)=3x+1$ via the scalar-affine op.

Float checks

def NN.Examples.Functional.Transcendentals.approx (a b : Float) (tol : Float := 1e-6) : Bool

Absolute-tolerance float compare.

def NN.Examples.Functional.Transcendentals.expectGrad (name : String) (got expected : Float) (tol : Float := 1e-6) : IO Unit

Positive control: name's autograd gradient is approximately equal to the expected value; throws on mismatch.

def NN.Examples.Functional.Transcendentals.expectNot (name : String) (got wrong : Float) (tol : Float := 1e-6) : IO Unit

Negative control: the gradient must not equal wrong; throws if it does.

def NN.Examples.Functional.Transcendentals.gradAt (f : TorchLean.autograd.func.Fn Spec.Shape.scalar Spec.Shape.scalar) (x0 : Float) : IO Float

Differentiate a scalar→scalar Fn at a Float point, returning the gradient.

def NN.Examples.Functional.Transcendentals.checkAll : IO Unit

def main : IO Unit

Compiled entry point. Autograd uses the native runtime, so this runs as a compiled lean_exe (lake exe transcendentals_check), not via #eval (the interpreter cannot load native tape externs).