theorem
Hex.GraphIso.Nauty.scatter_of_descPaths
{n : Nat}
{ctx : Ctx n}
{st : Search n}
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
{ancestor : RefineSt n}
(hsmall : SubtreeOk ctx st.gcaFirst ancestor)
{p₁ p₂ : List (Nat × Nat)}
{level₁ level₂ : Nat}
{U V : RefineSt n}
(hU : DescPath ctx st.gcaFirst ancestor p₁ level₁ U)
(hV : DescPath ctx st.gcaFirst ancestor p₂ level₂ V)
(htargets : List.map Prod.fst p₂ <+: List.map Prod.fst p₁)
(hUd : ∀ (i : Nat), i < n → U.ptn[i]! ≤ level₁)
(hVd : ∀ (i : Nat), i < n → V.ptn[i]! ≤ level₂)
(hfirst : st.firstlab = U.lab)
(hcurrent : st.lab = V.lab)
(hwork : st.workperm.size = n)
:
Compatible descents below a cheap ancestor validate the search's first-reference scatter without an automorphism scan.