Adjacent swaps for arbitrary-axis concatenation

The concat evaluator moves the selected axis to the front, concatenates there, and moves it back. The proofs below connect its adjacent swaps to the independent coordinate map for tensor concatenation.

theorem NN.MLTheory.CROWN.Graph.swapAdjacentAxes_reverse_range (leading trailing : List ℕ) (axis : ℕ) : List.foldl Spec.Shape.swapAdjacentAxes (leading ++ axis :: trailing) (List.range leading.length).reverse = axis :: (leading ++ trailing)

Moving an axis left through its preceding axes preserves their relative order.

theorem NN.MLTheory.CROWN.Graph.permMoveAxisToFront_append (leading trailing : Spec.Shape) (length : ℕ) : IR.OpContracts.permMoveAxisToFront (List.length leading) (leading ++ length :: trailing) = Except.ok (List.length leading :: (List.range (List.length leading) ++ List.range' (List.length leading + 1) (List.length trailing))).toArray

The public front-axis contract returns the structural rotation used by the swap proof.

theorem NN.MLTheory.CROWN.Graph.swapDepthsForPerm_front (axis trailing : ℕ) : IR.Graph.swapDepthsForPerm (axis :: (List.range axis ++ List.range' (axis + 1) trailing)).toArray (axis + 1 + trailing) = Except.ok (List.range axis).reverse.toArray

The actual permutation planner moves one selected axis to the front by adjacent swaps.

theorem NN.MLTheory.CROWN.Graph.swapDepthsForPerm_back (axis trailing : ℕ) : IR.Graph.swapDepthsForPerm (List.range' 1 axis ++ 0 :: List.range' (axis + 1) trailing).toArray (axis + 1 + trailing) = Except.ok (List.range axis).toArray

The inverse rotation moves the leading axis right, one adjacent swap at each position.

def NN.MLTheory.CROWN.Graph.concatAxisToFront {α : Type} [TorchLean.Storage α] (leading trailing : Spec.Shape) {length : ℕ} (tensor : TorchLean.Tensor α (leading ++ length :: trailing)) : TorchLean.Tensor α (length :: (leading ++ trailing))

Move the selected axis to the front by its independent coordinate map.

theorem NN.MLTheory.CROWN.Graph.concatAxisToFront_concatenateAxes {α : Type} [TorchLean.Storage α] (leading trailing : Spec.Shape) (lengths : List ℕ) (values : (parent : Fin lengths.length) → TorchLean.Tensor α (leading ++ lengths.get parent :: trailing)) : concatAxisToFront leading trailing (TorchLean.Tensor.Internal.Rep.concatenateAxes leading trailing lengths values) = TorchLean.Tensor.Internal.Rep.concatenateAxes [] (leading ++ trailing) lengths fun (parent : Fin lengths.length) => concatAxisToFront leading trailing (values parent)

Moving the selected axis to the front commutes with family concatenation.

theorem NN.MLTheory.CROWN.Graph.permuteSomeTensor_front_of_ok {α : Type} [TorchLean.Storage α] [Context α] (leading trailing : Spec.Shape) {length : ℕ} (tensor : TorchLean.Tensor α (leading ++ length :: trailing)) (result : Spec.SomeTensor α) (heval : IR.Graph.permuteSomeTensor (Spec.SomeTensor.ofTensor tensor) (List.length leading :: (List.range (List.length leading) ++ List.range' (List.length leading + 1) (List.length trailing))).toArray = Except.ok result) : result = Spec.SomeTensor.ofTensor (concatAxisToFront leading trailing tensor)

A successful runtime front permutation reads exactly the independently rotated coordinates.

theorem NN.MLTheory.CROWN.Graph.permuteSomeTensor_back_of_ok {α : Type} [TorchLean.Storage α] [Context α] (leading trailing : Spec.Shape) {length : ℕ} (tensor : TorchLean.Tensor α (leading ++ length :: trailing)) (result : Spec.SomeTensor α) (heval : IR.Graph.permuteSomeTensor (Spec.SomeTensor.ofTensor (concatAxisToFront leading trailing tensor)) (List.range' 1 (List.length leading) ++ 0 :: List.range' (List.length leading + 1) (List.length trailing)).toArray = Except.ok result) : result = Spec.SomeTensor.ofTensor tensor

A successful inverse runtime permutation restores a tensor after its front rotation.