theorem
Hex.GraphIso.Nauty.Max.NodeInput.codes
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
(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)
:
Every actual node returns settled incumbent codes on an extension of its incoming path, including the initial first descent.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.recovered_codes
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
(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)
(afterFirst : Bool)
(tv1 tv : Nat)
:
have out := (node first ctx (n + 2) tcLevel fuel f.level f.numcells f.entry).snd;
have middle := if afterFirst = true then afterChildFirst (f.level - 1) tv1 out else out;
have left :=
{ lab := middle.lab, ptn := middle.ptn, active := middle.active, orbits := middle.orbits,
fixedpts := middle.fixedpts.erase tv, autos := middle.autos, wsCap := middle.wsCap, firstcode := middle.firstcode,
canoncode := middle.canoncode, firsttc := middle.firsttc, firstlab := middle.firstlab, canonlab := middle.canonlab,
canong := middle.canong, samerows := middle.samerows, compCanon := middle.compCanon,
eqlevFirst := middle.eqlevFirst, eqlevCanon := middle.eqlevCanon, gcaFirst := middle.gcaFirst,
gcaCanon := middle.gcaCanon, canonlevel := middle.canonlevel, noncheaplevel := middle.noncheaplevel,
allsamelevel := middle.allsamelevel, cosetindex := middle.cosetindex, stabvertex := middle.stabvertex,
numnodes := middle.numnodes, tctotal := middle.tctotal, canupdates := middle.canupdates,
numorbits := middle.numorbits, numgenerators := middle.numgenerators, numbadleaves := middle.numbadleaves,
maxlevel := middle.maxlevel, order := middle.order, genTrace := middle.genTrace, workperm := middle.workperm };
have ready := recover (n + 2) f.codes.length left;
∃ (bs' : List Nat), ∃ (fs' : List Nat), Comparison ctx f.codes bs' fs' ready ∧ ready.compCanon ≤ 0 ∧ SearchState.best ctx ready = SearchState.key ctx bs' ready ∧ SearchState.best ctx out = SearchState.key ctx bs' ready
Cleanup preserves a settled receipt, and recovery identifies the next sweep's ghost incumbent with the actual returned stored key.