Fused lowering for repeat

A checked repeat is executed by one row-major output fill. For each output flat index, the checked axis projection computes the corresponding input coordinate after forgetting every introduced axis. The kernel then reads that entry directly from the input tensor's native array.

This implementation allocates no singleton reshape, broadcast tensor, or permutation tensor. Its correctness theorem compares the flat-index kernel with the independent coordinate denotation for every scalar type, rank, and checked repeat pattern.

def TorchLean.Tensor.Internal.Lowering.repeatTensor {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.repeat) (inputTensor : checked.InputTensor α) : checked.OutputTensor α

Repeat a tensor by filling one native output buffer from the certified output-to-input coordinate map.

theorem TorchLean.Tensor.Internal.Lowering.repeatTensor_correct {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.repeat) (inputTensor : checked.InputTensor α) : repeatTensor checked hKind inputTensor = Semantics.denoteRepeat checked hKind inputTensor

The fused row-major repeat kernel equals the independent coordinate denotation.