theorem Hex.GraphIso.Nauty.Sparse.FirstRef.target {n : Nat} {G : SparseGraph n} {tcLevel base level : Nat} {root current : RefineSt n} {st : State n} (h : FirstRef G tcLevel base root st) (hdepth : level ≤ h.last) (hr : RefineSt.Ready G base root) (hc : RefineSt.Ready G level current) (hshape : NodeShape n base root.ptn) (hp : FollowsPerm G st.firsttc base root level current) (hopen : discreteAt current.ptn level n ≠ true) : Int.ofNat (targetcell (Graph.ofGraph G) current.lab current.ptn level tcLevel (-1)) = st.firsttc[level]!

A live stored-target descent below a cheap ancestor chooses the exact saved next target, even after sibling searches reorder the current cells.