theorem
Hex.GraphIso.Nauty.Sparse.CellCover.frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc len : Nat}
{cs : List Nat}
{st out : State n}
{live : Nat → Prop}
{best : Option (Key n)}
(h : CellCover G.graph tcLevel fuel level numcells tc len cs st live best)
(hf : FrameOut G level level st out)
(hs : Ready G level numcells st)
(ho : Ready G level numcells out)
(hn : 0 < n)
(hl : 1 ≤ level)
(hc : IsCell st.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
(hfuel : n < fuel + (numcells + 1))
(hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true)
:
Parent recovery preserves the child coverage relation, including previously covered and still-live representatives in the reordered frame.
theorem
Hex.GraphIso.Nauty.Sparse.CanonGuide.frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc len : Nat}
{cs : List Nat}
{base st : State n}
{best : Option (Key n)}
(h :
CanonGuide level tc base
(fun (v : Nat) => prefixKey cs (vertexKey G.graph tcLevel fuel level base.lab base.ptn tc numcells v)) best st)
(hf : FrameOut G level level base st)
(hbase : Ready G level numcells base)
(hst : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(hc : IsCell base.ptn level tc len)
(hlen : 1 < len)
(hr : tc + len ≤ n)
(hfuel : n < fuel + (numcells + 1))
:
The reference and its native child key transfer together from the frozen base to the current frame, even if filtering removed that reference vertex from the mutable target set.