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

Native cached target dispatch retains the canonical ancestor.

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

Native row comparison and automorphism tests retain the canonical ancestor; installing a better label belongs to the subsequent leaf action.