OpSpec

Generic analytic (HasFDerivAt/fderiv) soundness for composed Spec.OpSpecs.

NN.Proofs.Autograd.FDeriv.Core proves the first end-to-end instance (a 2-layer MLP) by:

1. proving OpSpecCorrect (dot/JVP/VJP adjointness), and
2. identifying the JVP with the Fréchet derivative.

This file packages (2) as an extra field and shows it is closed under OpSpecCorrect.compose.

Result: once primitive ops have analytic JVP facts, any sequential OpSpec graph built by composition gets the theorem:

backward x δ = VJP[forward, x] δ (after converting tensors ↔ Euclidean vectors).

Basic tensor/vector roundtrip

Most analytic statements here are written in Euclidean space (Vec n) because Mathlib’s fderiv and adjoint API lives there. The following lemma just re-exports the ofFnE/getScalarE roundtrip in a form that is convenient for rewriting.

@[simp]

theorem Proofs.Autograd.ofFnE_getScalar {n : ℕ} (t : TorchLean.Tensor ℝ [n]) : ofFnE (getScalarE t) = t

structure Proofs.Autograd.OpSpecFDerivCorrect (inDim outDim : ℕ) : Type

A proved OpSpec (OpSpecCorrect) together with the analytic fact that its JVP is fderiv.

This is the “bridge object” that upgrades dot-level correctness (JVP/VJP adjointness) into an actual HasFDerivAt statement about the forward function on Vec n.

PyTorch analogy: this corresponds to saying “the local backward rule is the transpose Jacobian of the true derivative” for a primitive op, so that composing ops yields correct global backward.

• correct : OpSpecCorrect (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)

  The op together with its JVP and the VJP/JVP adjointness proof.

• deriv : Vec inDim → Vec inDim →L[ℝ] Vec outDim

  The Frechet derivative of the forward map at each point, as a continuous linear map.

• hasFDerivAt (xV : Vec inDim) : HasFDerivAt (fun (xV : Vec inDim) => getScalarE (self.correct.op.forward (ofFnE xV))) (self.deriv xV) xV

  The forward map on Vec inDim is differentiable everywhere with derivative deriv.

• jvp_eq (xV dxV : Vec inDim) : getScalarE (self.correct.jvp (ofFnE xV) (ofFnE dxV)) = (self.deriv xV) dxV

  The JVP of the op agrees with deriv applied to the tangent vector.

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.forwardVec {inDim outDim : ℕ} (C : OpSpecFDerivCorrect inDim outDim) : Vec inDim → Vec outDim

The induced forward function on Euclidean vectors.

theorem Proofs.Autograd.OpSpecFDerivCorrect.backward_eq_adjoint_fderiv {inDim outDim : ℕ} (C : OpSpecFDerivCorrect inDim outDim) (x : TorchLean.Tensor ℝ [inDim]) (δ : TorchLean.Tensor ℝ [outDim]) : getScalarE (C.correct.op.backward x δ) = (vjp C.forwardVec (getScalarE x)) (getScalarE δ)

Main analytic soundness statement for a single OpSpecFDerivCorrect:

backward x δ is the adjoint of the Fréchet derivative of the forward map, applied to δ.

This is the analytic justification for reverse-mode: it says the implemented VJP is the true Jacobian-transpose product.

noncomputable def Proofs.Autograd.OpSpecFDerivCorrect.compose {inDim midDim outDim : ℕ} (f : OpSpecFDerivCorrect inDim midDim) (g : OpSpecFDerivCorrect midDim outDim) : OpSpecFDerivCorrect inDim outDim

Composition preserves analytic correctness (chain rule).

If f and g each have a correct fderiv identification of their JVP, then g ∘ f does too. This is the key closure property used to scale from primitive ops to sequential models.