Higher derivatives of certified pullbacks

First-order graph certificates identify the real reverse pass with an adjoint Fréchet derivative. Jet preservation identifies nested-dual execution with repeated differentiation of that pass. Combining them proves higher-order reverse-mode correctness against mathlib, including smoothly varying output cotangents and arbitrary real normed parameter spaces.

Successful checked execution is connected to the same pure graph calculation. The derivative interpretation is exact-real; model recording must supply matching graphs and their local laws.

theorem Proofs.Autograd.Algebra.Graph.tangent_backprop_adjoint_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {Δ : Type} {Γ shapes : List Spec.Shape} (graph : Graph Δ Γ shapes) (nested : GraphData (Runtime.Autograd.Model.Dual.Nested ℝ n) Δ Γ shapes) (h : GraphData.PreservesPullbackJet E n graph.toData nested) (directions : Fin n → E) (x : E) (inputs : E → TorchLean.TensorPack ℝ Γ) (values : TorchLean.TensorPack (Runtime.Autograd.Model.Dual.Nested ℝ n) Γ) (data : Δ) (correct : GraphFDerivCorrect (graph.toReal data)) (hinputs : TorchLean.TensorPack.JetRelated directions x inputs values) (seed : E → TorchLean.TensorPack ℝ (Γ ++ shapes)) (seedValues : TorchLean.TensorPack (Runtime.Autograd.Model.Dual.Nested ℝ n) (Γ ++ shapes)) (hseed : TorchLean.TensorPack.JetRelated directions x seed seedValues) {shape : Spec.Shape} (input : Idx Γ shape) : Runtime.Autograd.Model.Dual.Nested.tangentTensor (getIdx (nested.backpropCtx values data seedValues) input) = (iteratedFDeriv ℝ n (fun (y : E) => getIdx (unflattenCtx ((ContinuousLinearMap.adjoint (fderiv ℝ (graph.toReal data).evalVec (flattenCtx (inputs y)))) (flattenCtx (seed y)))) input) x) directions

Nested-dual reverse execution computes every derivative of the exact adjoint derivative.

The first-order certificate identifies the real pullback with mathlib's fderiv; the jet laws then justify differentiating that pullback. Neither hypothesis can replace the other.

theorem Runtime.Autograd.Torch.TypedGraphWithData.tangent_forward {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {Δ : Type} {Γ : List Spec.Shape} {shape : Spec.Shape} (real : TypedGraphWithData ℝ Δ Γ shape) (nested : TypedGraphWithData (Model.Dual.Nested ℝ n) Δ Γ shape) (sameShapes : nested.nodeShapes = real.nodeShapes) (hgraph : Proofs.Autograd.Algebra.GraphData.PreservesJet E n real.data (sameShapes ▸ nested.data)) (sameOutput : sameShapes ▸ nested.output = real.output) (directions : Fin n → E) (x : E) (inputs : E → TorchLean.TensorPack ℝ Γ) (values : TorchLean.TensorPack (Model.Dual.Nested ℝ n) Γ) (data : Δ) (hinputs : TorchLean.TensorPack.JetRelated directions x inputs values) : Model.Dual.Nested.tangentTensor (nested.forward values data) = (iteratedFDeriv ℝ n (fun (y : E) => real.forward (inputs y) data) x) directions

Extracting a nested graph's output computes the iterated derivative of its real execution.

theorem Runtime.Autograd.Torch.TypedGraphWithData.tangent_vjp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {Δ : Type} {Γ : List Spec.Shape} {shape : Spec.Shape} (real : TypedGraphWithData ℝ Δ Γ shape) (nested : TypedGraphWithData (Model.Dual.Nested ℝ n) Δ Γ shape) (sameShapes : nested.nodeShapes = real.nodeShapes) (hgraph : Proofs.Autograd.Algebra.GraphData.PreservesPullbackJet E n real.data (sameShapes ▸ nested.data)) (sameOutput : sameShapes ▸ nested.output = real.output) (directions : Fin n → E) (x : E) (inputs : E → TorchLean.TensorPack ℝ Γ) (values : TorchLean.TensorPack (Model.Dual.Nested ℝ n) Γ) (data : Δ) (hinputs : TorchLean.TensorPack.JetRelated directions x inputs values) (seed : E → TorchLean.Tensor ℝ shape) (hseed : ContDiff ℝ (↑n) seed) {inputShape : Spec.Shape} (input : Proofs.Idx Γ inputShape) : Model.Dual.Nested.tangentTensor (Proofs.getIdx (nested.vjpWithSeed values data (Model.DualTensor.jet directions seed x)) input) = (iteratedFDeriv ℝ n (fun (y : E) => Proofs.getIdx (real.vjpWithSeed (inputs y) data (seed y)) input) x) directions

Every extracted input cotangent is the iterated derivative of the real typed graph's VJP.

The two runs must record the same node shapes and select the same output. Buffer observers do not enter this pure method. The seed can vary smoothly with the parameters being differentiated.

theorem Runtime.Autograd.Torch.TypedGraphWithData.tangent_vjpChecked {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {Δ : Type} {Γ : List Spec.Shape} {shape : Spec.Shape} (real : TypedGraphWithData ℝ Δ Γ shape) (nested : TypedGraphWithData (Model.Dual.Nested ℝ n) Δ Γ shape) (sameShapes : nested.nodeShapes = real.nodeShapes) (hgraph : Proofs.Autograd.Algebra.GraphData.PreservesPullbackJet E n real.data (sameShapes ▸ nested.data)) (sameOutput : sameShapes ▸ nested.output = real.output) (directions : Fin n → E) (x : E) (inputs : E → TorchLean.TensorPack ℝ Γ) (values : TorchLean.TensorPack (Model.Dual.Nested ℝ n) Γ) (data : Δ) (hinputs : TorchLean.TensorPack.JetRelated directions x inputs values) (seed : E → TorchLean.Tensor ℝ shape) (hseed : ContDiff ℝ (↑n) seed) (result : TorchLean.TensorPack (Model.Dual.Nested ℝ n) Γ × TorchLean.Tensor (Model.Dual.Nested ℝ n) shape) (checked : nested.vjpChecked values data (Model.DualTensor.jet directions seed x) = Except.ok result) {inputShape : Spec.Shape} (input : Proofs.Idx Γ inputShape) : Model.Dual.Nested.tangentTensor (Proofs.getIdx result.1 input) = (iteratedFDeriv ℝ n (fun (y : E) => Proofs.getIdx (real.vjpWithSeed (inputs y) data (seed y)) input) x) directions

A successful checked reverse pass has the same higher derivatives as the real pullback.

Validation is required at the nested input actually executed, not throughout a neighbourhood. Smoothness and the derivative interpretation come from the graph's separate jet certificate.

theorem Runtime.Autograd.Torch.TypedGraphWithData.tangent_vjpChecked_adjoint_fderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} {Δ : Type} {Γ : List Spec.Shape} {shape : Spec.Shape} (real : TypedGraphWithData ℝ Δ Γ shape) (nested : TypedGraphWithData (Model.Dual.Nested ℝ n) Δ Γ shape) (sameShapes : nested.nodeShapes = real.nodeShapes) (hgraph : Proofs.Autograd.Algebra.GraphData.PreservesPullbackJet E n real.data (sameShapes ▸ nested.data)) (sameOutput : sameShapes ▸ nested.output = real.output) (proofGraph : Proofs.Autograd.Algebra.Graph Δ Γ real.nodeShapes) (same : proofGraph.toData = real.data) (directions : Fin n → E) (x : E) (inputs : E → TorchLean.TensorPack ℝ Γ) (values : TorchLean.TensorPack (Model.Dual.Nested ℝ n) Γ) (data : Δ) (correct : (y : E) → Proofs.Autograd.GraphFDerivCorrectAt (proofGraph.toReal data) (Proofs.Autograd.flattenCtx (inputs y))) (hinputs : TorchLean.TensorPack.JetRelated directions x inputs values) (seed : E → TorchLean.Tensor ℝ shape) (hseed : ContDiff ℝ (↑n) seed) (result : TorchLean.TensorPack (Model.Dual.Nested ℝ n) Γ × TorchLean.Tensor (Model.Dual.Nested ℝ n) shape) (checked : nested.vjpChecked values data (Model.DualTensor.jet directions seed x) = Except.ok result) {inputShape : Spec.Shape} (input : Proofs.Idx Γ inputShape) : Model.Dual.Nested.tangentTensor (Proofs.getIdx result.1 input) = (iteratedFDeriv ℝ n (fun (y : E) => Proofs.getIdx (Proofs.Autograd.unflattenCtx ((ContinuousLinearMap.adjoint (fderiv ℝ (fun (z : Proofs.Autograd.CtxVec Γ) => Proofs.Autograd.tensorToVec (real.forward (Proofs.Autograd.unflattenCtx z) data)) (Proofs.Autograd.flattenCtx (inputs y)))) (Proofs.Autograd.tensorToVec (seed y)))) input) x) directions

Checked nested execution differentiates the adjoint of the selected forward derivative.

The first-order proof is needed at each input in the smooth family. Runtime validation is only needed for the particular nested execution returning result. These are separate obligations.

theorem Runtime.Autograd.Torch.TypedGraphWithData.tangent_vjpChecked_iteratedFDeriv {n : ℕ} {Δ : Type} {Γ : List Spec.Shape} {shape : Spec.Shape} (real : TypedGraphWithData ℝ Δ Γ shape) (nested : TypedGraphWithData (Model.Dual.Nested ℝ n) Δ Γ shape) (sameShapes : nested.nodeShapes = real.nodeShapes) (hgraph : Proofs.Autograd.Algebra.GraphData.PreservesPullbackJet (Proofs.Autograd.CtxVec Γ) n real.data (sameShapes ▸ nested.data)) (sameOutput : sameShapes ▸ nested.output = real.output) (proofGraph : Proofs.Autograd.Algebra.Graph Δ Γ real.nodeShapes) (same : proofGraph.toData = real.data) (directions : Fin n → Proofs.Autograd.CtxVec Γ) (x : Proofs.Autograd.CtxVec Γ) (values : TorchLean.TensorPack (Model.Dual.Nested ℝ n) Γ) (data : Δ) (correct : (y : Proofs.Autograd.CtxVec Γ) → Proofs.Autograd.GraphFDerivCorrectAt (proofGraph.toReal data) y) (hinputs : TorchLean.TensorPack.JetRelated directions x Proofs.Autograd.unflattenCtx values) (smooth : ContDiff ℝ (↑n + 1) fun (z : Proofs.Autograd.CtxVec Γ) => Proofs.Autograd.tensorToVec (real.forward (Proofs.Autograd.unflattenCtx z) data)) (seed : TorchLean.Tensor ℝ shape) (result : TorchLean.TensorPack (Model.Dual.Nested ℝ n) Γ × TorchLean.Tensor (Model.Dual.Nested ℝ n) shape) (checked : nested.vjpChecked values data (TorchLean.Tensor.map (Model.Dual.Nested.ofPrimal n) seed) = Except.ok result) {inputShape : Spec.Shape} (input : Proofs.Idx Γ inputShape) : Model.Dual.Nested.tangentTensor (Proofs.getIdx result.1 input) = Proofs.getIdx (Proofs.Autograd.unflattenCtx ((ContinuousLinearMap.adjoint (fderiv ℝ (fun (y : Proofs.Autograd.CtxVec Γ) => (iteratedFDeriv ℝ n (fun (z : Proofs.Autograd.CtxVec Γ) => Proofs.Autograd.tensorToVec (real.forward (Proofs.Autograd.unflattenCtx z) data)) y) directions) x)) (Proofs.Autograd.tensorToVec seed))) input

Checked nested reverse execution computes the pullback of any fixed higher derivative.

All context entries, including parameters, can occur in the direction tuple. Holding the output cotangent fixed is essential: a varying cotangent contributes additional derivative terms. The forward map must be C^(n+1) to interchange the reverse derivative with the n directions.