theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_boundary {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : Boundary level s.ptn (splitSingleton g level split s).ptn

theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_boundary {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : Boundary level s.ptn (splitNontrivial g level split s).ptn

theorem Hex.GraphIso.Nauty.Sparse.refineWith_boundary {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) : Boundary level ptn (refineWith g level lab ptn active numcells scratch).ptn

Distance refinement and the full active-cell loop preserve the allocation and existing closed boundaries of the incoming partition.