A live target is canonical or is the target saved by the first descent.
Equations
- Hex.GraphIso.Nauty.Choice ctx tcLevel level tc st = (st.eqlevFirst = level → Hex.GraphIso.Nauty.specTargetcell ctx st.lab st.ptn level tcLevel = tc ∨ st.firsttc[level]! = Int.ofNat tc)
Instances For
theorem
Hex.GraphIso.Nauty.Choice.cheap
{n : Nat}
{ctx : Ctx n}
{tcLevel level tc : Nat}
{st : Search n}
(h : Choice ctx tcLevel level tc st)
(first : Bool)
:
Choice ctx tcLevel level tc (cheapCheck first level st)
The cheap guard leaves the chosen target and its live comparison unchanged.
theorem
Hex.GraphIso.Nauty.GuidedState.choice
{n : Nat}
{ctx : Ctx n}
{tcLevel base level numcells : Nat}
{root : RefineSt n}
{st : Search n}
(h : GuidedState ctx tcLevel base root level level numcells st)
(hok : IterOk ctx base root)
(heq : Equitable ctx base root.lab root.ptn)
(hacc : bcount root.ptn base n = root.numcells)
(hnc : numcells < n)
(hlevel : 0 < level)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
:
An equitable guided endpoint makes the search's retained target canonical or equal to the saved first target.
theorem
Hex.GraphIso.Nauty.Choice.recover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells tc : Nat}
{st out : Search n}
(h : Choice ctx tcLevel level tc st)
(hb : st.eqlevFirst ≤ level)
(hlevel : 1 ≤ level)
(hn0 : 0 < n)
(hok : SearchOk G level numcells st)
(hout : SearchOut G level level st out)
(ht : out.firsttc = st.firsttc)
(hd : st.eqlevFirst < level → out.eqlevFirst < level)
:
Choice ctx tcLevel level tc (Nauty.recover (n + 2) level out)
A recovered parent retains its canonical-or-saved target even when its labels were reordered by the child.
theorem
Hex.GraphIso.Nauty.Choice.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 : Choice ctx tcLevel level tc st)
(hb : st.eqlevFirst ≤ level)
(first : Bool)
(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) (child first level tc tv st)).snd;
Choice ctx tcLevel level tc
(Nauty.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 })
The actual child call supplies the frame and divergence properties needed to retain its parent's choice after recovery.