structure Hex.GraphIso.Nauty.Sparse.RouteAligned {n : Nat} (G : SparseGraph n) (tcLevel base : Nat) (root : RefineSt n) (level agreed numcells : Nat) (st : State n) : Prop

Agreement with the saved first codes retains the complete guided native history for the current partition. Before comparison, agreed is the preceding level.

• bound : st.eqlevFirst ≤ agreed
• descent : st.eqlevFirst = agreed → RouteAt G tcLevel st.firsttc base root level numcells st

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.mono {n : Nat} {G : SparseGraph n} {tcLevel base level agreed numcells : Nat} {root : RefineSt n} {st out : State n} (h : RouteAligned G tcLevel base root level agreed numcells st) (he : out.eqlevFirst ≤ st.eqlevFirst) (ht : out.firsttc = st.firsttc) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) : RouteAligned G tcLevel base root level agreed numcells out

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.compare {n : Nat} {G : SparseGraph n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : RouteAligned G tcLevel base root level (level - 1) numcells st) (hl : 0 < level) (code : Nat) : RouteAligned G tcLevel base root level level numcells (compareCodes level code st)

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.target {n : Nat} {G : SparseGraph n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : RouteAligned G tcLevel base root level level numcells st) : RouteAligned G tcLevel base root level level numcells (chooseTarget false (Graph.ofGraph G) tcLevel level numcells st).snd.snd.snd

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.classify {n : Nat} {G : SparseGraph n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : RouteAligned G tcLevel base root level level numcells st) : RouteAligned G tcLevel base root level level numcells (Sparse.classify (Graph.ofGraph G) level numcells st).snd

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.leaf {n : Nat} {G : SparseGraph n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : RouteAligned G tcLevel base root level level numcells st) (leaf : Leaf) : RouteAligned G tcLevel base root level level numcells (leafExit leaf level st).snd

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.cheap {n : Nat} {G : SparseGraph n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : RouteAligned G tcLevel base root level level numcells st) (first : Bool) : RouteAligned G tcLevel base root level level numcells (cheapCheck first level st)

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : RouteAligned G.graph tcLevel base root level level numcells st) (first : Bool) (hr : RefineSt.Ready G.graph base root) (hok : Ready G level numcells st) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hrecord : st.eqlevFirst = level → tc = targetcell (Graph.ofGraph G.graph) st.lab st.ptn level tcLevel (-1) ∨ st.firsttc[level]! = Int.ofNat tc) : have next := Generic.Policy.child first level tc tv st; have r := visit (Graph.ofGraph G.graph) (level + 1) (numcells + 1) next; RouteAligned G.graph tcLevel base root (level + 1) level r.fst r.snd.snd

Individualization and the real cached visit extend the guided history from a canonical or saved target and the parent's equitable witness.

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.recover {n k : Nat} {G : Sparse.Colored n k} {tcLevel base level numcells : Nat} {root : RefineSt n} {st out : State n} (h : RouteAligned G.graph tcLevel base root level level numcells st) (hok : SearchOk G.toDense level numcells st.frame) (hout : FrameOut G level level st out) (ht : out.firsttc = st.firsttc) (hdiv : st.eqlevFirst < level → out.eqlevFirst < level) : RouteAligned G.graph tcLevel base root level level numcells (Generic.Policy.recover (n + 2) level out)

A return that cannot repair an earlier divergence preserves the ancestor's frozen descent through actual partition and cache recovery.

theorem Hex.GraphIso.Nauty.Sparse.RouteAligned.child_return {n k : Nat} {G : Sparse.Colored n k} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : RouteAligned G.graph tcLevel base root level level numcells st) (first : Bool) (fuel : Nat) (hl : 1 ≤ level) (hok : Ready G level numcells st) {tc tv : Nat} {cell : VSet n} (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) : have out := (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)).snd; RouteAligned G.graph tcLevel base root level level numcells (Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv out))

Every actual off-path child call has the frame and divergence effects needed to recover its parent's alignment, for arbitrary recursion fuel.