Forward noising process (spec layer)

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

x_t = sqrt(ᾱ_t) x_0 + sqrt(1-ᾱ_t) ε

where ε 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 | 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.