Inverting the front-axis permutation

The checked inverse-permutation algorithm fills an optional index table and then reads it in axis order. Its loop invariant identifies each written entry by its inverse position. Specializing the invariant to a front-axis rotation gives the permutation used to restore an arbitrary concat axis after concatenating along the leading axis.

theorem NN.MLTheory.CROWN.Graph.range_split_axis (axis trailing : ℕ) : List.range (axis + 1 + trailing) = List.range axis ++ axis :: List.range' (axis + 1) trailing

The axis indices of a rank split at a selected axis into the preceding and following axes.

theorem NN.MLTheory.CROWN.Graph.inversePerm_front (axis trailing : ℕ) : IR.OpContracts.inversePerm (axis :: (List.range axis ++ List.range' (axis + 1) trailing)).toArray = Except.ok (List.range' 1 axis ++ [0] ++ List.range' (axis + 1) trailing).toArray

Inverting a front-axis rotation restores the original order of the preceding axes.