Nested forward-mode inputs

Each layer of Dual.Nested α n carries one independent differentiation direction. The last direction is outermost: for two directions the input is ⟨⟨x, v⟩, ⟨w, 0⟩⟩. The first listed direction is therefore innermost. Keeping this order matters for backends whose arithmetic is not associative.

Seeding and extraction work for every runtime scalar context. Their exact-real derivative interpretation is proved separately in NN.Proofs.Autograd.Dual.

def Runtime.Autograd.Model.Dual.Nested (α : Type) : ℕ → Type

The runtime dual carrier nested once for each differentiation direction.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instStorageNested {α : Type} [TorchLean.Storage α] (n : ℕ) : TorchLean.Storage (Nested α n)

Preserve the base backend's storage at order zero; dual layers use array storage.

@[instance_reducible]

instance Runtime.Autograd.Model.Dual.instContextNested {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) : Context (Nested α n)

Reuse the scalar backend's arithmetic at every level of nesting.

def Runtime.Autograd.Model.Dual.Nested.ofPrimal {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) : α → Nested α n

Embed a constant in all primal slots and set its derivative coefficients to zero.

@[simp]

theorem Runtime.Autograd.Model.Dual.Nested.ofPrimal_zero {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) : ofPrimal n 0 = 0

Zero gradient buffers have the same representation at every nesting depth.

def Runtime.Autograd.Model.Dual.Nested.seed {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} : (Fin n → α) → α → Nested α n

Seed constant directions; the last direction occupies the outermost dual layer.

def Runtime.Autograd.Model.Dual.Nested.tangent {α : Type} {n : ℕ} : Nested α n → α

Extract the coefficient containing every differentiation direction exactly once.

@[simp]

theorem Runtime.Autograd.Model.Dual.Nested.seed_zero {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) (x : α) : seed (fun (x : Fin n) => 0) x = ofPrimal n x

Zero directions give the same coefficients as a constant embedding.

def Runtime.Autograd.Model.Dual.Nested.seedTensor {α : Type} [TorchLean.Storage α] [Context α] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → TorchLean.Tensor α shape) (input : TorchLean.Tensor α shape) : TorchLean.Tensor (Nested α n) shape

Seed a direction tuple of arbitrary tensor shape, coordinate by coordinate.

def Runtime.Autograd.Model.Dual.Nested.tangentTensor {α : Type} [TorchLean.Storage α] {shape : Spec.Shape} {n : ℕ} (output : TorchLean.Tensor (Nested α n) shape) : TorchLean.Tensor α shape

Extract the mixed derivative coefficient at every output coordinate.

@[simp]

theorem Runtime.Autograd.Model.Dual.Nested.seedTensor_apply {α : Type} [TorchLean.Storage α] [Context α] {shape : Spec.Shape} {n : ℕ} (directions : Fin n → TorchLean.Tensor α shape) (input : TorchLean.Tensor α shape) (i : shape.Coord) : TorchLean.Tensor.Internal.Rep.get (seedTensor directions input) i = seed (fun (k : Fin n) => TorchLean.Tensor.Internal.Rep.get (directions k) i) (TorchLean.Tensor.Internal.Rep.get input i)

Seeding preserves the supplied value and directions at every tensor coordinate.

@[simp]

theorem Runtime.Autograd.Model.Dual.Nested.seedTensor_zero {α : Type} [TorchLean.Storage α] [Context α] {shape : Spec.Shape} (n : ℕ) (x : TorchLean.Tensor α shape) : seedTensor (fun (x : Fin n) => TorchLean.Tensor.zeros shape) x = TorchLean.Tensor.map (ofPrimal n) x

A tensor with zero directions is held constant at every nesting depth.

@[simp]

theorem Runtime.Autograd.Model.Dual.Nested.tangentTensor_apply {α : Type} [TorchLean.Storage α] {shape : Spec.Shape} {n : ℕ} (output : TorchLean.Tensor (Nested α n) shape) (i : shape.Coord) : TorchLean.Tensor.Internal.Rep.get (tangentTensor output) i = (TorchLean.Tensor.Internal.Rep.get output i).tangent

Tensor extraction reads exactly the scalar coefficient at each coordinate.

theorem Runtime.Autograd.Model.Dual.Nested.seedTensor_succ {α : Type} [TorchLean.Storage α] [Context α] {shape : Spec.Shape} {n : ℕ} (directions : Fin (n + 1) → TorchLean.Tensor α shape) (input : TorchLean.Tensor α shape) : seedTensor directions input = DualTensor.withTangents (seedTensor (Fin.init directions) input) (TorchLean.Tensor.map (ofPrimal n) (directions (Fin.last n)))

Adding a direction uses the existing one-step tensor seeding operation.