def Hex.GraphIso.Nauty.Sparse.GuidedPerm {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (store : Array Int) (base : Nat) (root : RefineSt n) (level : Nat) (current : RefineSt n) : Prop

A native guided history with all its refinement codes, allowing the current endpoint's labels to be reordered within the same cells.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.GuidedPerm.refl {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (store : Array Int) (level : Nat) (st : RefineSt n) : GuidedPerm G tcLevel store level st level st

theorem Hex.GraphIso.Nauty.Sparse.GuidedPerm.setLab {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {store : Array Int} {base level : Nat} {root current : RefineSt n} (h : GuidedPerm G tcLevel store base root level current) (lab : Array Nat) (he : cellsPerm current.ptn level lab current.lab) : GuidedPerm G tcLevel store base root level { lab := lab, ptn := current.ptn, active := current.active, queue := current.queue, cellstart := current.cellstart, cellend := current.cellend, indexed := current.indexed, hits := current.hits, marks := current.marks, vmarks := current.vmarks, stamp := current.stamp, numcells := current.numcells, longcode := current.longcode }

Recovered label order retains the same complete guided path.

theorem Hex.GraphIso.Nauty.Sparse.GuidedPerm.leaf {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {store : Array Int} {base level : Nat} {root current : RefineSt n} (h : GuidedPerm G tcLevel store base root level current) (hr : RefineSt.Ready G base root) (hc : RefineSt.Ready G level current) (hd : discreteAt current.ptn level n = true) : ∃ (leaf : RefineSt n), ∃ (path : List (Nat × Nat)), ∃ (codes : List Nat), ∃ (trace : CodePath G base root path level leaf codes), CodePath.Guided tcLevel store trace ∧ leaf.lab = current.lab ∧ leaf.ptn = current.ptn

At a discrete endpoint, the guided history has the literal current label array, so its scatter and native key can be used directly.

theorem Hex.GraphIso.Nauty.Sparse.GuidedPerm.child {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {store : Array Int} {base level : Nat} {root current : RefineSt n} (h : GuidedPerm G tcLevel store base root level current) (hr : RefineSt.Ready G base root) (hc : RefineSt.Ready G level current) {tc len o : Nat} (hcell : IsCell current.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (hchoice : tc = targetcell (Graph.ofGraph G) current.lab current.ptn level tcLevel (-1) ∨ store[level]! = Int.ofNat tc) (scratch : Scratch) (hs : Scratch.Bounded n scratch) : GuidedPerm G tcLevel store base root (level + 1) (RefineSt.child (Graph.ofGraph G) level current tc current.lab[tc + o]! scratch)

A canonical or saved target extends the history through actual individualization and cached refinement, including after sibling recovery.

theorem Hex.GraphIso.Nauty.Sparse.FirstRef.guided_follows {n : Nat} {G : SparseGraph n} {tcLevel base level : Nat} {root current : RefineSt n} {st : State n} {f l : Label n} (h : FirstRef G tcLevel base root st) (hr : RefineSt.Ready G base root) (hc : RefineSt.Ready G level current) (hg : GuidedPerm G tcLevel st.firsttc base root level current) (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) : level = h.last ∧ st.firstcode[level + 1]! = codeSentinel ∧ G.relabel l.perm = G.relabel f.perm

A recovered guided history and a checked native automorphism supply the saved first sentinel and graph without a cheap-shape assumption.