Gradient references carry the version of their last materialization. A uniform contribution updates one shared history; selected parent gradients replay their pending updates before receiving the node's complete local contribution. All scalar additions retain their dense evaluation order.

def Proofs.Autograd.Algebra.Deferred.addUniform {α : Type} [TorchLean.Storage α] [Add α] {shape : Spec.Shape} (uniform : α) (value : TorchLean.Tensor α shape) : TorchLean.Tensor α shape

Add a uniform tensor on the right, exactly as in dense context accumulation.

def Proofs.Autograd.Algebra.Deferred.materializePack {α : Type} [TorchLean.Storage α] [Add α] [DecidableEq α] (history : History α) (clock : ℕ) (epochs : Array ℕ) {shapes : List Spec.Shape} : TorchLean.TensorPack α shapes → ℕ → TorchLean.TensorPack α shapes

Materialize a typed boundary in one traversal, with constant-time version lookup.

theorem Proofs.Autograd.Algebra.Deferred.getIdx_materializePack {α : Type} [TorchLean.Storage α] [Add α] [DecidableEq α] (history : History α) (clock : ℕ) (epochs : Array ℕ) {shapes : List Spec.Shape} (xs : TorchLean.TensorPack α shapes) (offset : ℕ) {shape : Spec.Shape} (idx : Idx shapes shape) : getIdx (materializePack history clock epochs xs offset) idx = applyRecentStable addUniform history (clock - epochs[offset + ↑idx.i]?.getD 0) (getIdx xs idx)

theorem Proofs.Autograd.Algebra.Deferred.materializePack_snoc {α : Type} [TorchLean.Storage α] [Add α] [DecidableEq α] (history : History α) (clock : ℕ) (epochs : Array ℕ) {shapes : List Spec.Shape} (xs : TorchLean.TensorPack α shapes) (offset : ℕ) {shape : Spec.Shape} (value : TorchLean.Tensor α shape) : materializePack history clock epochs (xs.snoc value) offset = (materializePack history clock epochs xs offset).snoc (applyRecentStable addUniform history (clock - epochs[offset + shapes.length]?.getD 0) value)

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

Array gradients and a shared chronological history of deferred uniform additions.

• stored : TensorContext α shapes

  Most recently materialized tensor at each active position.

• epochs : Array ℕ

  History version already applied to each tensor. Finalized suffix entries may remain here.

• clock : ℕ

  Number of uniform additions issued so far.

• history : Deferred.History α

  Consecutive identical contributions share one run.

• covered : self.stored.values.size ≤ self.epochs.size

  Every active tensor has a version slot.

• bounded (i : ℕ) (bound : i < self.epochs.size) : self.epochs[i] ≤ self.clock

  No tensor version refers to an update that has not happened.

def Proofs.Autograd.Algebra.GradientContext.ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (seed : TorchLean.TensorPack α shapes) : GradientContext α shapes

Start with a materialized seed and no deferred additions.

def Proofs.Autograd.Algebra.GradientContext.lookup {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) : TensorLookup α shapes

Read one gradient, replaying precisely the updates since its saved version.

def Proofs.Autograd.Algebra.GradientContext.toPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) : TorchLean.TensorPack α shapes

Materialize only when crossing back into the public typed pack interface.

@[simp]

theorem Proofs.Autograd.Algebra.GradientContext.lookup_toPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) : TensorLookup.ofPack ctx.toPack = ctx.lookup

@[simp]

theorem Proofs.Autograd.Algebra.GradientContext.lookup_ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (seed : TorchLean.TensorPack α shapes) : (ofPack seed).lookup = TensorLookup.ofPack seed

@[simp]

theorem Proofs.Autograd.Algebra.GradientContext.toPack_ofPack {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (seed : TorchLean.TensorPack α shapes) : (ofPack seed).toPack = seed

def Proofs.Autograd.Algebra.GradientContext.addUniform {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [DecidableEq α] (ctx : GradientContext α shapes) (uniform : α) : GradientContext α shapes

Defer one uniform contribution to the active prefix.

theorem Proofs.Autograd.Algebra.GradientContext.lookup_addUniform {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) (uniform : α) {shape : Spec.Shape} (idx : Idx shapes shape) : (ctx.addUniform uniform).lookup.read idx = Deferred.addUniform uniform (ctx.lookup.read idx)

def Proofs.Autograd.Algebra.GradientContext.set {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : GradientContext α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) (value : TorchLean.Tensor α shape) : GradientContext α shapes

Save an already materialized gradient and its current history version.

@[simp]

theorem Proofs.Autograd.Algebra.GradientContext.lookup_set {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) {shape : Spec.Shape} (idx : Idx shapes shape) (value : TorchLean.Tensor α shape) : (ctx.set idx value).lookup = ctx.lookup.set idx value

@[reducible, inline]

abbrev Proofs.Autograd.Algebra.GradientContext.Update (α : Type) [TorchLean.Storage α] (shapes : List Spec.Shape) : Type

A materialized update contains no reference to the full previous gradient context.

def Proofs.Autograd.Algebra.GradientContext.snapshot {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (indices : List (SomeIdx shapes)) (source : TensorLookup α shapes) : List (Update α shapes)

Compute every exceptional result before modifying the gradient array.

def Proofs.Autograd.Algebra.GradientContext.setMany {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} (ctx : GradientContext α shapes) : List (Update α shapes) → GradientContext α shapes

Install materialized exceptions in their existing order. Duplicate writes are identical.

theorem Proofs.Autograd.Algebra.GradientContext.lookup_setMany_snapshot {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) (indices : List (SomeIdx shapes)) (source : TensorLookup α shapes) {shape : Spec.Shape} (other : Idx shapes shape) : (ctx.setMany (snapshot indices source)).lookup.read other = if ↑other.i ∈ List.map (fun (entry : SomeIdx shapes) => ↑entry.snd.i) indices then source.read other else ctx.lookup.read other

def Proofs.Autograd.Algebra.GradientContext.addContributions {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) (contribution : Contributions α shapes) : GradientContext α shapes

Accumulate a node's complete local contribution, preserving each dense addition.

theorem Proofs.Autograd.Algebra.GradientContext.lookup_addContributions {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) (contribution : Contributions α shapes) : (ctx.addContributions contribution).lookup = ctx.lookup.add contribution.lookup

theorem Proofs.Autograd.Algebra.GradientContext.toPack_addContributions {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) (contribution : Contributions α shapes) : (ctx.addContributions contribution).toPack = ctx.toPack.add (contribution.dense ())

Compact accumulation equals full pack addition without an additive-identity assumption.

def Proofs.Autograd.Algebra.GradientContext.addDense {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) (contribution : TorchLean.TensorPack α shapes) : GradientContext α shapes

Custom dense VJPs remain supported through an exact materializing adapter.

@[simp]

theorem Proofs.Autograd.Algebra.GradientContext.toPack_addDense {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] (ctx : GradientContext α shapes) (contribution : TorchLean.TensorPack α shapes) : (ctx.addDense contribution).toPack = ctx.toPack.add contribution

def Proofs.Autograd.Algebra.GradientContext.cast {α : Type} [TorchLean.Storage α] {shapes other : List Spec.Shape} (same : shapes = other) (ctx : GradientContext α shapes) : GradientContext α other

Transport the typed active prefix without touching gradient storage.

@[simp]

theorem Proofs.Autograd.Algebra.GradientContext.toPack_cast {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] {other : List Spec.Shape} (same : shapes = other) (ctx : GradientContext α shapes) : (cast same ctx).toPack = TorchLean.TensorPack.cast same ctx.toPack

def Proofs.Autograd.Algebra.GradientContext.pop {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] {shape : Spec.Shape} (ctx : GradientContext α (shapes ++ [shape])) : GradientContext α shapes × TorchLean.Tensor α shape

Finalize one output gradient and remove its slot from the active prefix.

theorem Proofs.Autograd.Algebra.GradientContext.toPack_pop {α : Type} [TorchLean.Storage α] {shapes : List Spec.Shape} [Add α] [DecidableEq α] {shape : Spec.Shape} (ctx : GradientContext α (shapes ++ [shape])) : (ctx.pop.1.toPack, ctx.pop.2) = ctx.toPack.unsnoc

Removing a deferred gradient context agrees with removing the fully materialized pack.