theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_coset {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : (chooseTarget first g tcLevel level numcells st).snd.snd.snd.cosetindex = st.cosetindex

Native target selection borrows scratch without changing the index selected by the most recent first-path descent.

theorem Hex.GraphIso.Nauty.Sparse.classify_coset {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : (classify g level numcells st).snd.cosetindex = st.cosetindex

theorem Hex.GraphIso.Nauty.Sparse.node_coset {n : Nat} (g : Graph n) (inf tcLevel fuel level numcells : Nat) (st : State n) : (Generic.node false g inf tcLevel fuel level numcells st).snd.cosetindex = st.cosetindex

Complete native off-path recursion retains the suspended first child's index through every filter, recovery and nonlocal return.