theorem Hex.GraphIso.Nauty.Sparse.indexCells_size (n : Nat) (lab ptn : Array Nat) (level : Nat) (starts ends : Array Nat) : have out := indexCells n lab ptn level starts ends; out.fst.size = starts.size ∧ out.snd.size = ends.size

Index rebuilding retains both allocations, independently of index contents and partition validity.

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

The complete executed refinement preserves scratch allocation and mark generation bounds, including distance initialization and both splitter paths.

theorem Hex.GraphIso.Nauty.Sparse.refine_bounded {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : Scratch.Bounded n (refine g level lab ptn active numcells).toScratch

theorem Hex.GraphIso.Nauty.Sparse.visit_bounded {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) (h : Scratch.Bounded n st.canong.scratch) : Scratch.Bounded n (visit g level numcells st).snd.snd.canong.scratch

Visiting a production-search node retains the same persistent bounds.