Algebraic contraction planning

This module isolates the mathematical certificate used when a generated einsum kernel changes the nesting order of contracted axes. A permutation of duplicate-free logical axes induces an equivalence of coordinate spaces. Coordinate sums may be transported across that equivalence only when addition is commutative, so ordered scalar folds keep their original traversal.

def TorchLean.Tensor.Internal.Lowering.coordinatePermutationEquiv {ι : Type u} [BEq ι] [LawfulBEq ι] (length : ι → ℕ) {original planned : List ι} (hOriginal : original.Nodup) (hPermutation : planned.Perm original) : Coord (List.map length planned) ≃ Coord (List.map length original)

A permutation of duplicate-free axes induces an equivalence between their row-major coordinate spaces.

The equivalence changes only the order in which coordinates are presented. Each named axis retains its original length and bounded coordinate.

theorem TorchLean.Tensor.Internal.Lowering.coordinateSum_permute {R : Type v} [AddCommMonoid R] {ι : Type u} [BEq ι] [LawfulBEq ι] (length : ι → ℕ) {original planned : List ι} (hOriginal : original.Nodup) (hPermutation : planned.Perm original) (values : Coord (List.map length original) → R) (initial : R) : Semantics.coordinateSum (List.map length planned) (fun (coordinate : Coord (List.map length planned)) => values ((coordinatePermutationEquiv length hOriginal hPermutation) coordinate)) initial = Semantics.coordinateSum (List.map length original) values initial

Changing the nesting order of contracted axes preserves a coordinate sum when the scalar addition is commutative.

The executable planner uses this theorem as its only algebraic permission to reorder contraction coordinates. In particular, no corresponding theorem is available for merely ordered floating-point addition.

theorem TorchLean.Tensor.Internal.Lowering.coordinateSum_permute_of_eq {R : Type v} [AddCommMonoid R] {ι : Type u} [BEq ι] [LawfulBEq ι] (length : ι → ℕ) {original planned : List ι} (hOriginal : original.Nodup) (hPermutation : planned.Perm original) (coordinateMap : Coord (List.map length planned) → Coord (List.map length original)) (hCoordinateMap : ∀ (coordinate : Coord (List.map length planned)), coordinateMap coordinate = (coordinatePermutationEquiv length hOriginal hPermutation) coordinate) (values : Coord (List.map length original) → R) (initial : R) : Semantics.coordinateSum (List.map length planned) (fun (coordinate : Coord (List.map length planned)) => values (coordinateMap coordinate)) initial = Semantics.coordinateSum (List.map length original) values initial

An executable coordinate map may use a compiler-generated direct projection instead of evaluating the abstract permutation equivalence.

Pointwise equality with the equivalence is sufficient to retain the same coordinate-sum certificate.