theorem Hex.GraphIso.Nauty.Sparse.child_valid {n : Nat} (first : Bool) (level tc tv : Nat) (st : State n) (h : Scratch.Bounded n st.canong.scratch) : have out := Generic.Policy.child first level tc tv st; Scratch.Valid n out.lab out.ptn (level + 1) out.canong.scratch

Individualization retains allocated scratch and invalidates the indices in the actual sparse policy before exposing the child partition.

theorem Hex.GraphIso.Nauty.Sparse.recover_valid {n : Nat} (inf level : Nat) (st : State n) (h : Scratch.Bounded n st.canong.scratch) : have out := Generic.Policy.recover inf level st; Scratch.Valid n out.lab out.ptn level out.canong.scratch

The sparse policy's recovery invalidates indices after reopening the parent partition, preserving the allocation and generation bounds.

theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_valid {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) (h : Scratch.Valid n st.lab st.ptn level st.canong.scratch) : have out := (chooseTarget first g tcLevel level numcells st).snd.snd.snd; Scratch.Valid n out.lab out.ptn level out.canong.scratch

Target selection's guards, optional hint, borrowed hit array, and bookkeeping updates all preserve scratch validity for the returned state.

theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_bounded {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) (h : Scratch.Bounded n st.canong.scratch) : Scratch.Bounded n (chooseTarget first g tcLevel level numcells st).snd.snd.snd.canong.scratch

The target policy preserves allocation and generation bounds independently of cell-index correctness.