Image diffusion API contracts

These equalities connect the public image helpers to their scalar-polymorphic specifications. The Float tensor operations use specialized kernels, so their coordinate laws supply the connection to the spec's pointwise operations. No real-field identities or tolerances are used.

The reverse update agrees with ImageDDIM.stepFromEps. Agreement with the separate ddimStep formula would require changing clipping, denominator, and time conventions, so it is not the contract stated here.

theorem Generative.Diffusion.ImageDDIM.float_add_eq_addSpec {s : Spec.Shape} (left right : TorchLean.Tensor Float s) : left.add right = left.addSpec right

Public Float addition and the spec addition have the same coordinate values.

theorem Generative.Diffusion.ImageDDIM.float_sub_eq_subSpec {s : Spec.Shape} (left right : TorchLean.Tensor Float s) : left.sub right = left.subSpec right

Public Float subtraction and the spec subtraction have the same coordinate values.

theorem Generative.Diffusion.ImageDDIM.ddimPrev_eq_stepFromEps {s : Spec.Shape} (previousAlpha alpha : Float) (sample epsilon : TorchLean.Tensor Float s) : TorchLean.diffusion.ddimPrev previousAlpha alpha sample epsilon = stepFromEps 1e-12 previousAlpha alpha sample epsilon

The public reverse update is the image DDIM formula with denominator floor 1e-12.

The equality preserves clipping before remixing and reuse of the supplied epsilon. It applies to the actual Float expression, with its original multiplication and addition order.

theorem Generative.Diffusion.ImageDDIM.schedule_alphaBar_eq {T : ℕ} (schedule : TorchLean.diffusion.Schedule T) (step : ℕ) : schedule.alphaBar step = alphaBar schedule.alphaBars (schedule.index step).succ

Cycling a public training step selects noisy state index + 1 in the spec view.

theorem Generative.Diffusion.ImageDDIM.schedule_normalizedTime_eq {T : ℕ} (schedule : TorchLean.diffusion.Schedule T) (step : ℕ) : schedule.normalizedTime step = timeOfIndex (schedule.index step)

The image time embedding agrees with the public schedule, including its single-state case.

theorem Generative.Diffusion.ImageDDIM.noisedSampleFromNoise_input_eq_qSample {T : ℕ} (batchShape : Spec.Shape) {d c : ℕ} (spatial : TorchLean.Tensor ℕ [d]) (schedule : TorchLean.diffusion.Schedule T) (specSchedule : VPSchedule Float T) (hCoefficients : ∀ (index : Fin T), schedule.alphaBars[index] = specSchedule.alphaBar index.succ) (clean epsilon : TorchLean.Tensor Float (TorchLean.diffusion.sampleShape batchShape c spatial)) (step : ℕ) : (TorchLean.diffusion.noisedSampleFromNoise batchShape spatial schedule clean epsilon step).input = TorchLean.diffusion.appendTimeChannel batchShape spatial (qSample specSchedule clean (schedule.index step).succ epsilon) (timeOfIndex (schedule.index step))

Matching cumulative coefficients gives the same forward-corrupted sample and image time channel.

The hypothesis compares the actual stored coefficients with the chosen VP schedule. It does not identify the two linear constructors: their one-step endpoint conventions differ.