Dense Runtime Backward Pass Link

This file proves that the executable dense backward loop produced by graph compilation agrees with the proof-level backpropAllCtx semantics. It is the main bridge between the runtime tape engine and the algebraic reverse-mode model.

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

Main runtime/link theorem: running the runtime dense backward loop on a tape produced by compileAux matches the proved “full backpropagation” backpropAllCtx.

This is the formal statement that the executable engine implements the same reverse-mode accumulation semantics as the proved tape model.