theorem Hex.GraphIso.Nauty.Sparse.Index.Two.of_scatter {n first cut last : Nat} {lab oldstarts starts : Array Nat} (h : Scatter n lab oldstarts starts cut last cut) (hp : lab.toList.Perm (List.range n)) (_hf : first < cut) (hl : cut < last) (hb : last ≤ n) (hc : ∀ (q : Nat), first ≤ q → q < cut → oldstarts[lab[q]!]! = first) : have middle := if cut = first + 1 then starts.setIfInBounds lab[first]! n else starts; have out := if last = cut + 1 then middle.setIfInBounds lab[cut]! n else middle; Two n first cut last last lab out

The singleton splitter normalizes singleton sentinels after its reverse scatter has assigned the second fragment's start.

theorem Hex.GraphIso.Nauty.Sparse.Index.Frame.sentinels {n first cut last : Nat} {lab oldlab oldstarts starts oldends ends : Array Nat} (h : Frame n first (last - 1) oldlab lab oldstarts starts oldends ends) (hp : lab.toList.Perm (List.range n)) (hf : first < cut) (hl : cut < last) (hb : last ≤ n) : have middle := if cut = first + 1 then starts.setIfInBounds lab[first]! n else starts; have out := if last = cut + 1 then middle.setIfInBounds lab[cut]! n else middle; Frame n first (last - 1) oldlab lab oldstarts out oldends ends

Sentinel normalization retains all cache entries outside the split.