theorem Hex.GraphIso.Nauty.Sparse.Sort.children_append (start len left right : Nat) (rest : List (Nat × Nat)) : children start len left right rest = children start len left right [] ++ rest

theorem Hex.GraphIso.Nauty.Sparse.Sort.Separated.pending {x y : Array Nat} {start len v left right : Nat} (h : Separated x y start (start + len) v (start + left) (start + len - right)) (hr : right ≤ len) : Pending x y start (start + len) (children start len left right [])

theorem Hex.GraphIso.Nauty.Sparse.Sort.Sorted.pending {x y : Array Nat} {start len : Nat} (h : Sorted x y start len) : Pending x y start (start + len) []

theorem Hex.GraphIso.Nauty.Sparse.Sort.indirect_sorted (x y : Array Nat) (start len : Nat) (hb : start + len ≤ x.size) : Sorted (indirect x y start len) y start len

The complete executed indirect sort orders its requested segment. The proof uses the actual smaller-side-first stack, its established exhaustion bound, and the exact partition and insertion operations.