Row-major composition laws

These laws connect structural coordinate composition with the flat row-major indices used by native lowering. They are independent of any einops operation.

theorem TorchLean.Tensor.Internal.AxisTuple.values_append {ι : Type u_1} {length : ι → ℕ} {left right : List ι} (leftCoordinate : AxisTuple length left) (rightCoordinate : AxisTuple length right) : (List.ofFn fun (index : Fin (left ++ right).length) => ↑(append left leftCoordinate rightCoordinate index)) = (List.ofFn fun (index : Fin left.length) => ↑(leftCoordinate index)) ++ List.ofFn fun (index : Fin right.length) => ↑(rightCoordinate index)

The row-major values of appended named-axis coordinates are the values of the left coordinate followed by the values of the right coordinate.

theorem TorchLean.Tensor.Internal.Coord.linearize_appendEquiv_symm_val (left right : Shape) (leftCoordinate : Coord left) (rightCoordinate : Coord right) : ↑((appendEquiv left right).symm (leftCoordinate, rightCoordinate)).linearize = ↑rightCoordinate.linearize + right.size * ↑leftCoordinate.linearize

Appending two coordinates places the right coordinate in the low-order row-major digits and the left coordinate in the high-order digits.

theorem TorchLean.Tensor.Internal.AxisTuple.linearize_append_val {ι : Type u_1} {length : ι → ℕ} (left right : List ι) (leftCoordinate : AxisTuple length left) (rightCoordinate : AxisTuple length right) : ↑((coordEquiv length (left ++ right)).symm (append left leftCoordinate rightCoordinate)).linearize = ↑((coordEquiv length right).symm rightCoordinate).linearize + Shape.size (List.map length right) * ↑((coordEquiv length left).symm leftCoordinate).linearize

Linearizing appended named-axis coordinates has the same row-major formula as appending their ordinary coordinate representations.