Reverse DDIM sampler (spec layer)

DDIM (Denoising Diffusion Implicit Models) can be viewed as a deterministic sampler that reuses the same denoiser ε_θ(x,t) but removes per-step noise.

This file provides the η = 0 variant (fully deterministic), which is often used as a simple "flow-like" sampler derived from the same diffusion model.

Reference (informal pointer):

• Song, Meng, Ermon (2021), "Denoising Diffusion Implicit Models" (DDIM).

def Generative.Diffusion.ddimStep {α : Type} [Context α] {T : ℕ} {s : Spec.Shape} (sched : VPSchedule α T) (model : EpsModel α s) (k : Fin T) (x_t : Spec.Tensor α s) : Spec.Tensor α s

One deterministic DDIM step x_t -> x_{t-1} (η = 0).

We reuse the same x0Pred reconstruction as DDPM and then recompose x_{t-1} using the forward-process coefficients at time t-1:

x_{t-1} = sqrt(ᾱ_{t-1}) * x0_pred + sqrt(1-ᾱ_{t-1}) * ε̂.

def Generative.Diffusion.ddimSample {α : Type} [Context α] {T : ℕ} {s : Spec.Shape} (sched : VPSchedule α T) (model : EpsModel α s) (x_T : Spec.Tensor α s) : Spec.Tensor α s

Run the full deterministic DDIM sampler for T steps (η = 0).

noncomputable def Generative.Diffusion.ddimStepSystem {T : ℕ} {s : Spec.Shape} (sched : VPSchedule Spec.SpecScalar T) (model : EpsModel Spec.SpecScalar s) (k : Fin T) : NN.Spec.Dynamics.DynamicalSystem s

Real-valued DDIM transition as a DynamicalSystem.

DynamicalSystem is fixed to SpecScalar = ℝ, so this adapter gives DDIM samplers the same trajectory/fixed-point API used by SSMs and other discrete systems.

@[simp]

theorem Generative.Diffusion.ddimStepSystem_step {T : ℕ} {s : Spec.Shape} (sched : VPSchedule Spec.SpecScalar T) (model : EpsModel Spec.SpecScalar s) (k : Fin T) (x : Spec.SpecTensor s) : (ddimStepSystem sched model k).step x = ddimStep sched model k x