Diffusion core (spec layer)

This module defines the common vocabulary used by TorchLean's diffusion / flow specs:

• EpsModel: an $\varepsilon_\theta(x,t)$ denoiser interface (noise prediction), and
• a couple of total scalar helpers (sqrtNonneg, safeDiv) that keep specs robust across scalar backends.

Design notes:

• EpsModel is deliberately backbone-independent: it is a pure function of the current state x and a scalar time parameter t (typically normalized into [0,1]).
• Schedules and samplers remain separate modules so we can reuse the same denoiser with:
  • discrete DDPM / DDIM-style samplers, and
  • continuous-time probability-flow ODE samplers.

References (informal pointers):

• Ho, Jain, Abbeel (2020), "Denoising Diffusion Probabilistic Models" (DDPM).
• Song et al. (2021), "Score-Based Generative Modeling through Stochastic Differential Equations" (continuous-time VP SDE and probability-flow ODE).

def Generative.Diffusion.sqrtNonneg {α : Type} [Context α] (x : α) : α

A safe square root used by diffusion schedules and samplers: $\sqrt{\max(x,0)}$.

Why this helper exists:

• Some backends (intervals, IEEE models, etc.) prefer total semantics.
• In diffusion schedules, the quantities under a square root are mathematically nonnegative (e.g. $\bar\alpha(t)$ and $1-\bar\alpha(t)$), but numeric backends can still produce small negative values.

def Generative.Diffusion.safeDiv {α : Type} [Context α] (x y : α) : α

Safe scalar division with epsilon protection: $x/(y+\varepsilon)$.

This is primarily used to avoid $1/0$ in edge cases like $t=0$ or degenerate schedules.

structure Generative.Diffusion.EpsModel (α : Type) (s : Spec.Shape) [Context α] : Type

Noise-prediction model interface: $\varepsilon_\theta(x,t)$.

The intended interpretation is "predict the noise used to construct the noisy sample x at time t".

Notes:

• t is a scalar, not a discrete index. Discrete samplers can provide t := (k/T) or any other conventional embedding; continuous samplers can pass true continuous time.
• This interface does not bake in class-conditioning or text-conditioning; those can be handled by closing over extra context in the eps function, or by defining a richer model record in user code.

• eps : Spec.Tensor α s → α → Spec.Tensor α s

  Predict $\varepsilon$ from a noisy sample $x$ at scalar time $t$.