theorem Hex.GraphIso.Nauty.leafExit_coset {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.cosetindex = st.cosetindex

Leaf actions preserve the coset index selected by first-path descent.

theorem Hex.GraphIso.Nauty.compare_coset {n : Nat} {κ : Type} (level code : Nat) (st : SearchState n κ) : (compareCodes level code st).cosetindex = st.cosetindex

Local off-path operations retain the coset index.

theorem Hex.GraphIso.Nauty.classify_coset {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).snd.cosetindex = st.cosetindex

Classification changes scratch data without changing the coset index.

theorem Hex.GraphIso.Nauty.recover_coset {n : Nat} {κ : Type} (inf level : Nat) (st : SearchState n κ) : (recover inf level st).cosetindex = st.cosetindex

Recovery preserves the current coset index.

theorem Hex.GraphIso.Nauty.node_coset {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) : (node false ctx inf tcLevel fuel level numcells st).snd.cosetindex = st.cosetindex

Off-path recursion never overwrites the suspended first child's index.