Fused native lowering for reduction

A checked reduction allocates only its final output tensor. For each output coordinate, the executable kernel:

1. converts the retained output axes to elementary-axis coordinates;
2. enumerates assignments of only the axes removed by the reduction;
3. reconstructs the corresponding original input coordinate;
4. reads that scalar directly from the input tensor's native array.

There are no intermediate reshape, permutation, or reduction tensors. A generic reducer still receives a Multiset, because its type promises that the result is independent of coordinate enumeration order, but that multiset contains exactly one value per removed-axis assignment.

The correctness proof uses the abstract reduction-fiber equivalence only in the theorem layer. The executable definitions remain computable and operate directly on native Rep storage.

theorem TorchLean.Tensor.Internal.Lowering.Reduce.Impl.inputAxes_subset_output_append_reduced (checked : Check.CheckedTransform) ⦃axis : Check.AxisId⦄ : axis ∈ checked.value.normalized.inputAxes → axis ∈ checked.value.normalized.outputAxes ++ checked.reducedAxes

Every input axis is either retained or assigned by the reduction fiber.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reconstructedInputCoordinate (checked : Check.CheckedTransform) (outputCoordinate : Coord checked.value.output) (reducedCoordinate : AxisTuple checked.value.axisLength checked.reducedAxes) : Coord checked.value.normalized.input

Reconstruct one original input coordinate from its retained output axes and one assignment of all removed axes.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionInputFlatIndex (checked : Check.CheckedTransform) (outputCoordinate : Coord checked.value.output) (reducedFlatIndex : Fin checked.reductionShape.size) : Fin checked.value.normalized.input.size

Compute the row-major input index selected by one output coordinate and one flat reduced-axis coordinate.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionValuesFromFlat {α : Type u} (checked : Check.CheckedTransform) (read : Fin checked.value.normalized.input.size → α) (outputCoordinate : Coord checked.value.output) : Multiset α

Collect exactly the input values belonging to one output coordinate through a flat scalar reader.

The executable enumeration uses the row-major flat index of the removed-axis shape. This avoids constructing the generic Fintype instance for a dependent function tuple at every output coordinate.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionValues {α : Type u} [Storage α] (checked : Check.CheckedTransform) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : Multiset α

Collect one reduction fiber from an ordinary tensor's flat storage.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionFoldlFromFlat {α : Type u} {β : Type v} (step : β → α → β) (initial : β) (checked : Check.CheckedTransform) (read : Fin checked.value.normalized.input.size → α) (outputCoordinate : Coord checked.value.output) : β

Fold one reduction fiber without materializing its value multiset.

The traversal is the same row-major enumeration used by reductionValues. Only the accumulator and the current scalar remain live in the loop.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionFoldl {α : Type u} {β : Type v} [Storage α] (step : β → α → β) (initial : β) (checked : Check.CheckedTransform) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : β

Fold one reduction fiber by reading an ordinary tensor's flat storage.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionFoldlNonemptyFromFlat {α : Type u} (step : α → α → α) (checked : Check.CheckedTransform) (hPositive : 0 < checked.reductionFiberSize) (read : Fin checked.value.normalized.input.size → α) (outputCoordinate : Coord checked.value.output) : α

Fold a nonempty reduction fiber from its first row-major value.

Starting from an actual tensor entry avoids inventing sentinel values for operations such as minimum and maximum. The remaining entries are visited in the same order as reductionFoldl, so scalar operations with observable operand order, including IEEE min and max in the presence of NaNs, have a fully specified result.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionFoldlNonempty {α : Type u} [Storage α] (step : α → α → α) (checked : Check.CheckedTransform) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : α

Fold a nonempty reduction fiber by reading an ordinary tensor's flat storage.

def TorchLean.Tensor.Internal.Lowering.reduceTensor {α : Type u} {β : Type v} [Storage α] [Storage β] (aggregate : Multiset α → β) (checked : Check.CheckedTransform) (_hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) : checked.OutputTensor β

Execute a checked reduction with one final output allocation.

The aggregate receives one value for every assignment of the removed axes. Its result type may differ from the input scalar type, and its empty-multiset value determines empty-fiber behavior.

theorem TorchLean.Tensor.Internal.Lowering.reduceTensor_correct {α : Type u} {β : Type v} [Storage α] [Storage β] (aggregate : Multiset α → β) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) : reduceTensor aggregate checked hKind inputTensor = Semantics.denoteReduce aggregate checked hKind inputTensor

Fused native reduction equals the independent coordinate-fiber denotation for every multiset aggregate, checked reduction plan, and input tensor.

theorem TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionValues_card {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : (reductionValues checked inputTensor outputCoordinate).card = checked.reductionFiberSize

The fused reduction enumerates exactly the certified number of fiber values.

def TorchLean.Tensor.Internal.Lowering.reduceFoldTensor {α : Type u} {β : Type v} {γ : Type w} [Storage α] [Storage γ] (step : β → α → β) (initial : β) (finish : β → ℕ → γ) (checked : Check.CheckedTransform) (_hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) : checked.OutputTensor γ

Reduce every fiber through one accumulator loop and one scalar finalizer.

The finalizer also receives the certified fiber cardinality. This supports cardinality-dependent reductions such as the arithmetic mean without constructing a multiset merely to count its entries.

def TorchLean.Tensor.Internal.Lowering.reduceNonemptyFoldTensor {α : Type u} [Storage α] (step : α → α → α) (checked : Check.CheckedTransform) (_hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) : checked.OutputTensor α

Reduce every nonempty fiber from its first row-major value.

Unlike reduceNonemptyTensor, this executor does not materialize a multiset. It is intended for ordered binary operations whose result may depend on traversal order.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensor_ordered_correct {α : Type u} {β : Type v} {γ : Type w} [Storage α] [Storage γ] (step : β → α → β) (initial : β) (finish : β → ℕ → γ) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) : reduceFoldTensor step initial finish checked hKind inputTensor = Semantics.denoteOrderedReduce step initial finish checked hKind inputTensor

The direct accumulator executor implements the independent row-major ordered reduction denotation for every scalar operation.

In particular, this theorem requires no associativity or commutativity and is therefore suitable for IEEE floating-point arithmetic.

theorem TorchLean.Tensor.Internal.Lowering.reduceNonemptyFoldTensor_ordered_correct {α : Type u} [Storage α] (step : α → α → α) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) : reduceNonemptyFoldTensor step checked hKind hPositive inputTensor = Semantics.denoteOrderedReduceNonempty step checked hKind hPositive inputTensor

The direct first-value executor implements the independent ordered nonempty reduction denotation for every binary scalar operation.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensor_correct {α : Type u} {β : Type v} {γ : Type w} [Storage α] [Storage γ] (step : β → α → β) [RightCommutative step] (initial : β) (finish : β → ℕ → γ) (aggregate : Multiset α → γ) (hAggregate : ∀ (values : Multiset α), aggregate values = finish (Multiset.foldl step initial values) values.card) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) : reduceFoldTensor step initial finish checked hKind inputTensor = Semantics.denoteReduce aggregate checked hKind inputTensor

The direct accumulator executor implements any multiset aggregate that factors through an order-independent left fold and the multiset cardinality.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensor_nonempty_correct {α : Type u} {β : Type v} {γ : Type w} [Storage α] [Storage γ] (step : β → α → β) [RightCommutative step] (initial : β) (finish : β → ℕ → γ) (aggregate : (values : Multiset α) → values ≠ 0 → γ) (hAggregate : ∀ (values : Multiset α) (hValues : values ≠ 0), aggregate values hValues = finish (Multiset.foldl step initial values) values.card) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) : reduceFoldTensor step initial finish checked hKind inputTensor = Semantics.denoteReduceNonempty aggregate checked hKind hPositive inputTensor

The accumulator executor also implements nonempty aggregates that factor through an order-independent fold and the certified fiber cardinality.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensor_sum {α : Type u} [Storage α] [AddCommMonoid α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) : reduceFoldTensor (fun (x1 x2 : α) => x1 + x2) 0 (fun (total : α) (x : ℕ) => total) checked hKind inputTensor = Semantics.denoteReduce Multiset.sum checked hKind inputTensor

Additive reduction executes as one direct scalar fold per output entry.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensor_prod {α : Type u} [Storage α] [CommMonoid α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) : reduceFoldTensor (fun (x1 x2 : α) => x1 * x2) 1 (fun (total : α) (x : ℕ) => total) checked hKind inputTensor = Semantics.denoteReduce Multiset.prod checked hKind inputTensor

Multiplicative reduction executes as one direct scalar fold per output entry.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensor_any (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor Bool) : reduceFoldTensor or false (fun (total : Bool) (x : ℕ) => total) checked hKind inputTensor = Semantics.denoteReduce Reduction.any checked hKind inputTensor

Boolean disjunction reduction executes without constructing a multiset.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensor_all (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor Bool) : reduceFoldTensor and true (fun (total : Bool) (x : ℕ) => total) checked hKind inputTensor = Semantics.denoteReduce Reduction.all checked hKind inputTensor

Boolean conjunction reduction executes without constructing a multiset.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensor_mean {α : Type u} [Storage α] [DivisionRing α] [CharZero α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) : reduceFoldTensor (fun (x1 x2 : α) => x1 + x2) 0 (fun (total : α) (cardinality : ℕ) => total / ↑cardinality) checked hKind inputTensor = Semantics.denoteReduceNonempty Reduction.mean checked hKind hPositive inputTensor

Exact mean reduction accumulates the sum directly and divides once by the certified fiber cardinality.

def TorchLean.Tensor.Internal.Lowering.reduceNonemptyTensor {α : Type u} {β : Type v} [Storage α] [Storage β] (aggregate : (values : Multiset α) → values ≠ 0 → β) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) : checked.OutputTensor β

Execute a reduction whose aggregate is defined only for nonempty multisets, using the same single-allocation fused kernel.

theorem TorchLean.Tensor.Internal.Lowering.reduceNonemptyTensor_correct {α : Type u} {β : Type v} [Storage α] [Storage β] (aggregate : (values : Multiset α) → values ≠ 0 → β) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) : reduceNonemptyTensor aggregate checked hKind hPositive inputTensor = Semantics.denoteReduceNonempty aggregate checked hKind hPositive inputTensor

Fused nonempty reduction equals its independent coordinate-fiber denotation.