theorem Hex.GraphIso.Nauty.Sparse.DescPath.leaf_graph {n : Nat} (G : SparseGraph n) (tcs : List Nat) {level last : Nat} {root U V : RefineSt n} {xs ys : List (Nat × Nat)} {u v : Label n} : RefineSt.Ready G level root → NodeShape n level root.ptn → DescPath G level root xs last U → List.map Prod.fst xs = tcs → discreteAt U.ptn last n = true → Label.ofArray? n U.lab = some u → DescPath G level root ys last V → List.map Prod.fst ys = tcs → discreteAt V.ptn last n = true → Label.ofArray? n V.lab = some v → G.relabel u.perm = G.relabel v.perm

Two discrete native descents below a cheap-shaped equitable node, following the same target positions, have identical normalized leaf graphs. Each descent retains its own actual cached refinement calls.