Higher derivatives through the model API

The public transforms lower a model, embed fixed state, and seed input directions. The forward theorem connects coefficient extraction to mathlib's iterated derivative. Model.Reverse also connects the returned state and input gradients to its pullback. Their hypotheses identify the recorded graph and certify its operations; successful recording alone does not imply differentiability.

theorem TorchLean.nn.TypedGraphModel.forward_empty {σ τ : Shape} {α : Type} [Storage α] (model : TypedGraphModel [] σ τ α) (state : State α []) (input : Tensor α σ) : model.forward state input = Runtime.Autograd.Torch.TypedGraph.forward model (TensorPack.singleton input)

A model with no state tensors evaluates on its input alone, regardless of the empty state value. This equation lets clients reason about execution without unpacking the opaque state wrapper.

theorem TorchLean.autograd.model.derivative_eq {σ τ : Shape} (model : nn.Sequential σ τ) (state : State model ℝ) (input : Tensor ℝ σ) (directions : List (Tensor ℝ σ)) (real : nn.TypedGraphModel (Runtime.Autograd.Model.Layers.Seq.stateShapes model) σ τ ℝ) (nested : nn.TypedGraphModel (Runtime.Autograd.Model.Layers.Seq.stateShapes model) σ τ (Runtime.Autograd.Model.Dual.Nested ℝ directions.length)) (lowered : Runtime.Autograd.Model.Layers.Seq.lowerToTypedGraph model Runtime.Autograd.Model.Layers.Mode.eval = pure nested) (sameShapes : nested.nodeShapes = real.nodeShapes) (hgraph : Proofs.Autograd.Algebra.GraphData.PreservesJet (Tensor ℝ σ) directions.length real.data (sameShapes ▸ nested.data)) (sameOutput : sameShapes ▸ nested.output = real.output) : derivative model state input directions = pure ((iteratedFDeriv ℝ directions.length (fun (y : Tensor ℝ σ) => real.forward state y) input) fun (i : Fin directions.length) => directions[i])

Successful certified lowering makes model.derivative compute the iterated Fréchet derivative.

State is fixed, directions can repeat, and the list length is the derivative order. real supplies the reference function, while the jet certificate relates every recorded operation to the nested graph actually returned by the IO lowering call. No assumption identifies native floats with reals.