theorem Hex.GraphIso.Nauty.Sparse.classify_frame {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : have out := (classify g level numcells st).snd; out.lab = st.lab ∧ out.ptn = st.ptn ∧ out.firstlab = st.firstlab ∧ out.canonlab = st.canonlab

Native classification preserves the partition and saved reference labels, including branches that install canonical rows or scatter an automorphism.

theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_frame {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : have out := (chooseTarget first g tcLevel level numcells st).snd.snd.snd; out.lab = st.lab ∧ out.ptn = st.ptn ∧ out.firstlab = st.firstlab ∧ out.canonlab = st.canonlab

Borrowing target scratch and recording target hints changes no partition or saved label field in the actual sparse dispatch.

theorem Hex.GraphIso.Nauty.Sparse.Ready.classify {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) : Local G level numcells st (Sparse.classify (Graph.ofGraph G.graph) level numcells st).snd

theorem Hex.GraphIso.Nauty.Sparse.Ready.target_frame {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (first : Bool) (tcLevel : Nat) : Local G level numcells st (chooseTarget first (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd