theorem Hex.GraphIso.Nauty.child_canon {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv : Nat} {first : Bool} {cell : VSet n} {st : Search n} (h : SearchOk G level numcells st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (ht : cell.mem tv = true) (childFirst : Bool) : have out := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd; out.gcaCanon ≤ st.gcaCanon ∧ out.canonlab = st.canonlab ∨ out.canonlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab out.canonlab ∧ out.canonlab[tc]! = tv

The actual child either retains the old reference and does not raise its ancestor, or installs a reference through the chosen vertex.

theorem Hex.GraphIso.Nauty.child_canon_old {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv : Nat} {first : Bool} {cell : VSet n} {st : Search n} (h : SearchOk G level numcells st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (ht : cell.mem tv = true) (childFirst : Bool) : have out := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd; out.gcaCanon ≤ level → out.gcaCanon = st.gcaCanon ∧ out.canonlab = st.canonlab

A canonical reference pointing above the child is precisely the reference held by the receiving parent before the child was entered.

theorem Hex.GraphIso.Nauty.SweepPre.canon_return {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 tv : Nat} {first : Bool} {cell : VSet n} {st : Search n} (h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st) (hn0 : 0 < n) (childFirst : Bool) : have out := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd; out.gcaCanon ≤ st.gcaCanon ∧ out.canonlab = st.canonlab ∨ out.canonlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab out.canonlab ∧ out.canonlab[tc]! = tv

Later siblings use the partition-only canonical-return theorem.

theorem Hex.GraphIso.Nauty.SweepPre.canon_old {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 tv : Nat} {first : Bool} {cell : VSet n} {st : Search n} (h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st) (hn0 : 0 < n) (childFirst : Bool) : have out := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd; out.gcaCanon ≤ level → out.gcaCanon = st.gcaCanon ∧ out.canonlab = st.canonlab

Later siblings retain precisely the reference above their child.

def Hex.GraphIso.Nauty.CanonGuide {n : Nat} (level tc : Nat) (base : Search n) (key : Nat → Key n) (best : Option (Key n)) (st : Search n) : Prop

At a frozen sweep frame, a canonical ancestor pointing to this level names a child already bounded by the incumbent.

Equations

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

theorem Hex.GraphIso.Nauty.CanonGuide.vacuous {n level tc : Nat} {base st : Search n} {key : Nat → Key n} {best : Option (Key n)} (h : st.gcaCanon < level) : CanonGuide level tc base key best st

Before any child has installed a reference at this level, the guide has no coverage obligation.

theorem Hex.GraphIso.Nauty.CanonGuide.rebase {n k : Nat} {G : Colored n k} {level tc : Nat} {base st : Search n} {key : Nat → Key n} {best : Option (Key n)} (h : CanonGuide level tc base key best st) (hf : SearchOut G level level base st) : CanonGuide level tc st key best st

A reference expressed in a frozen frame also belongs to the current frame's cells after labels have been permuted within those cells.

theorem Hex.GraphIso.Nauty.CanonGuide.mem {n level tc len : Nat} {base st : Search n} {key : Nat → Key n} {best : Option (Key n)} (h : CanonGuide level tc base key best st) (hok : LabOk base.lab n) (hc : IsCell base.ptn level tc len) (hr : tc + len ≤ base.lab.size) (he : st.gcaCanon = level) : ∃ (v : Nat), Generic.Covers (key v) best ∧ st.canonlab[tc]! = v ∧ (windowSet n base.lab tc len).mem v = true

The guide's reference vertex belongs to the original target window, even if a filter has removed it from the mutable target set.

theorem Hex.GraphIso.Nauty.SweepPre.canon_locate {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 tv : Nat} {first : Bool} {cell : VSet n} {base st : Search n} {key : Nat → Key n} {best : Option (Key n)} (h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st) (hn0 : 0 < n) (childFirst : Bool) (hguide : CanonGuide level tc base key best st) : have out := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd; out.gcaCanon = level → ∃ (v : Nat), Generic.Covers (key v) best ∧ out.canonlab[tc]! = v ∧ cellsPerm base.ptn level base.lab out.canonlab

A canonical return to this loop names its previously covered reference child, even before the returned partition is recovered.

theorem Hex.GraphIso.Nauty.CanonGuide.recover {n k : Nat} {G : Colored n k} {level tc tv : Nat} {base st out : Search n} {key : Nat → Key n} {before after : Option (Key n)} (h : CanonGuide level tc base key before st) (hbound : st.gcaCanon ≤ level) (hgrows : Generic.Grows before after) (hdone : Generic.Covers (key tv) after) (hframe : SearchOut G level level base st) (hreturn : out.gcaCanon ≤ st.gcaCanon ∧ out.canonlab = st.canonlab ∨ out.canonlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab out.canonlab ∧ out.canonlab[tc]! = tv) (inf : Nat) : CanonGuide level tc base key after (Nauty.recover inf level out)

The receiving loop uses either its old covered reference or the child whose result was just absorbed, then clamps the reference's ancestor.

theorem Hex.GraphIso.Nauty.child_canon_guide {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 tv : Nat} {first : Bool} {cell : VSet n} {base st : Search n} {key : Nat → Key n} {before after : Option (Key n)} (h : SearchOk G level numcells st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (ht : cell.mem tv = true) (hbound : st.gcaCanon ≤ level) (hguide : CanonGuide level tc base key before st) (hframe : SearchOut G level level base st) (hgrows : Generic.Grows before after) (hdone : Generic.Covers (key tv) after) : have childFirst := first && tv == tv1; have raw := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd; have left := if childFirst = true then afterChildFirst level tv1 raw else raw; have out := { lab := left.lab, ptn := left.ptn, active := left.active, orbits := left.orbits, fixedpts := left.fixedpts.erase tv, autos := left.autos, wsCap := left.wsCap, firstcode := left.firstcode, canoncode := left.canoncode, firsttc := left.firsttc, firstlab := left.firstlab, canonlab := left.canonlab, canong := left.canong, samerows := left.samerows, compCanon := left.compCanon, eqlevFirst := left.eqlevFirst, eqlevCanon := left.eqlevCanon, gcaFirst := left.gcaFirst, gcaCanon := left.gcaCanon, canonlevel := left.canonlevel, noncheaplevel := left.noncheaplevel, allsamelevel := left.allsamelevel, cosetindex := left.cosetindex, stabvertex := left.stabvertex, numnodes := left.numnodes, tctotal := left.tctotal, canupdates := left.canupdates, numorbits := left.numorbits, numgenerators := left.numgenerators, numbadleaves := left.numbadleaves, maxlevel := left.maxlevel, order := left.order, genTrace := left.genTrace, workperm := left.workperm }; CanonGuide level tc base key after (recover (n + 2) level out)

A child's guide survives both first-child control updates and fixed-point cleanup. Only the reached partition is required, so this also applies before any first-path sibling has returned.