Reverse execution over saved node programs uses indexed gradients and deferred uniform updates. The all-seeds pass is proved equal to dense backpropagation without assuming associativity, zero identities, or that a VJP maps the zero cotangent to zero. The separate single-output pass omits unrelated nodes; these two semantics need not agree for arbitrary user-defined VJPs.

def Proofs.Autograd.Algebra.PreparedNode.accumulate {α : Type} [TorchLean.Storage α] [Add α] [DecidableEq α] {shapes : List Spec.Shape} {shape : Spec.Shape} (node : PreparedNode α shapes shape) (seed : TorchLean.Tensor α shape) (ctx : GradientContext α shapes) : GradientContext α shapes

Evaluate every VJP, selecting its certified compact program when available.

theorem Proofs.Autograd.Algebra.PreparedNode.toPack_accumulate {α : Type} [TorchLean.Storage α] [Add α] [DecidableEq α] {shapes : List Spec.Shape} {shape : Spec.Shape} (node : PreparedNode α shapes shape) (seed : TorchLean.Tensor α shape) (ctx : GradientContext α shapes) : (node.accumulate seed ctx).toPack = ctx.toPack.add (node.vjp seed)

Either execution path adds exactly the complete dense contribution.

def Proofs.Autograd.Algebra.SavedGraph.backpropArray {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} [DecidableEq α] {ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : GradientContext α (Γ ++ ss)) : TensorContext α (Γ ++ ss)

Reverse traversal finalizes one output gradient before continuing with the active prefix.

theorem Proofs.Autograd.Algebra.SavedGraph.toPack_backpropArray {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} [DecidableEq α] {ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : GradientContext α (Γ ++ ss)) : (saved.backpropArray seed).toPack = saved.backpropDense seed.toPack

Indexed reverse traversal returns every dense gradient in precisely the same order.

theorem Proofs.Autograd.Algebra.SavedGraph.ofGraph_backpropArray {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} [DecidableEq α] {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : ((ofGraph graph inputs data).1.backpropArray (GradientContext.ofPack seed)).toPack = graph.backpropAllCtx inputs data seed

Prepared array backpropagation preserves full graph semantics for arbitrary seed packs.

def Proofs.Autograd.Algebra.SavedGraph.backpropStored {α : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TensorContext α (Γ ++ ss)

Use certified equality when the scalar storage provides it. Other carriers retain the exact dense program, so the generic interface needs no additional scalar hypotheses.

theorem Proofs.Autograd.Algebra.SavedGraph.toPack_backpropStored {α : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : TorchLean.TensorPack α (Γ ++ ss)) : (saved.backpropStored seed).toPack = saved.backpropDense seed

Backend selection preserves the complete reverse program for every scalar storage.

theorem Proofs.Autograd.Algebra.SavedGraph.ofGraph_backpropStored {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : ((ofGraph graph inputs data).1.backpropStored seed).toPack = graph.backpropAllCtx inputs data seed

Stored reverse execution agrees with the original graph for every seed and scalar backend.

def Proofs.Autograd.Algebra.SavedGraph.Internal.backpropReachableArray {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} [DecidableEq α] [Zero α] {ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : GradientContext α (Γ ++ ss)) (reached : Array Bool) : TensorContext α (Γ ++ ss)

Visit only dependencies of the seeded output when a node has a certified compact support. An opaque dense VJP conservatively makes every preceding position reachable. Reachability follows the prepared VJP's support: a reached node still runs when its cotangent happens to be zero.

def Proofs.Autograd.Algebra.SavedGraph.backpropFrom {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} [Zero α] {ss : List Spec.Shape} {shape : Spec.Shape} (saved : SavedGraph α Γ ss) (output : Idx (Γ ++ ss) shape) (seed : TorchLean.Tensor α shape) : TensorContext α (Γ ++ ss)

Backpropagate from one output using certified support when storage equality is available.

Storage equality compares carrier encodings, not the scalar's numerical BEq; IEEE signed zeros and NaNs therefore do not invalidate the support check. Carriers without decidable storage equality retain the full dense program. backpropStored remains the explicit all-seeds reference. Opaque VJPs conservatively visit the full prefix. Custom compact VJPs supply their own support; this traversal makes no separate claim that it captures the syntactic dependencies of an arbitrary user-defined forward function.

def Proofs.Autograd.Algebra.SavedGraph.backpropInputsDense {α : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TorchLean.TensorPack α Γ

Dense inputs-only reference, retaining the original local accumulation order.

theorem Proofs.Autograd.Algebra.SavedGraph.ofGraph_backpropInputsDense {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} {Δ : Type} {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : (ofGraph graph inputs data).1.backpropInputsDense seed = graph.backpropCtx inputs data seed

Saving primals also preserves the original inputs-only VJP for every seed.

def Proofs.Autograd.Algebra.SavedGraph.backpropInputsArray {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} [DecidableEq α] {ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : GradientContext α (Γ ++ ss)) : TorchLean.TensorPack α Γ

Inputs-only reverse traversal releases finalized intermediate gradients immediately.

theorem Proofs.Autograd.Algebra.SavedGraph.backpropInputsArray_eq {α : Type} [TorchLean.Storage α] [Add α] {Γ : List Spec.Shape} [DecidableEq α] {ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : GradientContext α (Γ ++ ss)) : saved.backpropInputsArray seed = saved.backpropInputsDense seed.toPack

Dropping finalized intermediates preserves the complete inputs-only result.

def Proofs.Autograd.Algebra.SavedGraph.backpropInputsStored {α : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TorchLean.TensorPack α Γ

Select the certified indexed implementation without strengthening the scalar interface.

theorem Proofs.Autograd.Algebra.SavedGraph.backpropInputsStored_eq {α : Type} [TorchLean.Storage α] [Add α] {Γ ss : List Spec.Shape} (saved : SavedGraph α Γ ss) (seed : TorchLean.TensorPack α (Γ ++ ss)) : saved.backpropInputsStored seed = saved.backpropInputsDense seed

Both storage choices compute the same ordered inputs-only reverse program.

def Proofs.Autograd.Algebra.GraphData.backpropCtxSaved {α : Type} [TorchLean.Storage α] {Δ : Type} {Γ : List Spec.Shape} [Add α] {ss : List Spec.Shape} (graph : GraphData α Δ Γ ss) (inputs : TorchLean.TensorPack α Γ) (data : Δ) (seed : TorchLean.TensorPack α (Γ ++ ss)) : TorchLean.TensorPack α Γ

Save one primal execution and compute its input pullback using indexed gradients.

@[csimp]

theorem Proofs.Autograd.Algebra.GraphData.backpropCtx_eq_saved : @backpropCtx = @backpropCtxSaved

The ordinary pure VJP API compiles to the proved saved-program implementation.