theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.target_perm {n : Nat} {G : SparseGraph n} {level : Nat} {s t : RefineSt n} (hs : Ready G level s) (ht : Ready G level t) (hp : s.ptn = t.ptn) (he : cellsPerm t.ptn level s.lab t.lab) (tcLevel : Nat) (hint : Int) : targetcell (Graph.ofGraph G) s.lab s.ptn level tcLevel hint = targetcell (Graph.ofGraph G) t.lab t.ptn level tcLevel hint

Native target selection depends on an equitable partition's ordered cells, independently of the label order and the witness's saved active set.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.target {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j) {level : Nat} {s t : RefineSt n} (hs : Ready G level s) (ht : Ready H level t) (he : Equiv (renamingOf p) level s t) (tcLevel : Nat) (hint : Int) : targetcell (Graph.ofGraph H) t.lab t.ptn level tcLevel hint = targetcell (Graph.ofGraph G) s.lab s.ptn level tcLevel hint

Equivalent native equitable nodes choose the same target position. The rule includes the hint and depth cutoff and needs no cache identity.