Correctness of checked differentiation

The public autograd transforms run domain validation, lower a graph to a tape, sweep its stored reverse rules, and recover the typed input gradients from a heterogeneous array. The theorems here connect that complete checked path to the graph semantics and, for analytically correct real graphs, to mathlib's Fréchet derivative. Validation remains a separate hypothesis: passing a runtime domain check alone is not a derivative-correctness certificate.

theorem Runtime.Autograd.Torch.TypedGraphWithData.vjpChecked_eq {α Δ : Type} [TorchLean.Storage α] [Add α] [Zero α] {Γ : List Spec.Shape} {τ : Spec.Shape} (graph : TypedGraphWithData α Δ Γ τ) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (seed : TorchLean.Tensor α τ) (result : Tape α × TorchLean.TensorPack α (Γ ++ graph.nodeShapes)) (checked : TypedGraph.lowerToTapeChecked graph.data inputs data = Except.ok result) : graph.vjpChecked inputs data seed = Except.ok (graph.vjpWithSeed inputs data seed, graph.forward inputs data)

Successful validation makes the checked VJP agree with the stored graph reverse rules. This preserves the order of additions and requires no algebraic laws on the scalar backend.

theorem Runtime.Autograd.Torch.TypedGraphWithData.hasFDerivAt_forward {Δ : Type} {Γ : List Spec.Shape} {τ : Spec.Shape} (graph : TypedGraphWithData ℝ Δ Γ τ) (proofGraph : Proofs.Autograd.Algebra.Graph Δ Γ graph.nodeShapes) (same : proofGraph.toData = graph.data) (inputs : TorchLean.TensorPack ℝ Γ) (data : Δ) (correct : Proofs.Autograd.GraphFDerivCorrectAt (proofGraph.toReal data) (Proofs.Autograd.flattenCtx inputs)) : HasFDerivAt (fun (x : Proofs.Autograd.CtxVec Γ) => Proofs.Autograd.tensorToVec (graph.forward (Proofs.Autograd.unflattenCtx x) data)) (Proofs.Autograd.CtxVec.getCLM graph.output ∘SL fderiv ℝ (proofGraph.toReal data).evalVec (Proofs.Autograd.flattenCtx inputs)) (Proofs.Autograd.flattenCtx inputs)

The selected output has the derivative obtained by projecting the graph derivative.

theorem Runtime.Autograd.Torch.TypedGraphWithData.jvpChecked_fderiv {Δ : Type} {Γ : List Spec.Shape} {τ : Spec.Shape} (graph : TypedGraphWithData ℝ Δ Γ τ) (proofGraph : Proofs.Autograd.Algebra.Graph Δ Γ graph.nodeShapes) (same : proofGraph.toData = graph.data) (inputs tangents : TorchLean.TensorPack ℝ Γ) (data : Δ) (correct : Proofs.Autograd.GraphFDerivCorrectAt (proofGraph.toReal data) (Proofs.Autograd.flattenCtx inputs)) (result : TorchLean.TensorPack ℝ (Γ ++ graph.nodeShapes) × TorchLean.TensorPack ℝ (Γ ++ graph.nodeShapes)) (checked : TypedGraph.jvpChecked graph.data inputs tangents data = Except.ok result) : Proofs.Autograd.tensorToVec (Proofs.getIdx result.2 graph.output) = (fderiv ℝ (fun (x : Proofs.Autograd.CtxVec Γ) => Proofs.Autograd.tensorToVec (graph.forward (Proofs.Autograd.unflattenCtx x) data)) (Proofs.Autograd.flattenCtx inputs)) (Proofs.Autograd.flattenCtx tangents)

The checked forward-mode tangent is mathlib's derivative applied to the input direction.

theorem Runtime.Autograd.Torch.TypedGraphWithData.vjpWithSeed_adjoint_fderiv {Δ : Type} {Γ : List Spec.Shape} {τ : Spec.Shape} (graph : TypedGraphWithData ℝ Δ Γ τ) (proofGraph : Proofs.Autograd.Algebra.Graph Δ Γ graph.nodeShapes) (same : proofGraph.toData = graph.data) (inputs : TorchLean.TensorPack ℝ Γ) (data : Δ) (seed : TorchLean.Tensor ℝ τ) (correct : Proofs.Autograd.GraphFDerivCorrectAt (proofGraph.toReal data) (Proofs.Autograd.flattenCtx inputs)) : Proofs.Autograd.flattenCtx (graph.vjpWithSeed inputs data seed) = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (x : Proofs.Autograd.CtxVec Γ) => Proofs.Autograd.tensorToVec (graph.forward (Proofs.Autograd.unflattenCtx x) data)) (Proofs.Autograd.flattenCtx inputs))) (Proofs.Autograd.tensorToVec seed)

The pure graph pullback is the adjoint derivative of its selected output.

theorem Runtime.Autograd.Torch.TypedGraphWithData.vjpChecked_adjoint_fderiv {Δ : Type} {Γ : List Spec.Shape} {τ : Spec.Shape} (graph : TypedGraphWithData ℝ Δ Γ τ) (proofGraph : Proofs.Autograd.Algebra.Graph Δ Γ graph.nodeShapes) (same : proofGraph.toData = graph.data) (inputs : TorchLean.TensorPack ℝ Γ) (data : Δ) (seed : TorchLean.Tensor ℝ τ) (correct : Proofs.Autograd.GraphFDerivCorrectAt (proofGraph.toReal data) (Proofs.Autograd.flattenCtx inputs)) (result : TorchLean.TensorPack ℝ Γ × TorchLean.Tensor ℝ τ) (checked : graph.vjpChecked inputs data seed = Except.ok result) : Proofs.Autograd.flattenCtx result.1 = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (x : Proofs.Autograd.CtxVec Γ) => Proofs.Autograd.tensorToVec (graph.forward (Proofs.Autograd.unflattenCtx x) data)) (Proofs.Autograd.flattenCtx inputs))) (Proofs.Autograd.tensorToVec seed)

The checked API returns the adjoint of mathlib's derivative of its selected forward output.

The proof graph must describe the exact operation data that execution uses. Differentiability is required only at this input and the corresponding intermediate values. The carrier is ℝ; floating-point error and native kernels are not identified with exact real arithmetic.