Tape invariants of lowered graphs

Lowering a graph marks every runtime node as a gradient accumulation slot and only emits backward contributions to earlier node ids (BackwardPidsLt). The dense reverse sweep proofs in BackwardGraph consume both invariants.

theorem Proofs.Autograd.Algebra.Graph.all_requiresGrad_addLeaves {α : Type} [TorchLean.Storage α] (t : Runtime.Autograd.Tape (Spec.SomeTensor α)) (ht : (t.nodes.all fun (n : Runtime.Autograd.Node (Spec.SomeTensor α)) => n.requiresGrad) = true) {Γ : List Spec.Shape} (xs : TorchLean.TensorPack α Γ) : ((addLeaves t xs).nodes.all fun (n : Runtime.Autograd.Node (Spec.SomeTensor α)) => n.requiresGrad) = true

addLeaves keeps every tape node eligible for gradient accumulation.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape_all_requires_grad_true {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : ((lowerGraphDataToTape g x d).1.nodes.all fun (n : Runtime.Autograd.Node (Spec.SomeTensor α)) => n.requiresGrad) = true

All nodes produced by lowerGraphDataToTape have requiresGrad = true.

This is a simplifying invariant: the lowered tape is meant for correctness proofs, so we mark every node as eligible for gradient accumulation (including leaves for inputs).

theorem Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape_requires_grad_true {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d : Δ) : have t := (lowerGraphDataToTape g x d).1; ∀ (i : ℕ) (hi : i < t.nodes.size), t.nodes[i].requiresGrad = true

Pointwise form of lowerGraphDataToTape_all_requires_grad_true, convenient for array indexing: every node of the lowered tape has requiresGrad = true.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape_backward_pids_lt_id {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d0 : Δ) : BackwardPidsLt (lowerGraphDataToTape g x d0).1

Backward closure safety for lowerGraphDataToTape: parent ids produced by any node are strictly smaller than the node id.

This is the “edges point backwards” invariant required by the runtime reverse loop: when processing node id, every contribution targets an earlier node (pid < id), so accumulation is well-founded.