theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.stabilizes
{n k : Nat}
{G : Sparse.Colored n k}
{c : Cell n}
{st : State n}
{gamma : Array Nat}
(h : Valid G c)
(he : FrameOut G c.level c.level c.entry st)
(hs : Ready G c.level c.numcells st)
(hg : CellStab st.ptn c.level st.lab gamma)
:
A pair interpreted in the current recovered partition also stabilizes the original frozen cells; both share the actual parent frame.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.long
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{c : Cell n}
{st : State n}
{cell : VSet n}
{live : Nat → Prop}
{best : Option (Key n)}
(h : Cover G.graph tcLevel c live best)
(hc : Valid G c)
(he : FrameOut G c.level c.level c.entry st)
(hp : PairsReady G tcLevel c.level c.numcells st)
(hv : ∀ (v : Nat), live v → c.vertices.mem v = true)
(hm : ∀ (v : Nat), live v → cell.mem v = true)
:
The literal native long filter preserves coverage in the original window, even after recovery has reordered its vertices.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.short
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel runFuel : Nat}
{c : Cell n}
{st : State n}
{cell : VSet n}
{tv target : Nat}
{first : Bool}
{live : Nat → Prop}
{best guideBest : Option (Key n)}
(h : Cover G.graph tcLevel c live best)
(hc : Valid G c)
(he : FrameOut G c.level c.level c.entry st)
(hp : PairsReady G tcLevel c.level c.numcells st)
(ht : Generic.Target State.frame c.level c.tc cell st)
(htv : cell.mem tv = true)
(hrecord : CheapRecorded c.level c.tc st)
(hcanon : st.gcaCanon ≤ c.level)
(hcap : 0 < st.wsCap)
(hexit :
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel runFuel (c.level + 1) (c.numcells + 1)
(Generic.Policy.child first c.level c.tc tv st)).fst = Generic.Exit.unwind target true)
(hreceive : c.level ≤ target)
(hguide : CanonGuide c.level c.tc c.entry (key G.graph tcLevel c) guideBest st)
(hv : ∀ (v : Nat), live v → c.vertices.mem v = true)
(hm : ∀ (v : Nat), live v → cell.mem v = true)
:
have raw :=
(Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel runFuel (c.level + 1) (c.numcells + 1)
(Generic.Policy.child first c.level c.tc tv st)).snd;
Cover G.graph tcLevel c
(fun (v : Nat) => live v ∧ (Generic.Policy.shortprune cell (Generic.Policy.leaveChild tv raw)).mem v = true) best
The actual received short pair preserves coverage in the original window. Its checked carrier and strict descent come from the executed child, not a premise about every vertex removed by the filter.