Flat input views for reduction

These kernels consume a certified flat scalar reader instead of requiring an already materialized input tensor. The ordinary reduction definitions and the fused transform-to-reduction path therefore share the same fiber enumeration, accumulator order, and correctness proofs.

def TorchLean.Tensor.Internal.Lowering.reduceTensorFromFlat {α : Type u} {β : Type v} [Storage α] [Storage β] (aggregate : Multiset α → β) (checked : Check.CheckedTransform) (_hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) (read : Fin checked.value.normalized.input.size → α) (_hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : checked.OutputTensor β

Apply a total multiset aggregate to every reduction fiber read through a flat input view.

def TorchLean.Tensor.Internal.Lowering.reduceFoldTensorFromFlat {α : 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 α) (read : Fin checked.value.normalized.input.size → α) (_hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : checked.OutputTensor γ

Fold every reduction fiber through one flat scalar reader and one final output allocation.

def TorchLean.Tensor.Internal.Lowering.reduceNonemptyFoldTensorFromFlat {α : Type u} [Storage α] (step : α → α → α) (checked : Check.CheckedTransform) (_hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) (read : Fin checked.value.normalized.input.size → α) (_hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : checked.OutputTensor α

Fold every nonempty reduction fiber from its first flat-view value.

theorem TorchLean.Tensor.Internal.Lowering.reduceTensorFromFlat_eq {α : Type u} {β : Type v} [Storage α] [Storage β] (aggregate : Multiset α → β) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) (read : Fin checked.value.normalized.input.size → α) (hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : reduceTensorFromFlat aggregate checked hKind inputTensor read hRead = reduceTensor aggregate checked hKind inputTensor

Pointwise-equal flat readers produce the same multiset reduction tensor.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensorFromFlat_eq {α : 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 α) (read : Fin checked.value.normalized.input.size → α) (hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : reduceFoldTensorFromFlat step initial finish checked hKind inputTensor read hRead = reduceFoldTensor step initial finish checked hKind inputTensor

Pointwise-equal flat readers produce the same ordered accumulator reduction.

theorem TorchLean.Tensor.Internal.Lowering.reduceNonemptyFoldTensorFromFlat_eq {α : Type u} [Storage α] (step : α → α → α) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) (read : Fin checked.value.normalized.input.size → α) (hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : reduceNonemptyFoldTensorFromFlat step checked hKind hPositive inputTensor read hRead = reduceNonemptyFoldTensor step checked hKind hPositive inputTensor

Pointwise-equal flat readers produce the same ordered nonempty reduction.

theorem TorchLean.Tensor.Internal.Lowering.reduceTensorFromFlat_correct {α : Type u} {β : Type v} [Storage α] [Storage β] (aggregate : Multiset α → β) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) (read : Fin checked.value.normalized.input.size → α) (hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : reduceTensorFromFlat aggregate checked hKind inputTensor read hRead = Semantics.denoteReduce aggregate checked hKind inputTensor

The fused flat-reader kernel implements the independent multiset reduction semantics.

theorem TorchLean.Tensor.Internal.Lowering.reduceFoldTensorFromFlat_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 α) (read : Fin checked.value.normalized.input.size → α) (hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : reduceFoldTensorFromFlat step initial finish checked hKind inputTensor read hRead = Semantics.denoteOrderedReduce step initial finish checked hKind inputTensor

The fused flat-reader accumulator preserves the independent row-major ordered reduction semantics.

theorem TorchLean.Tensor.Internal.Lowering.reduceNonemptyFoldTensorFromFlat_ordered_correct {α : Type u} [Storage α] (step : α → α → α) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) (read : Fin checked.value.normalized.input.size → α) (hRead : ∀ (inputIndex : Fin checked.value.normalized.input.size), read inputIndex = Rep.getFlat inputTensor inputIndex) : reduceNonemptyFoldTensorFromFlat step checked hKind hPositive inputTensor read hRead = Semantics.denoteOrderedReduceNonempty step checked hKind hPositive inputTensor

The fused flat-reader nonempty accumulator preserves the independent ordered nonempty reduction semantics.