Reduction semantics

Independent unordered and row-major ordered denotations for checked reductions, together with their aggregation and differential laws.

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

Independent reduction denotation: apply aggregate to the multiset of input values in each certified input-to-output coordinate fiber.

Using a multiset makes permutation invariance part of the function's type and allows the output scalar type to differ from the input scalar type.

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

Independent denotation for a reducer that is defined only on nonempty fibers.

The positive fiber-size premise is shape-level evidence that every aggregate application receives at least one value.

noncomputable def TorchLean.Tensor.Internal.Semantics.orderedReductionValues {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : List α

Values in one reduction fiber, listed in physical row-major order.

The coordinate equivalence supplies the same fiber used by denoteReduce, while List.ofFn fixes an order that remains meaningful for IEEE floating point operations and other nonassociative scalar functions.

@[simp]

theorem TorchLean.Tensor.Internal.Semantics.orderedReductionValues_length {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : (orderedReductionValues checked hKind inputTensor outputCoordinate).length = checked.reductionFiberSize

The ordered fiber list has the checked reduction-fiber cardinality.

theorem TorchLean.Tensor.Internal.Semantics.orderedReductionValues_ne_nil {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : orderedReductionValues checked hKind inputTensor outputCoordinate ≠ []

A positive checked fiber size makes every ordered fiber list nonempty.

noncomputable def TorchLean.Tensor.Internal.Semantics.denoteOrderedReduce {α : 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 γ

Ordered reduction denotation with an explicit initial accumulator.

The list fold visits removed-axis coordinates in row-major order. The finalizer also receives the checked fiber cardinality, which supports operations such as mean without recounting the list.

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

Ordered reduction denotation initialized from the first fiber value.

This form gives minimum and maximum a precise IEEE behavior without sentinel values. Positivity of the checked fiber size proves that the first value exists; the remaining row-major values are folded from left to right.

theorem TorchLean.Tensor.Internal.Semantics.denoteReduce_sum_apply_reconstructed {α : Type u} [Storage α] [AddCommMonoid α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) (inputCoordinate : AxisTuple checked.value.axisLength (List.filter (fun (axis : Check.AxisId) => !checked.value.normalized.outputAxes.contains axis) checked.value.normalized.inputAxes) → Coord checked.value.normalized.input) (retainsOutput : ∀ (reducedCoordinate : AxisTuple checked.value.axisLength (List.filter (fun (axis : Check.AxisId) => !checked.value.normalized.outputAxes.contains axis) checked.value.normalized.inputAxes)), checked.outputCoordinateOfInput ⋯ (inputCoordinate reducedCoordinate) = outputCoordinate) (recoversReduction : ∀ (reducedCoordinate : AxisTuple checked.value.axisLength (List.filter (fun (axis : Check.AxisId) => !checked.value.normalized.outputAxes.contains axis) checked.value.normalized.inputAxes)), AxisTuple.select ⋯ (checked.inputTensorCoordinateEquiv (inputCoordinate reducedCoordinate)) = reducedCoordinate) : Rep.get (denoteReduce Multiset.sum checked hKind inputTensor) outputCoordinate = ∑ reducedCoordinate : AxisTuple checked.value.axisLength (List.filter (fun (axis : Check.AxisId) => !checked.value.normalized.outputAxes.contains axis) checked.value.normalized.inputAxes), Rep.get inputTensor (inputCoordinate reducedCoordinate)

Evaluate a sum reduction using any explicit reconstruction of the complete input coordinate from the retained output coordinate and removed-axis coordinates.

The premises state exactly that the reconstruction remains in the requested output fiber and recovers every supplied removed-axis tuple. This form is independent of rank and is convenient when relating einops reductions to established finite-sum operations.

theorem TorchLean.Tensor.Internal.Semantics.sum_denoteReduce_sum {α : Type u} [Storage α] [AddCommMonoid α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor α) : ∑ outputCoordinate : Coord checked.value.output, Rep.get (denoteReduce Multiset.sum checked hKind inputTensor) outputCoordinate = ∑ inputCoordinate : Coord checked.value.normalized.input, Rep.get inputTensor inputCoordinate

Sum reduction preserves the total additive sum of all tensor entries.

The output fibers partition the finite input-coordinate space, including when that space is empty.

theorem TorchLean.Tensor.Internal.Semantics.dot_denoteReduce_sum {R : Type u} [Storage R] [Semiring R] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (inputTensor : checked.InputTensor R) (outputTensor : checked.OutputTensor R) : Rep.dot (denoteReduce Multiset.sum checked hKind inputTensor) outputTensor = Rep.dot inputTensor (Rep.pull (checked.outputCoordinateOfInput ⋯) outputTensor)

The adjoint of sum reduction under the finite tensor pairing is pullback along the retained-coordinate projection.

At the tensor level this pullback broadcasts each output cotangent across all input coordinates in its reduction fiber, which is the algebraic core of the sum-reduction VJP.

theorem TorchLean.Tensor.Internal.Semantics.sum_minEqualShareTieWeight {R : Type u} [Storage R] [Field R] [LinearOrder R] [CharZero R] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor R) (outputCoordinate : Coord checked.value.output) : ∑ inputCoordinate : Fiber (checked.outputCoordinateOfInput ⋯) outputCoordinate, Rep.equalShareTieWeight Reduction.min (checked.outputCoordinateOfInput ⋯) ⋯ inputTensor outputCoordinate inputCoordinate = 1

The equal-share weights of minimum reduction sum to one in every checked nonempty fiber.

Consequently, when n input coordinates share the minimum, each receives weight 1 / n. This is the library's explicit minimum tie convention.

theorem TorchLean.Tensor.Internal.Semantics.sum_maxEqualShareTieWeight {R : Type u} [Storage R] [Field R] [LinearOrder R] [CharZero R] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor : checked.InputTensor R) (outputCoordinate : Coord checked.value.output) : ∑ inputCoordinate : Fiber (checked.outputCoordinateOfInput ⋯) outputCoordinate, Rep.equalShareTieWeight Reduction.max (checked.outputCoordinateOfInput ⋯) ⋯ inputTensor outputCoordinate inputCoordinate = 1

The equal-share weights of maximum reduction sum to one in every checked nonempty fiber.

Consequently, when n input coordinates share the maximum, each receives weight 1 / n. This is the library's explicit maximum tie convention.

theorem TorchLean.Tensor.Internal.Semantics.dot_equalShareTieReduce {R : Type u} [Storage R] [Field R] [DecidableEq R] (aggregate : (values : Multiset R) → values ≠ 0 → R) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hPositive : 0 < checked.reductionFiberSize) (inputTensor inputTangent : checked.InputTensor R) (outputCotangent : checked.OutputTensor R) : (Rep.equalShareTieDifferential aggregate (checked.outputCoordinateOfInput ⋯) ⋯ inputTensor inputTangent).dot outputCotangent = Rep.dot inputTangent (Rep.equalShareTieVjp aggregate (checked.outputCoordinateOfInput ⋯) ⋯ inputTensor outputCotangent)

The equal-share linearization of any checked nonempty reducer is adjoint to its equal-share VJP.

For Reduction.min and Reduction.max, the preceding normalization theorems show that this splits cotangent equally among all tied extrema. At a tie this is a named symmetric generalized derivative, not a claim of unique classical differentiability.

theorem TorchLean.Tensor.Internal.Semantics.dot_denoteMeanReduce {R : Type u} [Storage R] [DivisionRing R] [CharZero R] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.reduce) (hNonempty : 0 < checked.reductionFiberSize) (inputTangent : checked.InputTensor R) (outputCotangent : checked.OutputTensor R) : Rep.dot (denoteReduceNonempty Reduction.mean checked hKind hNonempty inputTangent) outputCotangent = Rep.dot inputTangent (Rep.map (fun (value : R) => (↑checked.reductionFiberSize)⁻¹ * value) (Rep.pull (checked.outputCoordinateOfInput ⋯) outputCotangent))

The VJP of a checked mean reduction broadcasts the output cotangent and scales it by the reciprocal of the reduction-fiber size.

The denominator is the product of the removed axis lengths certified by the checked pattern. Positivity rules out an empty mean, while CharZero ensures that this positive natural number remains nonzero in the scalar division ring.