Forward noising process (spec layer)

This module defines the standard VP/DDPM forward noising transformation:

$$ x_t=\sqrt{\bar\alpha_t}\,x_0+\sqrt{1-\bar\alpha_t}\,\varepsilon $$

where $\varepsilon$ is intended to be standard normal noise (in runtime usage), but at the spec level is treated as an explicit input tensor.

def Generative.Diffusion.qSample {α : Type} [Context α] {T : ℕ} {s : Spec.Shape} (sched : VPSchedule α T) (x0 : Spec.Tensor α s) (t : Fin (T + 1)) (eps : Spec.Tensor α s) : Spec.Tensor α s

Forward-process sampling $q(x_t\mid x_0)$ for a discrete VP schedule.

Inputs:

• x0: clean data sample,
• t: discrete time index in 0..T,
• eps: explicit noise tensor (intended as N(0,I)).

Output:

• the noisy sample $x_t$.

This function is pure and total; any probabilistic interpretation is handled in the MLTheory layer (mathlib) or at runtime by sampling eps.