GraphData Backward Pass Link

This file lifts the dense-backward correctness theorem from plain graphs to GraphData, where the forward/backward closures carry an additional payload such as parameters or configuration data.

theorem Proofs.Autograd.Algebra.Graph.backwardDenseFrom_compileAuxData_eq_backpropAllCtx {α Δ : Type} [DecidableEq Spec.Shape] [CommSemiring α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TList α Γ) (d0 : Δ) (seed : TList α (Γ ++ ss)) : (compileAuxData g x d0).1.backwardDenseFrom seed.toAnyArray = Except.ok (g.backpropAllCtx x d0 seed).toAnyArray

Variant of backwardDenseFrom_compileAux_eq_backpropAllCtx for the GraphData interface.

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