theorem
Hex.GraphIso.Nauty.Sparse.child_canon_cover
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel runFuel level numcells tc tv len : Nat}
{first childFirst : Bool}
{cell : VSet n}
{st : State n}
{cs : List Nat}
{best : Option (Key n)}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hc : IsCell st.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
(hf : n < fuel + (numcells + 1))
(hguide :
CanonGuide level tc st
(fun (v : Nat) => prefixKey cs (vertexKey G.graph tcLevel fuel level st.lab st.ptn tc numcells v)) best st)
:
have out :=
(Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel runFuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
out.gcaCanon = level →
out.canonlab.size = n →
Automorphism G out.workperm →
(∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!) →
Covers (prefixKey cs (vertexKey G.graph tcLevel fuel level st.lab st.ptn tc numcells tv)) best
A canonical scatter returning from an actual child identifies its whole unpruned maximum with the already covered reference child. The emitting leaf may have returned through arbitrarily many intervening native sweeps.
theorem
Hex.GraphIso.Nauty.Sparse.PairsReady.short_witness
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel runFuel level numcells tc tv target len : Nat}
{first : Bool}
{cell : VSet n}
{base st : State n}
{cs : List Nat}
{best : Option (Key n)}
(h : PairsReady G tcLevel level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hrecord : CheapRecorded level tc st)
(hcanon : st.gcaCanon ≤ level)
(hcap : 0 < st.wsCap)
(he :
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel runFuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).fst = Generic.Exit.unwind target true)
(hreceive : level ≤ target)
(hbase : Ready G level numcells base)
(hframe : FrameOut G level level base st)
(hc : IsCell base.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
(hf : n < fuel + (numcells + 1))
(hguide :
CanonGuide level tc base
(fun (v : Nat) => prefixKey cs (vertexKey G.graph tcLevel fuel level base.lab base.ptn tc numcells v)) best st)
:
have out :=
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel runFuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
Covers (prefixKey cs (vertexKey G.graph tcLevel fuel level st.lab st.ptn tc numcells tv)) best ∨ target ≤ out.noncheaplevel - 1
An actually received short return either covers the entire current child via its canonical automorphism, or retains the implicit cheap-boundary limit. All child result validity is derived from the native entry invariants.