theorem Hex.GraphIso.Nauty.Sparse.Sort.Sorted.pairwise {lab hits : Array Nat} {first len : Nat} (h : Sorted lab hits first len) : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) (List.map (fun (v : Nat) => hits[v]!) (segN lab first len))

Sorting an indirect segment orders its literal sequence of keys.

theorem Hex.GraphIso.Nauty.Sparse.Sort.Sorted.keys_eq {lab hits : Array Nat} {first len : Nat} {out keys : Array Nat} {q : Nat} (ha : Sorted lab hits first len) (hb : Sorted out keys first len) (hp : (List.map (fun (v : Nat) => hits[v]!) (segN lab first len)).Perm (List.map (fun (v : Nat) => keys[v]!) (segN out first len))) (hq : first ≤ q) (he : q < first + len) : hits[lab[q]!]! = keys[out[q]!]!

Equal key multisets have the same sorted key at every position, even when equal-key vertices are reordered.

theorem Hex.GraphIso.Nauty.Sparse.CountPartition.eq_ptn {level first last : Nat} {lab hits before ptn out keys other : Array Nat} (ha : CountPartition level first last lab hits before ptn) (hb : CountPartition level first last out keys before other) (hk : ∀ (q : Nat), first ≤ q → q ≤ last → hits[lab[q]!]! = keys[out[q]!]!) : ptn = other

Equal count sequences determine the complete partition array written by count splitting, including all unchanged exterior values.