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

A frozen equitable witness connects an entire guided code history to the production labels, partition and count. Its active set is retained with the witness; actual child calls install their own splitter.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.RouteAt.congr {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {store : Array Int} {base level numcells : Nat} {root : RefineSt n} {st out : State n} (h : RouteAt G tcLevel store base root level numcells st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) : RouteAt G tcLevel store base root level numcells out

theorem Hex.GraphIso.Nauty.Sparse.RouteAt.reorder {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {store : Array Int} {base level numcells : Nat} {root : RefineSt n} {st out : State n} (h : RouteAt G tcLevel store base root level numcells st) (hl : out.lab.size = st.lab.size) (hp : out.ptn = st.ptn) (hc : cellsPerm st.ptn level out.lab st.lab) : RouteAt G tcLevel store base root level numcells out

Adopting returned label order preserves both the guided history and the equitable certificate of the restored parent.

theorem Hex.GraphIso.Nauty.Sparse.RouteAt.child {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {store : Array Int} {base level numcells : Nat} {root : RefineSt n} {st : State n} (h : RouteAt G tcLevel store base root level numcells st) (hr : RefineSt.Ready G base root) (first : Bool) {tc len o : Nat} (hc : IsCell st.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (hchoice : tc = targetcell (Graph.ofGraph G) st.lab st.ptn level tcLevel (-1) ∨ store[level]! = Int.ofNat tc) (hs : Scratch.Bounded n st.canong.scratch) : have next := Generic.Policy.child first level tc st.lab[tc + o]! st; have r := visit (Graph.ofGraph G) (level + 1) (numcells + 1) next; RouteAt G tcLevel store base root (level + 1) r.fst r.snd.snd

Actual native individualization and the cached child visit extend the guided code history using either an unhinted or stored target.

theorem Hex.GraphIso.Nauty.Sparse.RouteAt.first_leaf {n : Nat} {G : SparseGraph n} {tcLevel base level : Nat} {root : RefineSt n} {st : State n} (h : RouteAt G tcLevel st.firsttc base root level n st) (href : FirstRef G tcLevel base root st) (hr : RefineSt.Ready G base root) {f l : Label n} (hf : Label.ofArray? n st.firstlab = some f) (hl : Label.ofArray? n st.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 = st.lab) : st.firstcode[level + 1]! = codeSentinel ∧ G.relabel l.perm = G.relabel f.perm

The actual guided endpoint and a native automorphism identify the saved first sentinel and graph at a discrete production node.

theorem Hex.GraphIso.Nauty.Sparse.RouteAt.recover {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {store : Array Int} {base level numcells : Nat} {root : RefineSt n} {st out : State n} (h : RouteAt G.graph tcLevel store base root level numcells st) (hok : SearchOk G.toDense level numcells st.frame) (hout : FrameOut G level level st out) : RouteAt G.graph tcLevel store base root level numcells (Generic.Policy.recover (n + 2) level out)

Native partition recovery restores the guided history using the independently proved effect of the actual child search.