Runtime link: lowerGraphToTape + Tape.backwardDenseFrom

lowerGraphToTape produces a runtime tape whose node ids correspond to positions in the proof context Γ ++ ss, and bakes the proved vjp into each node's runtime backward closure.

The theorem backwardDenseFrom_lowerGraphToTape_eq_backpropAllCtx states that executing the runtime reverse-mode loop on this lowered tape matches the proved backpropAllCtx.

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 α) => 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: every node index is requiresGrad = true.

This is often more convenient than the .all formulation when reasoning about array indexing.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphDataToTape_backward_pids_lt_id {α Δ : Type} [TorchLean.Storage α] {Γ ss : List Spec.Shape} (g : GraphData α Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d0 : Δ) (id : ℕ) (n : Runtime.Autograd.Node α) : (lowerGraphDataToTape g x d0).1.getNode? id = some n → ∀ (d : Spec.SomeTensor α) (contribs : Array (ℕ × Spec.SomeTensor α)), n.backward d = Except.ok contribs → ∀ {pid : ℕ} {pg : Spec.SomeTensor α}, (pid, pg) ∈ contribs → pid < id

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.

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

All nodes produced by lowerGraphToTape have requiresGrad = true.

This mirrors lowerGraphDataToTape_all_requires_grad_true for the Graph interface.

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

Pointwise form of lowerGraphToTape_all_requires_grad_true.

theorem Proofs.Autograd.Algebra.Graph.lowerGraphToTape_backward_pids_lt_id {α Δ : Type} [TorchLean.Storage α] [CommSemiring α] {Γ ss : List Spec.Shape} (g : Graph Δ Γ ss) (x : TorchLean.TensorPack α Γ) (d0 : Δ) (id : ℕ) (n : Runtime.Autograd.Node α) : (g.lowerGraphToTape x d0).1.getNode? id = some n → ∀ (d : Spec.SomeTensor α) (contribs : Array (ℕ × Spec.SomeTensor α)), n.backward d = Except.ok contribs → ∀ {pid : ℕ} {pg : Spec.SomeTensor α}, (pid, pg) ∈ contribs → pid < id

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

This mirrors lowerGraphDataToTape_backward_pids_lt_id for the Graph interface.