theorem
Hex.GraphIso.Nauty.CanonGuide.frame
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells tc len : Nat}
{cs : List Nat}
{base st : Search n}
{best : Option (Key n)}
(h :
CanonGuide level tc base
(fun (v : Nat) => prefixKey cs (vertexKey ctx tcLevel fuel level base.lab base.ptn tc numcells v)) best st)
(hf : SearchOut G level level base st)
(hbase : SearchOk G level numcells base)
(hst : SearchOk G level numcells st)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hc : IsCell base.ptn level tc len)
(hlen : 2 ≤ len)
(hr : tc + len ≤ n)
(hfuel : level + 1 + fuel ≤ n + 1)
:
The guide and its vertex keys transfer together from the frozen sweep frame to the current ordering, including references removed by a filter.
theorem
Hex.GraphIso.Nauty.child_canon_cover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel runFuel level numcells tc tv len : Nat}
{first childFirst : Bool}
{cell : VSet n}
{st : Search n}
{cs : List Nat}
{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)
(htv : cell.mem tv = true)
(hgsz : ctx.g.size = n)
(hc : IsCell st.ptn level tc len)
(hr : tc + len ≤ n)
(hfuel : level + 1 + fuel ≤ n + 1)
(hguide :
CanonGuide level tc st (fun (v : Nat) => prefixKey cs (vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells v))
best st)
:
have out := (node childFirst ctx (n + 2) tcLevel runFuel (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]!) →
Generic.Covers (prefixKey cs (vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells tv)) best
A canonical scatter returning from an actual child identifies that whole child's specification key with an already covered reference child. The emitting leaf may lie below arbitrarily many intermediate sweeps.
theorem
Hex.GraphIso.Nauty.SweepPre.short_witness
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel runFuel level numcells tc tv1 tv target len : Nat}
{first : Bool}
{cell : VSet n}
{base st : Search n}
{cs : List Nat}
{best : Option (Key n)}
(h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st)
(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)
(he :
(node false ctx (n + 2) tcLevel runFuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).fst = Generic.Exit.unwind target true)
(hi :
RunInv G ctx
(node false ctx (n + 2) tcLevel runFuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd)
(hreceive : level ≤ target)
(hbase : SearchOk G level numcells base)
(hframe : SearchOut G level level base st)
(hc : IsCell base.ptn level tc len)
(hlen : 2 ≤ len)
(hr : tc + len ≤ n)
(hfuel : level + 1 + fuel ≤ n + 1)
(hguide :
CanonGuide level tc base
(fun (v : Nat) => prefixKey cs (vertexKey ctx tcLevel fuel level base.lab base.ptn tc numcells v)) best st)
:
An actual received short return either covers the entire current child through its canonical-reference automorphism, or carries the cheap boundary. Classifier provenance and the scatter survive all intervening sweeps.