Scheduler Arithmetic

Learning-rate schedulers for TorchLean runtime training.

Schedulers are small deterministic state machines that answer:

• “what learning rate should we use at this step?”
• “how do we advance to the next step?”

TorchLean keeps schedulers explicit and pure so:

• runtime code can store scheduler state in a record (or serialize it),
• proofs and specs can refer to the exact schedule that was used.

Step counter convention:

• currentStep is 0-indexed. The first call to getLr uses currentStep = 0.
• step increments the counter by 1.

This module contains the shared scalar operations used by native and PyTorch-compatible schedules.

References (common schedules we implement):

• Cosine annealing / SGDR (Loshchilov–Hutter, 2017): https://arxiv.org/abs/1608.03983
• Cyclical learning rates (Smith, 2017): https://arxiv.org/abs/1506.01186
• 1cycle policy (Smith, 2018): https://arxiv.org/abs/1803.09820

PyTorch references:

• torch.optim.lr_scheduler overview: https://pytorch.org/docs/stable/optim.html#how-to-adjust-learning-rate

Shared utilities

def Optim.SchedulerUtils.clamp {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] (value lo hi : α) : α

Clamp value to the closed interval [lo, hi].

def Optim.SchedulerUtils.safeDiv {α : Type} [Context α] (num denom : α) : α

Safe division num/denom.

Returns 0 when denom == 0 so schedulers stay total even when misconfigured. This is used by the PyTorch-compatible schedulers, which mirror PyTorch's use of floating pct values but avoid exceptions in pure code.

def Optim.SchedulerUtils.ratioNat {α : Type} [Context α] (num denom : ℕ) : α

Safe ratio num/denom cast into the scalar type.

Returns 0 when denom = 0 so schedulers stay total even when misconfigured.

def Optim.SchedulerUtils.linearInterpolation {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] (startValue endValue factor : α) : α

Linear interpolation between startValue and endValue with factor ∈ [0,1].

def Optim.SchedulerUtils.linearInterpolationRaw {α : Type} [Context α] (startValue endValue factor : α) : α

Linear interpolation between startValue and endValue with no clamping.

This matches PyTorch's anneal helpers (OneCycleLR._annealing_linear), which permit factor outside [0,1] and therefore extrapolate.

def Optim.SchedulerUtils.cosineInterpolation {α : Type} [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] (startValue endValue factor : α) : α

Cosine interpolation between startValue and endValue with factor ∈ [0,1].

This is the usual smooth schedule: it starts and ends with zero slope.

def Optim.SchedulerUtils.cosineAnnealRaw {α : Type} [Context α] (startValue endValue factor : α) : α

Cosine anneal between startValue and endValue with no clamping.

This matches PyTorch's anneal helper (OneCycleLR._annealing_cos).