theorem Hex.GraphIso.Nauty.Sparse.Sort.Window.map {before after : Array Nat} {first last : Nat} (h : Window before after first last) (f : Nat → Nat) : Window (Array.map f before) (Array.map f after) first last

Mapping vertex names preserves the support of a label permutation, including the default reads beyond both arrays.

theorem Hex.GraphIso.Nauty.Sparse.binary_cells_map {before lab : Array Nat} {first last : Nat} {other out ptn : Array Nat} {level cut : Nat} (f : Nat → Nat) (hs : «Sort».Window before lab first last) (ht : «Sort».Window other out first last) (hbs : last ≤ before.size) (hbt : last ≤ other.size) (hbp : last ≤ ptn.size) (hc : IsCell ptn level first (last - first)) (hf : first ≤ cut) (he : cut ≤ last) (hp : cellsPerm ptn level other (Array.map f before)) (hl : (segN out first (cut - first)).Perm (segN (Array.map f lab) first (cut - first))) (hr : (segN out cut (last - cut)).Perm (segN (Array.map f lab) cut (last - cut))) : cellsPerm (if cut ≠ last ∧ cut ≠ first then ptn.set! (cut - 1) level else ptn) level out (Array.map f lab)

Two transported binary fragments and their exterior windows determine cell equivalence for the entire updated partition. Uniform classes retain the old partition and use the whole-window permutation contract.