Adjacent swaps and row-major coordinates

The tensor evaluator's swaps are coordinate bijections. Encoding their coordinates with the runtime's multiplication-and-addition loop agrees with ordinary tensor linearization.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.coord_toList_length (s : Spec.Shape) (c : s.Coord) : (Spec.Shape.Coord.toList s c).length = List.length s

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.swapCoordinate_toList (s : Spec.Shape) (depth : ℕ) (c : (s.swapAdjacentAtDepth depth).Coord) : Spec.Shape.Coord.toList s (Proofs.TensorAxis.swapCoordinate s depth c) = Spec.Shape.swapAdjacentAxes (Spec.Shape.Coord.toList (s.swapAdjacentAtDepth depth) c) depth

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.swapCoordinate_bijective (s : Spec.Shape) (depth : ℕ) : Function.Bijective (Proofs.TensorAxis.swapCoordinate s depth)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.permutedCoordinate_bijective (s : Spec.Shape) (swaps : List ℕ) : Function.Bijective (Proofs.TensorAxis.permutedCoordinate s swaps)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.permutedCoordinate_toList (s : Spec.Shape) (swaps : List ℕ) (c : (s.applyAdjacentSwaps swaps).Coord) : Spec.Shape.Coord.toList s (Proofs.TensorAxis.permutedCoordinate s swaps c) = List.foldl Spec.Shape.swapAdjacentAxes (Spec.Shape.Coord.toList (s.applyAdjacentSwaps swaps) c) swaps.reverse

noncomputable def NN.MLTheory.CROWN.Graph.DirectedBackward.adjacentCoordinateEquiv (s : Spec.Shape) (swaps : List ℕ) : s.Coord ≃ (s.applyAdjacentSwaps swaps).Coord

Forward transport of an input coordinate through the evaluator's actual swaps.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.adjacentCoordinateEquiv_toList (s : Spec.Shape) (swaps : List ℕ) (c : s.Coord) : Spec.Shape.Coord.toList (s.applyAdjacentSwaps swaps) ((adjacentCoordinateEquiv s swaps) c) = List.foldl Spec.Shape.swapAdjacentAxes (Spec.Shape.Coord.toList s c) swaps

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.someTensor_swapFold {β : Type} [TorchLean.Storage β] {s : Spec.Shape} (x : TorchLean.Tensor β s) (swaps : List ℕ) : List.foldl Spec.SomeTensor.swapAdjacentAtDepth { shape := s, tensor := x } swaps = { shape := s.applyAdjacentSwaps swaps, tensor := x.permuteByAdjacentSwaps swaps }

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.permuteByAdjacentSwaps_coordinate {β : Type} [TorchLean.Storage β] {s : Spec.Shape} (x : TorchLean.Tensor β s) (swaps : List ℕ) (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (x.permuteByAdjacentSwaps swaps) ((adjacentCoordinateEquiv s swaps) c) = TorchLean.Tensor.Internal.Rep.get x c

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.adjacentSwaps_size (s : Spec.Shape) (swaps : List ℕ) : (s.applyAdjacentSwaps swaps).size = s.size

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.range_map_getElem! (xs : List ℕ) : List.map (fun (i : ℕ) => xs[i]!) (List.range xs.length) = xs

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.swapFold_eq_axis_map (xs swaps : List ℕ) : List.foldl Spec.Shape.swapAdjacentAxes xs swaps = List.map (fun (i : ℕ) => xs[i]!) (List.foldl Spec.Shape.swapAdjacentAxes (List.range xs.length) swaps)