theorem
Hex.GraphIso.Nauty.Sparse.CodePath.target_prefix
{n : Nat}
{G : SparseGraph n}
{tcLevel base last level : Nat}
{root leaf current : RefineSt n}
{path xs : List (Nat × Nat)}
{codes : List Nat}
(h : CodePath G base root path last leaf codes)
(hr : RefineSt.Ready G base root)
(hshape : NodeShape n base root.ptn)
(hsel : Selects tcLevel h)
(hd : discreteAt leaf.ptn last n = true)
(hp : DescPath G base root xs level current)
(hprefix : List.map Prod.fst xs <+: List.map Prod.fst path)
(hopen : discreteAt current.ptn level n ≠ true)
:
An open native descent following a prefix of a selected cheap subtree chooses the next saved target. Sibling offsets and cache contents may differ.