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

At a cheap first-path ancestor, retain its saved first descent and the current descent selected by the live agreement counter.

Equations

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

theorem Hex.GraphIso.Nauty.CheapHistory.transport {n : Nat} {ctx : Ctx n} {tcLevel level agreed numcells level' agreed' numcells' : Nat} {st out : Search n} (h : CheapHistory ctx tcLevel level agreed numcells st) (hr : SearchState.reference out = SearchState.reference st) (hg : out.gcaFirst = st.gcaFirst) (hn : out.noncheaplevel ≤ st.gcaFirst → st.noncheaplevel ≤ st.gcaFirst) (hd : ∀ (last : Nat), Depth last st → Depth last out) (ha : ∀ (root : RefineSt n), Aligned ctx st.gcaFirst root level agreed numcells st → Aligned ctx st.gcaFirst root level' agreed' numcells' out) : CheapHistory ctx tcLevel level' agreed' numcells' out

Transport a frozen first ancestor through a local operation.

theorem Hex.GraphIso.Nauty.CheapHistory.compare {n : Nat} {ctx : Ctx n} {tcLevel level numcells code : Nat} {st : Search n} (h : CheapHistory ctx tcLevel level (level - 1) numcells st) (hlevel : 0 < level) (hcode : code < codeSentinel) : CheapHistory 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.CheapHistory.target {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : CheapHistory ctx tcLevel level level numcells st) : CheapHistory 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.CheapHistory.classify {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : CheapHistory ctx tcLevel level level numcells st) : CheapHistory ctx tcLevel level level numcells (Nauty.classify ctx level numcells st).snd

Classification preserves the live first-path history.

theorem Hex.GraphIso.Nauty.CheapHistory.leaf {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : CheapHistory ctx tcLevel level level numcells st) (leaf : Leaf) : CheapHistory 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.CheapHistory.cheap {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : CheapHistory ctx tcLevel level level numcells st) (first : Bool) (hg : st.gcaFirst ≤ level) : CheapHistory ctx tcLevel level level numcells (cheapCheck first level st)

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

def Hex.GraphIso.Nauty.CheapRecorded {n : Nat} (level tc : Nat) (st : Search n) : Prop

The sweep target is recorded whenever cheap first-path agreement is retained.

Equations

• Hex.GraphIso.Nauty.CheapRecorded level tc st = (st.noncheaplevel ≤ st.gcaFirst → st.eqlevFirst = level → st.firsttc[level]! = Int.ofNat tc)

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

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

theorem Hex.GraphIso.Nauty.CheapHistory.recorded {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : CheapHistory 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; CheapRecorded level r.fst.toNat r.snd.snd.snd

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

theorem Hex.GraphIso.Nauty.CheapHistory.child {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells tc tv : Nat} {st : Search n} {cell : VSet n} (h : CheapHistory 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 : CheapRecorded level tc st) : have next := Nauty.child first level tc tv st; have r := visit ctx (level + 1) (numcells + 1) next; CheapHistory 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.CheapHistory.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 : CheapHistory 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 }; CheapHistory ctx tcLevel level level numcells result ∧ (CheapRecorded level tc st → CheapRecorded level tc result)

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

theorem Hex.GraphIso.Nauty.CheapHistory.first_checked {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st out : Search n} (h : CheapHistory 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.CheapHistory.checked {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : Search n} (h : CheapHistory 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.