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

Code bookkeeping preserves arbitrary canonical storage.

theorem Hex.GraphIso.Nauty.SearchState.terminal_storage {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (firstterminal level st).canong = st.canong

theorem Hex.GraphIso.Nauty.SearchState.scatter_storage {n : Nat} {κ : Type} (ref : Array Nat) (st : SearchState n κ) : (scatter ref st).canong = st.canong

theorem Hex.GraphIso.Nauty.SearchState.push_storage {n : Nat} {κ : Type} (st : SearchState n κ) (pair : VSet n × VSet n) : (pushAuto st pair).canong = st.canong

theorem Hex.GraphIso.Nauty.SearchState.admit_storage {n : Nat} {κ : Type} (st : SearchState n κ) : (admit st).canong = st.canong

theorem Hex.GraphIso.Nauty.SearchState.prune_storage {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : (pruneReturn level st).snd.canong = st.canong

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

Every classification exit preserves storage while updating the selected label, row-prefix counter, automorphism trace and return controls.