theorem Hex.GraphIso.Nauty.Sparse.sortCells_perm (xs : Array Nat) : (sortCells xs).toList.Perm xs.toList

Touched-cell sorting retains all recorded cells and their multiplicities.

theorem Hex.GraphIso.Nauty.Sparse.sortCells_order (xs : Array Nat) : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) (sortCells xs).toList

The executed tiny-sort specialization shares this ascending order contract.

theorem Hex.GraphIso.Nauty.Sparse.Touched.sorted {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} (h : Touched n stamp before marks touched seen) : Touched n stamp before marks (sortCells touched) seen

Sorting preserves first-touch coverage and uniqueness.