theorem Hex.GraphIso.Nauty.Sparse.DescPath.nil_of_discrete {n : Nat} {G : SparseGraph n} {base last : Nat} {root leaf : RefineSt n} {path : List (Nat × Nat)} (h : DescPath G base root path last leaf) (hr : RefineSt.Ready G base root) (hd : discreteAt root.ptn base n = true) : path = []

A valid discrete native node has no further individualization step.

theorem Hex.GraphIso.Nauty.Sparse.DescPath.leaf_depth {n : Nat} (G : SparseGraph n) (tcs : List Nat) {level last current : Nat} {root U V : RefineSt n} {xs ys : List (Nat × Nat)} : RefineSt.Ready G level root → NodeShape n level root.ptn → DescPath G level root xs last U → discreteAt U.ptn last n = true → DescPath G level root ys current V → List.map Prod.fst ys = tcs → tcs <+: List.map Prod.fst xs → discreteAt V.ptn current n = true → current = last

Below a cheap-shaped equitable node, a discrete descent following a prefix of another discrete descent's targets reaches its full depth. Each branch keeps its own executed cached refinement calls.

theorem Hex.GraphIso.Nauty.Sparse.DescPath.leaf_prefix {n : Nat} {G : SparseGraph n} {level last current : Nat} {root U V : RefineSt n} {xs ys : List (Nat × Nat)} {u v : Label n} (hr : RefineSt.Ready G level root) (hshape : NodeShape n level root.ptn) (hU : DescPath G level root xs last U) (hdU : discreteAt U.ptn last n = true) (hu : Label.ofArray? n U.lab = some u) (hV : DescPath G level root ys current V) (hp : List.map Prod.fst ys <+: List.map Prod.fst xs) (hdV : discreteAt V.ptn current n = true) (hv : Label.ofArray? n V.lab = some v) : current = last ∧ G.relabel v.perm = G.relabel u.perm

Matching a saved target prefix at a discrete leaf gives both the saved depth and the saved normalized sparse graph.