theorem
Hex.GraphIso.Nauty.FirstPre.code_prefix
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(h : FirstPre G ctx level numcells st)
{cs : List Nat}
(hlen : cs.length + 1 = level)
(hcs : StoredCodes st.firstcode 1 cs)
:
StoredCodes (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd.firstcode 1
(cs ++ [(SearchState.refined ctx level numcells st).longcode])
The prepared first node has stored its incoming prefix followed by its own actual refinement code.
theorem
Hex.GraphIso.Nauty.firstSweep_codes
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
(hn0 : 0 < n)
(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)
(level numcells tc tv index : Nat)
(cell : VSet n)
(st : Search n)
(horbit : st.orbits[tv]! = tv)
(hfuel : n ≤ level + fuel)
(hcursor : n ≤ tv + (cfuel + 1))
(cs bs fs : List Nat)
(hlen : cs.length = level)
(hchild :
ReturnCodes ctx cs bs fs
(node true ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).snd)
(hready :
have out := (node true ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).snd;
have left :=
have __src := afterChildFirst level tv out;
{ lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits,
fixedpts := out.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode,
canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab,
canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst,
eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon,
canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel,
cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes,
tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits,
numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel,
order := __src.order, genTrace := __src.genTrace, workperm := __src.workperm };
SweepPre G ctx tcLevel true level numcells tc tv none cell (recover (n + 2) level left))
:
have before := (node true ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).snd;
have result := sweep true ctx (n + 2) tcLevel fuel (cfuel + 1) level numcells tc tv (some tv) cell index st;
∃ (bs' : List Nat), ReturnCodes ctx cs bs' fs result.snd.snd ∧ Generic.Grows (SearchState.key ctx bs before) (SearchState.key ctx bs' result.snd.snd)
The first child's settled code machines survive all later siblings, whose incumbents can only improve the value installed by that child.
theorem
Hex.GraphIso.Nauty.firstPath_codes
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(hn0 : 0 < n)
(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)
(hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
(hin : FirstPre G ctx level numcells st)
(hcanon : st.canoncode.size = n + 2)
(hfuel : n + 1 ≤ level + fuel)
{cs : List Nat}
(hlen : cs.length + 1 = level)
(hstore : StoredCodes st.firstcode 1 cs)
(hlt : ∀ (c : Nat), c ∈ cs → c < codeSentinel)
:
The actual first descent initializes the code machines; each ancestor then uses the same off-path comparison theorem for its remaining siblings.
Every nonempty coloured search run returns settled code comparisons, with the first reference and incumbent supplied by its actual descent.
The completed nonempty run exposes a readable installed incumbent.