theorem
Hex.GraphIso.Nauty.Sparse.DescPath.map_cells
{n : Nat}
{G : SparseGraph n}
{base last₁ last₂ : Nat}
{root first current : RefineSt n}
{path₁ path₂ : List (Nat × Nat)}
(hfirst : DescPath G base root path₁ last₁ first)
(hcurrent : DescPath G base root path₂ last₂ current)
(hr : RefineSt.Ready G base root)
(p : Perm n)
(hlabels : Array.map (renamingOf p).toFun first.lab = current.lab)
:
A renaming relating two descendant labels stabilizes their common ancestor's ordered cells. This uses the frame of the executed native calls.
theorem
Hex.GraphIso.Nauty.Sparse.CodePath.guided_leaf
{n : Nat}
{G : SparseGraph n}
{tcLevel base last₁ last₂ : Nat}
{root first current : RefineSt n}
{path₁ path₂ : List (Nat × Nat)}
{codes₁ codes₂ : List Nat}
{store : Array Int}
{f l : Label n}
(hfirst : CodePath G base root path₁ last₁ first codes₁)
(hr : RefineSt.Ready G base root)
(hselect : Selects tcLevel hfirst)
(htarget : Targets store base (List.map Prod.fst path₁))
(hcurrent : CodePath G base root path₂ last₂ current codes₂)
(hguided : Guided tcLevel store hcurrent)
(hd₁ : discreteAt first.ptn last₁ n = true)
(hd₂ : discreteAt current.ptn last₂ n = true)
(hf : Label.ofArray? n first.lab = some f)
(hl : Label.ofArray? n current.lab = some l)
(p : Perm n)
(hiso : ∀ (i j : Fin n), G.adj (p.get i) (p.get j) = G.adj i j)
(hlabels : Array.map (renamingOf p).toFun first.lab = current.lab)
:
An automorphism relating actual descendant labels identifies their depth and complete code sequence when one path is selected and the other uses native or saved targets. No small-cell shape is required.
theorem
Hex.GraphIso.Nauty.Sparse.FirstRef.leaf_guided
{n : Nat}
{G : SparseGraph n}
{tcLevel base level : Nat}
{root current : RefineSt n}
{st : State n}
{path : List (Nat × Nat)}
{codes : List Nat}
{f l : Label n}
(h : FirstRef G tcLevel base root st)
(hr : RefineSt.Ready G base root)
(hc : CodePath G base root path level current codes)
(hg : CodePath.Guided tcLevel st.firsttc hc)
(hd : discreteAt current.ptn level n = true)
(hf : Label.ofArray? n st.firstlab = some f)
(hl : Label.ofArray? n current.lab = some l)
(p : Perm n)
(hiso : ∀ (i j : Fin n), G.adj (p.get i) (p.get j) = G.adj i j)
(hlabels : Array.map (renamingOf p).toFun st.firstlab = current.lab)
:
The saved native first reference supplies the selected path, code slots and terminal sentinel needed by the general automorphism argument.