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 of β₀, …, β_{T-1} with 0 ≤ β_t < 1,
• define α_t := 1 - β_t,
• define the cumulative product ᾱ_0 := 1 and ᾱ_{t+1} := ᾱ_t * α_t.

Then the forward noising kernel is (informally):

x_t = sqrt(ᾱ_t) x_0 + sqrt(1-ᾱ_t) ε where ε ~ 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 β_t for t = 0..T-1.

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

Fetch β_t as a scalar.

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

α_t := 1 - β_t.

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

Compute ᾱ_t for t : Fin (T+1) with the convention:

• ᾱ_0 = 1,
• ᾱ_{t+1} = ᾱ_t * α_t.

Implementation note: we define an auxiliary recursion on Nat and then package it as a Fin function; this keeps the definition total and easy to evaluate.

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 ∈ [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 demos. 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 β schedule over T steps: β_t interpolates from β_start to β_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.