theorem
Hex.GraphIso.Nauty.child_pair
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells tc tv : Nat}
{first : Bool}
{cell : VSet n}
{base st : Search n}
{key : Nat → Key n}
{best : Option (Key n)}
(h : SearchOk G level numcells st)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hpath : FixedCells level st)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell st)
(ht : cell.mem tv = true)
(childFirst : Bool)
(hbase : SearchOk G level numcells base)
(hframe : SearchOut G level level base st)
(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 →
out.canonlab.size = n →
checkAutom ctx.g out.workperm = true →
(∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!) →
PairOk ctx.g base.ptn base.lab level (fmperm out.workperm n).fst (fmperm out.workperm n).snd
The canonical scatter of an actual child returning to this loop stabilizes the frozen parent cells. Its workspace pair is therefore valid at that parent, independently of the current ordering of labels.
theorem
Hex.GraphIso.Nauty.SweepPre.canon_pair
{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)
(hbase : SearchOk G level numcells base)
(hframe : SearchOut G level level base st)
(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 →
out.canonlab.size = n →
checkAutom ctx.g out.workperm = true →
(∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!) →
PairOk ctx.g base.ptn base.lab level (fmperm out.workperm n).fst (fmperm out.workperm n).snd
A later sibling's canonical scatter yields a valid pair at its frozen parent.