Correctness of checked differentiation

The public autograd transforms validate and evaluate the graph before sweeping saved reverse rules from its selected output. The theorems here connect that 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 (Spec.SomeTensor α) × TorchLean.TensorPack α (Γ ++ graph.nodeShapes)) (checked : TypedGraph.lowerToTapeChecked graph.data inputs data = Except.ok result) : graph.vjpChecked inputs data seed = Except.ok (graph.vjp inputs data seed, graph.forward inputs data)

Successful validation makes the checked VJP agree with the stored graph reverse rules. This requires no algebraic laws on the scalar backend. The single-output API uses certified support when available, rather than claiming equality with an arbitrary dense all-seeds VJP.

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

A successful checked reverse pass returns the graph pullback and forward value. Validation is required at the input actually executed; no scalar algebraic laws are needed.

theorem Runtime.Autograd.Torch.TypedGraphWithData.vjp_eq_backpropCtx {α Δ : Type} [TorchLean.Storage α] [Add α] [Zero α] {Γ : List Spec.Shape} {τ : Spec.Shape} (graph : TypedGraphWithData α Δ Γ τ) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (seed : TorchLean.Tensor α τ) (equality : TorchLean.Storage.decEq? = none) : graph.vjp inputs data seed = graph.data.backpropCtx inputs data (Proofs.Autograd.Algebra.TensorPack.single graph.output seed)

Without storage equality, single-output differentiation retains the exact dense reference. This connects real-valued and symbolic carriers to the existing derivative theorems.

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.vjp_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.vjp 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.