theorem Hex.GraphIso.Nauty.Sparse.CodePath.map {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) {tcLevel base last : Nat} {root leaf other : RefineSt n} {path : List (Nat × Nat)} {codes : List Nat} (hpath : CodePath G base root path last leaf codes) (hr : RefineSt.Ready G base root) (ht : RefineSt.Ready H base other) (he : RefineSt.Equiv (renamingOf p) base root other) (hsel : Selects tcLevel hpath) : ∃ (out : RefineSt n), ∃ (path' : List (Nat × Nat)), ∃ (trace : CodePath H base other path' last out codes), Selects tcLevel trace ∧ List.map Prod.fst path' = List.map Prod.fst path ∧ RefineSt.Equiv (renamingOf p) last leaf out

Transport a selected native descent under isomorphism, retaining its entire refinement-code sequence and unhinted target rule. Corresponding vertices may occupy different offsets and caches remain independent.