theorem Hex.GraphIso.Nauty.Sparse.splitCounts_bounded {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (h : Scratch.Bounded n s.toScratch) : Scratch.Bounded n (splitCounts level first distance s).toScratch

Dividing a cell preserves persistent allocation and generation bounds. Correctness of the newly written cell indices is established separately.

theorem Hex.GraphIso.Nauty.Sparse.Storage.invalidate_valid {n : Nat} (s : Storage n) (h : Scratch.Bounded n s.scratch) (lab ptn : Array Nat) (level : Nat) : Scratch.Valid n lab ptn level s.invalidate.scratch

The actual search invalidation permits the individualized or recovered partition while retaining all persistent storage bounds.

theorem Hex.GraphIso.Nauty.Sparse.Storage.update_valid {n : Nat} (g : Graph n) (s : Storage n) (lab ptn : Array Nat) (level same : Nat) (h : Scratch.Valid n lab ptn level s.scratch) : Scratch.Valid n lab ptn level (update g s lab same).scratch

Canonical installation changes only canonical rows, preserving scratch validity for the current partition.