Checked differentiation of composed, proved graphs

DGraph already stores the primitive derivative proofs and preserves them under composition. Selecting an output now gives the same typed graph that the runtime differentiates. The VJP theorem uses the stored certificates, so a new composition needs no separate backpropagation proof. Runtime domain validation is still allowed to reject an input.

These are exact-real semantics. They do not certify floating-point rounding or the nested-dual implementation of higher derivatives.

def Proofs.Autograd.DGraph.toTypedGraph {Γ ss : List Spec.Shape} {τ : Spec.Shape} (graph : DGraph Γ ss) (output : Idx (Γ ++ ss) τ) : Runtime.Autograd.Torch.TypedGraph ℝ Γ τ

Select an output of a proved graph for the checked runtime, preserving all node data.

theorem Proofs.Autograd.DGraph.vjpChecked_adjoint_fderiv {Γ ss : List Spec.Shape} {τ : Spec.Shape} (graph : DGraph Γ ss) (output : Idx (Γ ++ ss) τ) (inputs : TorchLean.TensorPack ℝ Γ) (seed : TorchLean.Tensor ℝ τ) (result : TorchLean.TensorPack ℝ Γ × TorchLean.Tensor ℝ τ) (checked : Runtime.Autograd.Torch.TypedGraphWithData.vjpChecked (graph.toTypedGraph output) inputs () seed = Except.ok result) : flattenCtx result.1 = (ContinuousLinearMap.adjoint (fderiv ℝ (fun (x : CtxVec Γ) => tensorToVec ((graph.toTypedGraph output).forward (unflattenCtx x))) (flattenCtx inputs))) (tensorToVec seed)

A successful pullback of a composed graph inherits its stored primitive derivative proofs.