Reduction index laws

Reduction lowering enumerates retained output coordinates and removed-axis coordinates separately. These laws combine those counters into one row-major coordinate and identify the resulting compact arithmetic with the independent checked reduction reconstruction.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.separatedRearrangeLinearIndex {ι : Type u_1} [BEq ι] (length : ι → ℕ) (source left right : List ι) (leftIndex rightIndex : ℕ) : ℕ

Compute a selected row-major index by decoding retained and reduced counters separately.

In the combined counter, retained axes occupy the high-order digits and reduced axes occupy the low-order digits. The resulting coordinates are then selected in source-axis order. Keeping the counters separate gives native reduction loops an index program without changing the checked coordinate semantics.

theorem TorchLean.Tensor.Internal.Lowering.Reduce.Impl.separatedRearrangeLinearIndex_eq {ι : Type u_1} [BEq ι] [LawfulBEq ι] (length : ι → ℕ) (source left right : List ι) (hSource : ∀ axis ∈ source, axis ∈ left ++ right) (leftIndex : Fin (Shape.size (List.map length left))) (rightIndex : Fin (Shape.size (List.map length right))) : separatedRearrangeLinearIndex length source left right ↑leftIndex ↑rightIndex = rearrangeLinearIndex length source (left ++ right) (↑rightIndex + Shape.size (List.map length right) * ↑leftIndex)

Separately decoded row-major counters select the same source index as their single combined row-major counter.

def TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionLinearIndex (checked : Check.CheckedTransform) (outputIndex : Fin checked.value.output.size) (reducedIndex : Fin checked.reductionShape.size) : ℕ

Compute a reduction input index as one compact row-major selection.

The removed-axis counter occupies the low-order digits because reduction fibers are traversed inside each retained output coordinate.

theorem TorchLean.Tensor.Internal.Lowering.Reduce.Impl.reductionInputFlatIndex_val (checked : Check.CheckedTransform) (outputIndex : Fin checked.value.output.size) (reducedIndex : Fin checked.reductionShape.size) : ↑(reductionInputFlatIndex checked (Coord.unlinearize outputIndex) reducedIndex) = reductionLinearIndex checked outputIndex reducedIndex

The compact row-major reduction index equals the independent reconstructed input coordinate.