def
Hex.GraphIso.Nauty.Sparse.CodePath.Guided
{n : Nat}
{G : SparseGraph n}
(tcLevel : Nat)
(store : Array Int)
{base last : Nat}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
{codes : List Nat}
:
A live first-reference path uses either the native canonical target or the saved target. Every step still records its actual cached call.
Equations
- One or more equations did not get rendered due to their size.
- Hex.GraphIso.Nauty.Sparse.CodePath.Guided tcLevel store (Hex.GraphIso.Nauty.Sparse.CodePath.refl x✝¹ x✝) = True
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.CodePath.Guided.extend
{n : Nat}
{G : SparseGraph n}
{tcLevel base level : Nat}
{store : Array Int}
{root leaf : RefineSt n}
{path : List (Nat × Nat)}
{codes : List Nat}
{h : CodePath G base root path level leaf codes}
(hg : Guided tcLevel store h)
{tc len o : Nat}
(hc : IsCell leaf.ptn level tc len)
(hb : tc + len ≤ n)
(hn : 1 < len)
(ho : o < len)
(scratch : Scratch)
(hs : Scratch.Bounded n scratch)
(hchoice : tc = targetcell (Graph.ofGraph G) leaf.lab leaf.ptn level tcLevel (-1) ∨ store[level]! = Int.ofNat tc)
:
Append one actual cached individualization to a guided history, retaining all earlier codes and recording the new refinement code.
theorem
Hex.GraphIso.Nauty.Sparse.CodePath.guided_codes
{n : Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j)
{tcLevel base last₁ last₂ : Nat}
{root other first current : RefineSt n}
{path₁ path₂ : List (Nat × Nat)}
{codes₁ codes₂ : List Nat}
{store : Array Int}
(hfirst : CodePath G base root path₁ last₁ first codes₁)
(hr : RefineSt.Ready G base root)
(ht : RefineSt.Ready H base other)
(he : RefineSt.Equiv (renamingOf p) base root other)
(hselect : Selects tcLevel hfirst)
(htarget : Targets store base (List.map Prod.fst path₁))
(hcurrent : CodePath H base other path₂ last₂ current codes₂)
(hguided : Guided tcLevel store hcurrent)
(hd₁ : discreteAt first.ptn last₁ n = true)
(hd₂ : discreteAt current.ptn last₂ n = true)
(hlabels : Array.map (renamingOf p).toFun first.lab = current.lab)
:
Matching final labels force equal depths and complete code sequences for a selected reference and a guided path, even with independent caches and label order within corresponding cells. Individualized vertices persist at literal positions.