Deferred uniform updates retain the order of scalar operations. Repeated updates can stop at a checked fixed point; the proof uses decidable equality, with no additive identity assumption. Repetition counts are Nat.iterate (step^[count]), whose evaluation order is the chronological one.

def Proofs.Autograd.Algebra.Deferred.repeatStable {β : Type} [DecidableEq β] (step : β → β) : ℕ → β → β

Stop repeating an operation only after checking that its actual result is a fixed point.

theorem Proofs.Autograd.Algebra.Deferred.repeatStable_eq {β : Type} [DecidableEq β] (step : β → β) (count : ℕ) (value : β) : repeatStable step count value = step^[count] value

Fixed-point compression preserves every finite sequence of repeated operations.

@[reducible, inline]

abbrev Proofs.Autograd.Algebra.Deferred.History (α : Type) : Type

Consecutive occurrences of the same uniform contribution share one run.

def Proofs.Autograd.Algebra.Deferred.push {α : Type} [DecidableEq α] (history : History α) (value : α) : History α

Append one update to a history stored with its newest run first.

def Proofs.Autograd.Algebra.Deferred.applyRecent {α β : Type} (step : α → β → β) : History α → ℕ → β → β

Apply the most recent count updates, in their original chronological order.

@[simp]

theorem Proofs.Autograd.Algebra.Deferred.applyRecent_zero {α β : Type} (step : α → β → β) (history : History α) (value : β) : applyRecent step history 0 value = value

theorem Proofs.Autograd.Algebra.Deferred.applyRecent_push {α β : Type} [DecidableEq α] (step : α → β → β) (history : History α) (uniform : α) (count : ℕ) (value : β) : applyRecent step (push history uniform) (count + 1) value = step uniform (applyRecent step history count value)

Extending the history performs exactly one more update, after all previous updates.

def Proofs.Autograd.Algebra.Deferred.applyRecentStable {α β : Type} [DecidableEq β] (step : α → β → β) : History α → ℕ → β → β

Execute a deferred history with checked fixed-point compression in each run.

theorem Proofs.Autograd.Algebra.Deferred.applyRecentStable_eq {α β : Type} [DecidableEq β] (step : α → β → β) (history : History α) (count : ℕ) (value : β) : applyRecentStable step history count value = applyRecent step history count value

Compressed history execution preserves the complete uncompressed update sequence.