theorem
Hex.GraphIso.Nauty.Sparse.CellCover.pruned
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc len : Nat}
{cs : List Nat}
{st : State n}
{live : Nat → Prop}
{best : Option (Key n)}
{filtered : VSet n}
(h : CellCover G.graph tcLevel fuel level numcells tc len cs st live best)
(hrdy : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(hc : IsCell st.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
(hf : n < fuel + (numcells + 1))
(hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true)
(hdrop :
∀ (v : Nat),
live v →
filtered.mem v = false →
∃ (gamma : Array Nat), checkAutom (Graph.context G.graph).g gamma = true ∧ CellStab st.ptn level st.lab gamma ∧ gamma[v]! < v)
:
A descending automorphism filter preserves coverage of the original target cell. A carrier may land in a visited child or outside the previous survivors; the established ranked coverage resolves either case.
theorem
Hex.GraphIso.Nauty.Sparse.PairsReady.long_cover
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc len : Nat}
{st : State n}
{cell : VSet n}
{cs : List Nat}
{live : Nat → Prop}
{best : Option (Key n)}
(h : PairsReady G tcLevel level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(hc : IsCell st.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
(hf : n < fuel + (numcells + 1))
(hcover : CellCover G.graph tcLevel fuel level numcells tc len cs st live best)
(hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true)
(hmem : ∀ (v : Nat), live v → cell.mem v = true)
:
The actual native long filter preserves coverage using the current path's checked interpretation of every applicable stored pair.
theorem
Hex.GraphIso.Nauty.Sparse.PairsReady.return_cover
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel runFuel level numcells tc tv target len : Nat}
{first : Bool}
{cell : VSet n}
{st : State n}
{key : Nat → Key n}
{guideBest : Option (Key n)}
{cs : List Nat}
{live : Nat → Prop}
{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)
(hguide : CanonGuide level tc st key guideBest st)
(hc : IsCell st.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
(hf : n < fuel + (numcells + 1))
(hcover : CellCover G.graph tcLevel fuel level numcells tc len cs st live best)
(hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true)
(hmem : ∀ (v : Nat), live v → cell.mem v = true)
:
have raw :=
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel runFuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
have out := Generic.Policy.leaveChild tv raw;
CellCover G.graph tcLevel fuel level numcells tc len cs st
(fun (v : Nat) => live v ∧ (Generic.Policy.shortprune cell out).mem v = true) best
Receiving a native short return preserves the frozen parent's child coverage. The pair validity comes from the actual completed child, and the key equality comes from transport of all its unpruned sparse leaves.