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

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

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

theorem Hex.GraphIso.Nauty.Aligned.mono {n : Nat} {ctx : Ctx n} {base level agreed numcells : Nat} {root : RefineSt n} {st out : Search n} (h : Aligned ctx 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) : Aligned ctx base root level agreed numcells out

Bookkeeping that can only lower agreement retains an aligned descent.

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

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

theorem Hex.GraphIso.Nauty.Aligned.target {n : Nat} {ctx : Ctx n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : Aligned ctx base root level level numcells st) : Aligned ctx 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.Aligned.classify {n : Nat} {ctx : Ctx n} {base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : Aligned ctx base root level level numcells st) : Aligned ctx 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.Aligned.leaf {n : Nat} {ctx : Ctx n} {base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : Aligned ctx base root level level numcells st) (leaf : Leaf) : Aligned ctx 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.Aligned.cheap {n : Nat} {ctx : Ctx n} {base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : Aligned ctx base root level level numcells st) (first : Bool) : Aligned ctx base root level level numcells (cheapCheck first level st)

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

theorem Hex.GraphIso.Nauty.Aligned.target_eq {n : Nat} {ctx : Ctx n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : Search n} (h : Aligned ctx base root level level numcells st) (href : FirstRef ctx tcLevel base root st) (hdepth : Depth href.last st) (hkeep : (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd.eqlevFirst = level) (hnc : numcells < n) (hlevel : 0 < level) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hsmall : SubtreeOk ctx base root) : (chooseTarget false ctx tcLevel level numcells st).fst = st.firsttc[level]!

A surviving target choice agrees with the recorded first-path target.

theorem Hex.GraphIso.Nauty.Aligned.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {base level numcells tc tv : Nat} {root : RefineSt n} {st : Search n} {cell : VSet n} (h : Aligned ctx 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 → st.firsttc[level]! = Int.ofNat tc) : have next := Nauty.child first level tc tv st; have r := visit ctx (level + 1) (numcells + 1) next; Aligned ctx 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.recover_eqlev {n : Nat} (inf level : Nat) (st : Search n) : (recover inf level st).eqlevFirst = min st.eqlevFirst level

Recovery bounds first-code agreement by the receiving frame.

theorem Hex.GraphIso.Nauty.Aligned.recover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {base level numcells : Nat} {root : RefineSt n} {st out : Search n} (h : Aligned ctx 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) : Aligned ctx base root level level numcells (Nauty.recover (n + 2) level out)

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

theorem Hex.GraphIso.Nauty.Aligned.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 : Aligned ctx 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; Aligned ctx 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.