Dense Runtime Backward Pass Link

This file proves that the executable dense backward loop on a lowered tape agrees with the proof-level full backpropagation backpropAllCtx. It is the main bridge between the runtime tape engine and the algebraic reverse-mode model.

The theorem is stated for GraphData, which stores executable forward and backward functions and needs only Storage and Add on the scalar. 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. A proved Graph lowers through Graph.toData, so its theorem is the GraphData one applied to g.toData.

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

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

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

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

The same statement for a proved graph, which lowers through g.toData.