Dense Backward Pass on Leaf Tapes #
Lowering an empty graph produces a tape that contains only leaf nodes. This file shows that the
runtime dense reverse loop is the identity on such a tape: every leaf's backward returns no
contributions, so each step performs its bookkeeping checks and returns the gradient array
unchanged. This is the nil case shared by the Graph and GraphData backward-link theorems.
theorem
Proofs.Autograd.Algebra.Graph.getNode?_addLeaves_empty
{α : Type}
[TorchLean.Storage α]
{Γ : List Spec.Shape}
(x : TorchLean.TensorPack α Γ)
{n : ℕ}
(hn : n < Γ.length)
:
The node stored at index n of a leaf-only tape is the leaf of the n-th input tensor.
theorem
Proofs.Autograd.Algebra.Graph.backwardDenseFromStep_addLeaves_empty
{α : Type}
[TorchLean.Storage α]
{Γ : List Spec.Shape}
[Add α]
(x seed : TorchLean.TensorPack α Γ)
{n : ℕ}
(hn : n < Γ.length)
:
One runtime backward step at a leaf leaves the dense gradient array unchanged.
theorem
Proofs.Autograd.Algebra.Graph.backwardDenseFromLoop_addLeaves_empty
{α : Type}
[TorchLean.Storage α]
{Γ : List Spec.Shape}
[Add α]
(x seed : TorchLean.TensorPack α Γ)
(n : ℕ)
:
n ≤ Γ.length →
(addLeaves Runtime.Autograd.Tape.empty x).backwardDenseFromLoop n seed.toShapeErasedArray = Except.ok seed.toShapeErasedArray
The runtime backward loop over a leaf-only tape is the identity on the gradient array.
theorem
Proofs.Autograd.Algebra.Graph.backwardDenseFrom_addLeaves_empty
{α : Type}
[TorchLean.Storage α]
{Γ : List Spec.Shape}
[Add α]
(x seed : TorchLean.TensorPack α Γ)
:
The dense backward pass over a leaf-only tape returns its seed unchanged.