First-Order Optimizer Relations

Relations between distinct first-order optimizer updates.

This is the tensor-facing layer: the statements are phrased over Spec.Tensor and the executable operator dictionary Spec.Context. When we want ordinary algebraic simplification, such as proving that a zero weight-decay AdamW update is the same parameter update as Adam, we specialize to ℝ, where mathlib provides the ring laws.

Context α gives us executable operators, but not algebraic laws like x * 0 = 0.

Optimizer-relationship theorems (AdamW → Adam, L2 vs weight decay, etc.) therefore live most naturally over proof backends like ℝ where the laws are available from Mathlib.

theorem Optim.AdamW.update_weight_decay_zero_params_eq_adam_real {s : Spec.Shape} (state : State ℝ s) (params grads : Spec.Tensor ℝ s) (hwd : state.weight_decay = 0) : (update state params grads).2 = (Adam.update { lr := state.lr, beta1 := state.beta1, beta2 := state.beta2, epsilon := state.epsilon, m := state.m, v := state.v, t := state.t } params grads).2

AdamW reduces to Adam when weight_decay = 0 (parameter-update equality), over ℝ.