theorem Hex.GraphIso.Nauty.DescPath.selected {n : Nat} {ctx : Ctx n} {σ : Renaming n} (hg : RowsMap σ ctx.g ctx.g) (tcLevel : Nat) {level last : Nat} {path : List (Nat × Nat)} {U leaf V : RefineSt n} : DescPath ctx level U path last leaf → Selects ctx tcLevel level U path → IterOk ctx level U → StPerm level V (mapSt σ U) → ∃ (out : RefineSt n), ∃ (path' : List (Nat × Nat)), DescPath ctx level V path' last out ∧ Selects ctx tcLevel level V path' ∧ List.map Prod.fst path' = List.map Prod.fst path ∧ StPerm last out (mapSt σ leaf)

Renaming and reordering within cells transports a canonically selected descent, retaining both its target positions and the canonical choices.

theorem Hex.GraphIso.Nauty.Guided.depth_map {n : Nat} {ctx : Ctx n} {σ : Renaming n} {tcLevel base last₁ last₂ : Nat} {store : Array Int} {root first current : RefineSt n} {p₁ p₂ : List (Nat × Nat)} (hg : RowsMap σ ctx.g ctx.g) (hfirst : DescPath ctx base root p₁ last₁ first) (hok : IterOk ctx base root) (hselect : Selects ctx tcLevel base root p₁) (htarget : Targets store base (List.map Prod.fst p₁)) (hcurrent : DescPath ctx base root p₂ last₂ current) (hguided : Guided ctx tcLevel store base root p₂) (hstab : StPerm base root (mapSt σ root)) (hdisc₁ : ∀ (q : Nat), q < n → first.ptn[q]! ≤ last₁) (hdisc₂ : ∀ (q : Nat), q < n → current.ptn[q]! ≤ last₂) (hlab : Array.map σ.toFun first.lab = current.lab) : last₂ = last₁

A checked row-preserving renaming relating the final labellings identifies descent depths whenever it stabilizes the common ancestor.