Differentiate three scalar functions

Run scripts/lake.sh exe torchlean transcendentals to compare autograd with hand-computed derivatives:

• exp x has derivative exp x;
• 3 * x + 1 has derivative 3;
• exp (-2 * x) has derivative -2 * exp (-2 * x) by the chain rule.

All three are evaluated at x = 0.5 using Float and absolute tolerance 1e-6. Each check also rejects a named wrong answer. In particular, the last one distinguishes a missing minus sign from rounding error. Every check should print PASS or PASS-NEG; a mismatch exits with an error. No dataset or GPU is needed.

expSpec and exp_backward_eq_adjoint_fderiv give the separate real-arithmetic theorem. The executable comparisons test the Float tape on these inputs; they do not prove its native implementation or establish a derivative at every input. Read exponential, then grad, then run for the application flow.

Proof objects and runtime checks

noncomputable def NN.Examples.Functional.Transcendentals.expSpec : 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.exp_backward_eq_adjoint_fderiv (x δ : TorchLean.Tensor ℝ [1]) : Proofs.Autograd.getScalarE (expSpec.correct.op.backward x δ) = (Proofs.Autograd.vjp expSpec.forwardVec (Proofs.Autograd.getScalarE x)) (Proofs.Autograd.getScalarE δ)

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.exponential (scale : ℤ := 1) : TorchLean.autograd.Function [] []

$f(x)=e^{\mathrm{scale}\,x}$ for any integer scale.

The default uses the exponential directly, without adding an identity-scale node to the tape. Other scales are converted through the scalar backend's natural-number and negation operations.

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.grad (f : TorchLean.autograd.Function [] []) (x0 : Float) : IO Float

Evaluate the scalar derivative at a Float input; extract its entry for printing.

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

Compare each derivative with its analytic value and reject a plausible wrong value.

The positive checks establish agreement at the sampled point; the negative controls show that those points and tolerances distinguish the particular mistakes named below.

def NN.Examples.Functional.Transcendentals.usage : String

Command-line help for the transcendental autograd checks.

def NN.Examples.Functional.Transcendentals.main (args : List String) : IO Unit

Entry point.