structure Hex.GraphIso.Nauty.GuidedState {n : Nat} (ctx : Ctx n) (tcLevel base : Nat) (root : RefineSt n) (level agreed numcells : Nat) (st : Search n) : Prop

Agreement with the first path carries the current partition's guided descent. Before comparing a node, agreed is level - 1.

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

theorem Hex.GraphIso.Nauty.GuidedState.mono {n : Nat} {ctx : Ctx n} {tcLevel base level agreed numcells : Nat} {root : RefineSt n} {st out : Search n} (h : GuidedState ctx tcLevel base root level agreed numcells st) (heq : out.eqlevFirst ≤ st.eqlevFirst) (htc : out.firsttc = st.firsttc) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) : GuidedState ctx tcLevel base root level agreed numcells out

Bookkeeping that can only lower agreement retains an aligned descent.

theorem Hex.GraphIso.Nauty.GuidedState.compare {n : Nat} {ctx : Ctx n} {tcLevel base level numcells code : Nat} {root : RefineSt n} {st : Search n} (h : GuidedState ctx tcLevel base root level (level - 1) numcells st) (hlevel : 0 < level) : GuidedState ctx tcLevel base root level level numcells (compareCodes level code st)

Comparing a code activates exactly the pending history of its node.

theorem Hex.GraphIso.Nauty.GuidedState.target {n : Nat} {ctx : Ctx n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : GuidedState ctx tcLevel base root level level numcells st) : GuidedState ctx tcLevel base root level level numcells (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd

A target mismatch discards alignment; every retained comparison keeps it.

theorem Hex.GraphIso.Nauty.GuidedState.classify {n : Nat} {ctx : Ctx n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : GuidedState ctx tcLevel base root level level numcells st) : GuidedState ctx tcLevel base root level level numcells (Nauty.classify ctx level numcells st).snd

Classification does not change the aligned partition or its comparison.

theorem Hex.GraphIso.Nauty.GuidedState.leaf {n : Nat} {ctx : Ctx n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : GuidedState ctx tcLevel base root level level numcells st) (leaf : Leaf) : GuidedState ctx tcLevel base root level level numcells (leafExit leaf level st).snd

Leaf actions retain the current descent, including when returning to an ancestor.

theorem Hex.GraphIso.Nauty.GuidedState.cheap {n : Nat} {ctx : Ctx n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : GuidedState ctx tcLevel base root level level numcells st) (first : Bool) : GuidedState ctx tcLevel base root level level numcells (cheapCheck first level st)

Testing whether a partition is cheap changes only the cheap boundary.

theorem Hex.GraphIso.Nauty.GuidedState.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel base level numcells tc tv : Nat} {root : RefineSt n} {st : Search n} {cell : VSet n} (h : GuidedState ctx tcLevel base root level level numcells st) (first : Bool) (hsize : ctx.g.size = n) (hroot : IterOk ctx base root) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) (hrecord : st.eqlevFirst = level → specTargetcell ctx st.lab st.ptn level tcLevel = tc ∨ st.firsttc[level]! = Int.ofNat tc) : have next := Nauty.child first level tc tv st; have r := visit ctx (level + 1) (numcells + 1) next; GuidedState ctx tcLevel base root (level + 1) level r.fst r.snd.snd

Individualization prepares the next pending history, for either parent-sweep flag.

theorem Hex.GraphIso.Nauty.GuidedState.recover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st out : Search n} (h : GuidedState ctx tcLevel base root level level numcells st) (hok : SearchOk G level numcells st) (hout : SearchOut G level level st out) (htc : out.firsttc = st.firsttc) (hdiv : st.eqlevFirst < level → out.eqlevFirst < level) : GuidedState ctx tcLevel base root level level numcells (Nauty.recover (n + 2) level out)

A child that cannot restore an earlier divergence retains the parent guided history on recovery.

theorem Hex.GraphIso.Nauty.GuidedState.child_return {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel base level numcells tc tv : Nat} {root : RefineSt n} {st : Search n} {cell : VSet n} (h : GuidedState ctx tcLevel base root level level numcells st) (first : Bool) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) : have out := (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd; GuidedState ctx tcLevel base root level level numcells (Nauty.recover (n + 2) level { lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts.erase tv, autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode, firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong, samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon, gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := out.stabvertex, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel, order := out.order, genTrace := out.genTrace, workperm := out.workperm })

An actual off-path child return has precisely the divergence and frame properties required to recover its parent's aligned history.