theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_bounded {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) (h : Scratch.Bounded n s.toScratch) : Scratch.Bounded n (splitSingleton g level split s).toScratch

The complete singleton pass preserves persistent allocation and generation bounds, including the borrowed arrays and reverse scatter of hit vertices.

theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_bounded {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) (h : Scratch.Bounded n s.toScratch) : Scratch.Bounded n (splitNontrivial g level split s).toScratch

First-touch clearing, neighbour accumulation, and all following count splits preserve the persistent scratch allocation and generation bounds.