Dense Runtime Backward Pass Link

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

The proof is an induction on the graph. The nil case is backwardDenseFrom_addLeaves_empty (the loop is the identity on a leaf-only tape) and the snoc case is backwardDenseFrom_addNode_lowerNode, instantiated with the forward-pass facts about the lowered prefix from Link.Core and Link.Invariants.

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

Main runtime/link theorem: running the runtime dense backward loop on a tape produced by lowerGraphToTape 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.