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) (postprocess : TorchLean.Tensor Float s → TorchLean.Tensor Float s := fun (reconstruction : TorchLean.Tensor Float s) => reconstruction.clamp (-1) 1) (denominatorFloor : Float := 1e-12) : TorchLean.diffusion.ddimPrev previousAlpha alpha sample epsilon postprocess denominatorFloor = stepFromEps denominatorFloor previousAlpha alpha sample epsilon postprocess

The public reverse update is the image DDIM formula for every denominator floor and shape-preserving reconstruction postprocessor.

The equality preserves postprocessing before remixing and reuse of the supplied epsilon. It applies to the actual Float expression, including non-finite values and the original multiplication and addition order. The defaults retain clipping and the floor 1e-12.

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.sample_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.sample batchShape spatial schedule clean step 0 epsilon).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.