VP diffusion schedules (spec layer)

This file defines a discrete-time variance-preserving (VP) schedule for diffusion models.

We follow the common DDPM-style discrete schedule:

• choose $T$ steps and a sequence $\beta_0,\ldots,\beta_{T-1}$ with $0\le\beta_t<1$,
• define $\alpha_t:=1-\beta_t$,
• define the cumulative product $\bar\alpha_0:=1$ and $\bar\alpha_{t+1}:=\bar\alpha_t\alpha_t$.

Then the forward noising kernel is (informally):

$$ x_t=\sqrt{\bar\alpha_t}\,x_0+\sqrt{1-\bar\alpha_t}\,\varepsilon, \qquad \varepsilon\sim\mathcal{N}(0,I). $$

We keep the schedule scalar-polymorphic (Context α) so the same definitions can be reused under:

• Float (fast runtime execution),
• IEEE32Exec / NeuralFloat (proof-relevant floating-point models),
• interval-like scalars (verification), and
• ℝ (mathematical proofs).

References (informal pointers):

• Ho, Jain, Abbeel (2020), "Denoising Diffusion Probabilistic Models" (DDPM).

structure Generative.Diffusion.VPSchedule (α : Type) (T : ℕ) [Context α] : Type

Discrete VP schedule with T diffusion steps.

• betas : Spec.Vec T α

  Per-step variances $\beta_t$ for $t=0,\ldots,T-1$.

def Generative.Diffusion.VPSchedule.beta {α : Type} [Context α] {T : ℕ} (sched : VPSchedule α T) (t : Fin T) : α

Fetch $\beta_t$ as a scalar.

def Generative.Diffusion.VPSchedule.alpha {α : Type} [Context α] {T : ℕ} (sched : VPSchedule α T) (t : Fin T) : α

$\alpha_t:=1-\beta_t$.

def Generative.Diffusion.VPSchedule.alphaBar {α : Type} [Context α] {T : ℕ} (sched : VPSchedule α T) (t : Fin (T + 1)) : α

Compute $\bar\alpha_t$ for t : Fin (T+1) with the convention:

• $\bar\alpha_0=1$,
• $\bar\alpha_{t+1}=\bar\alpha_t\alpha_t$.

Implementation note: define an auxiliary recursion on Nat, then package it as a Fin function.

def Generative.Diffusion.VPSchedule.alphaBar.go {α : Type} [Context α] {T : ℕ} (sched : VPSchedule α T) (k : ℕ) : k < T + 1 → α

def Generative.Diffusion.VPSchedule.alphaBarVec {α : Type} [Context α] {T : ℕ} (sched : VPSchedule α T) : Spec.Vec (T + 1) α

Vector form of alphaBar (length $T+1$).

def Generative.Diffusion.VPSchedule.timeOfIndex {α : Type} [Context α] {T : ℕ} (t : Fin (T + 1)) : α

Convert a discrete time index t : Fin (T+1) into a scalar time $t/T\in[0,1]$ (when $T>0$).

If $T=0$, we define the time as $0$ (the only index is $t=0$).

Simple constructors

These are convenience constructors for examples and examples. We intentionally keep them small and deterministic; large-scale training pipelines usually want explicit control over schedules.

def Generative.Diffusion.VPSchedule.linearBetas {α : Type} [Context α] (T : ℕ) (β_start β_end : α) : Spec.Vec T α

Linear $\beta$ schedule over $T$ steps: $\beta_t$ interpolates from $\beta_{\mathrm{start}}$ to $\beta_{\mathrm{end}}$.

Note: this is a small spec helper. Popular schedules in the diffusion literature often use variants such as cosine schedules or continuous VP schedules; add those as separate named specs when a model or theorem needs them.

def Generative.Diffusion.VPSchedule.linear {α : Type} [Context α] (T : ℕ) (β_start β_end : α) : VPSchedule α T

Build a schedule from a linear beta ramp.