theorem Hex.GraphIso.Nauty.Sparse.Sort.partition_perm (x y : Array Nat) (start len : Nat) : (partition x y start len).fst.toList.Perm x.toList

Every partition operation is a swap, including the equal-pivot blocks.

theorem Hex.GraphIso.Nauty.Sparse.Sort.partition_size (x y : Array Nat) (start len : Nat) : (partition x y start len).fst.size = x.size

theorem Hex.GraphIso.Nauty.Sparse.Sort.insertion_size (x y : Array Nat) (start len : Nat) : (insertion x y start len).size = x.size

theorem Hex.GraphIso.Nauty.Sparse.Sort.insertion_perm (x y : Array Nat) (start len : Nat) (h : start + len ≤ x.size) : (insertion x y start len).toList.Perm x.toList

theorem Hex.GraphIso.Nauty.Sparse.Sort.partition_bounds (x y : Array Nat) (start len : Nat) : (partition x y start len).snd.fst ≤ len ∧ (partition x y start len).snd.snd ≤ len

Both returned subsegments lie in the segment passed to partition.

theorem Hex.GraphIso.Nauty.Sparse.Sort.indirect_size (x y : Array Nat) (start len : Nat) : (indirect x y start len).size = x.size

theorem Hex.GraphIso.Nauty.Sparse.Sort.indirect_perm (x y : Array Nat) (start len : Nat) (h : start + len ≤ x.size) : (indirect x y start len).toList.Perm x.toList

The exact indirect sort preserves every entry, including its repeated keys. The work stack contains only subsegments of the original array.