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

The live first-path history retains a general guided descent and the stronger small-cell descent whenever its common ancestor is cheap.

• cheapHistory : CheapHistory ctx tcLevel level agreed numcells st
• route : RouteHistory ctx tcLevel level agreed numcells st

structure Hex.GraphIso.Nauty.Recorded {n : Nat} (ctx : Ctx n) (tcLevel level tc : Nat) (st : Search n) : Prop

The chosen sweep target follows either the canonical selector or the saved first path, and agrees with the saved path at cheap ancestors.

• cheapRecorded : CheapRecorded level tc st
• choice : Choice ctx tcLevel level tc st

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

Code comparison retains the frozen ancestor and activates the pending node history.

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

A retained target comparison preserves its history and saved sentinel bound.

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

Classification preserves the live first-path history.

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

Leaf actions preserve the live first-path history until the receiving frame recovers it.

theorem Hex.GraphIso.Nauty.History.cheap {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : History ctx tcLevel level level numcells st) (first : Bool) (hg : st.gcaFirst ≤ level) : History ctx tcLevel level level numcells (cheapCheck first level st)

A failed guard below the first ancestor cannot make that ancestor cheap.

theorem Hex.GraphIso.Nauty.Recorded.cheap {n : Nat} {ctx : Ctx n} {tcLevel level tc : Nat} {st : Search n} (h : Recorded ctx tcLevel level tc st) (first : Bool) (hg : st.gcaFirst ≤ level) : Recorded ctx tcLevel level tc (cheapCheck first level st)

A cheap-boundary update retains the recorded target when its ancestor remains cheap.

theorem Hex.GraphIso.Nauty.History.recorded {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : History ctx tcLevel level level numcells st) (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) : have r := chooseTarget false ctx tcLevel level numcells st; Recorded ctx tcLevel level r.fst.toNat r.snd.snd.snd

A target selected at a cheap ancestor is the stored target position.

theorem Hex.GraphIso.Nauty.History.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells tc tv : Nat} {st : Search n} {cell : VSet n} (h : History ctx tcLevel level level numcells st) (first : Bool) (hsize : ctx.g.size = n) (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 : Recorded ctx tcLevel level tc st) : have next := Nauty.child first level tc tv st; have r := visit ctx (level + 1) (numcells + 1) next; History ctx tcLevel (level + 1) level r.fst r.snd.snd

A sweep's stored target prepares the next actual child history.

theorem Hex.GraphIso.Nauty.History.child_return {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv : Nat} {st : Search n} {cell : VSet n} (h : History ctx tcLevel level level numcells st) (first : Bool) (hg : st.gcaFirst ≤ level) (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; have result := 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 }; History ctx tcLevel level level numcells result ∧ (Recorded ctx tcLevel level tc st → Recorded ctx tcLevel level tc result)

Recovering an actual child preserves the history at its receiving ancestor.

theorem Hex.GraphIso.Nauty.History.first_checked {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st out : Search n} (h : History ctx tcLevel level level numcells st) (hinv : RunInv G ctx st) (hn0 : 0 < n) (hok : SearchOk G level numcells st) (hauto : Nauty.classify ctx level numcells st = (Generic.Leaf.autoFirst, out)) (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) : checkAutom ctx.g out.workperm = true

The live history supplies the restored first-leaf admission test at every prepared node.

theorem Hex.GraphIso.Nauty.History.checked {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : History ctx tcLevel level level numcells st) (hinv : RunInv G ctx st) (hn0 : 0 < n) (hok : SearchOk G level numcells st) (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) : have r := Nauty.classify ctx level numcells st; r.fst = Generic.Leaf.autoFirst ∨ r.fst = Generic.Leaf.autoCanon → checkAutom ctx.g r.snd.workperm = true

Both automorphism classifications produce a checked scratch permutation.