GraphData Backward Pass Link

This file states the dense-backward correctness theorem for GraphData, where the forward/backward closures carry an additional payload such as parameters or configuration data.

The proof has the same two cases as backwardDenseFrom_lowerGraphToTape_eq_backpropAllCtx and uses the same shared lemmas, backwardDenseFrom_addLeaves_empty and backwardDenseFrom_addNode_lowerNode; only the forward-pass facts about the lowered prefix come from the GraphData lemmas of Link.Core and Link.Invariants.

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_lowerGraphDataToTape_eq_backpropAllCtx {α Δ : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d0 : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : (lowerGraphDataToTape g x d0).1.backwardDenseFrom seed.toShapeErasedArray = Except.ok (g.backpropAllCtx x d0 seed).toShapeErasedArray

Variant of backwardDenseFrom_lowerGraphToTape_eq_backpropAllCtx for the GraphData interface.

This is useful when a graph carries extra payload Δ (e.g. parameters/config) through forward and backward closures.