theorem Hex.GraphIso.Nauty.Sparse.Sort.Window.cells {before after : Array Nat} {first last : Nat} {ptn : Array Nat} {level : Nat} (h : Window before after first last) (hf : first ≤ last) (hb : last ≤ before.size) (hc : IsCell ptn level first (last - first)) : cellsPerm ptn level after before

A permutation confined to one complete cell preserves the multiset of vertices in every old cell.

theorem Hex.GraphIso.Nauty.Sparse.Cuts.perm {n level old count upto : Nat} {before ptn lab out : Array Nat} (h : Cuts level n before ptn old count upto) (hp : before.size = n) (hl : lab.size = n) (ho : out.size = n) (hend : before[n - 1]! ≤ level) (hc : cellsPerm ptn level out lab) : cellsPerm before level out lab

Cell permutations after refinement also preserve each original cell, because every original closed boundary remains closed.