A VJP can describe a uniform contribution with finitely many exceptions. Its dense program remains available as a compatibility adapter. The certificate preserves the scalar program at every entry; in particular, adding two contributions does not discard zeros or combine repeated parents early.

@[reducible, inline]

abbrev Proofs.Autograd.Algebra.SomeIdx (shapes : List Spec.Shape) : Type

A typed position whose shape is available without traversing the context's shape list.

def Proofs.Autograd.Algebra.TensorLookup.fill {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (value : α) : TensorLookup α shapes

A reader whose tensors all contain the same scalar.

def Proofs.Autograd.Algebra.TensorLookup.add {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] (left right : TensorLookup α shapes) : TensorLookup α shapes

Pointwise addition retains left-to-right scalar argument order.

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.ofPack_fill {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (value : α) : ofPack (TorchLean.TensorPack.fill value) = fill value

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.ofPack_zero {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Zero α] : ofPack TorchLean.TensorPack.zero = fill 0

@[simp]

theorem Proofs.Autograd.Algebra.TensorLookup.ofPack_add {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] (left right : TorchLean.TensorPack α shapes) : ofPack (left.add right) = (ofPack left).add (ofPack right)

structure Proofs.Autograd.Algebra.Contributions (α : Type) [TorchLean.Storage α] (shapes : List Spec.Shape) : Type

A dense VJP program with a certified compact description of its entries.

• dense : Unit → TorchLean.TensorPack α shapes

  The original dense program, evaluated only by the compatibility adapter.

• lookup : TensorLookup α shapes

  Constant-time lookup for the small expression formed by one node's VJP.

• uniform : α

  Scalar present in tensors at positions outside support.

• support : List (SomeIdx shapes)

  Positions where the contribution can differ from the uniform tensor.

• correct : TensorLookup.ofPack (self.dense ()) = self.lookup

  The compact reader computes exactly the dense VJP.

• outside {shape : Spec.Shape} (idx : Idx shapes shape) : (∀ entry ∈ self.support, ↑entry.snd.i ≠ ↑idx.i) → self.lookup.read idx = TorchLean.Tensor.full shape self.uniform

  Every omitted position really is uniform, without assuming any law about zero.

def Proofs.Autograd.Algebra.Contributions.zero {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Zero α] : Contributions α shapes

The original all-zero pack, with its explicit uniform contribution retained.

def Proofs.Autograd.Algebra.Contributions.add {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] (left right : Contributions α shapes) : Contributions α shapes

Add two VJP descriptions in the original order. Duplicate support entries intentionally remain: the reader evaluates the complete local sum before the global gradient receives one contribution.