theorem
Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.member
{n k : Nat}
{G : Sparse.Colored n k}
{c : Cell n}
{st : State n}
{len v : Nat}
(h : Valid G c)
(he : FrameOut G c.level c.level c.entry st)
(hw : IsCell st.ptn c.level c.tc len)
(hv : (windowSet n st.lab c.tc len).mem v = true)
:
A recovered window at the selected coordinate is the same complete cell as the frozen selection, regardless of mutable filtering.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Loop.cover
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{l : Loop n}
{best : Option (Key n)}
(h : Frame.Valid G l.node)
(hi : (visit (Graph.ofGraph G.graph) l.node.level l.node.numcells l.node.entry).fst < n)
(hc : Cell.Valid G (cell G.graph tcLevel l))
(ht : Frame.Choice G.graph tcLevel l.node (cell G.graph tcLevel l).tc best)
(hd :
∀ (v : Nat),
(cell G.graph tcLevel l).vertices.mem v = true → Covers (Cell.key G.graph tcLevel (cell G.graph tcLevel l) v) best)
:
Exhausting the actual target covers its native node. If the target was hinted, the existing negative-prefix alternative covers the node.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Loop.ranked
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{l : Loop n}
{st : State n}
{bs : List Nat}
{cell : VSet n}
{tv : Nat}
(hc : Cell.Valid G (Loop.cell G.graph tcLevel l))
(he : FrameOut G l.node.level l.node.level (Loop.cell G.graph tcLevel l).entry st)
(hs : Ready G l.node.level (Loop.cell G.graph tcLevel l).numcells st)
(hd : Cell.Cover G.graph tcLevel (Loop.cell G.graph tcLevel l) (Remaining (some tv) cell) (State.key G.graph bs st))
:
Parent.Ranked G.graph tcLevel (parent G.graph tcLevel l st bs cell tv)
Ranked coverage of the actual selected cell supplies the suspended parent's smaller-vertex invariant, for hinted and unhinted selections.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Loop.canon_guide
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{l : Loop n}
{st : State n}
{bs : List Nat}
{cell : VSet n}
{tv : Nat}
(hc : Cell.Valid G (Loop.cell G.graph tcLevel l))
(he : FrameOut G l.node.level l.node.level (Loop.cell G.graph tcLevel l).entry st)
(hs : Ready G l.node.level (Loop.cell G.graph tcLevel l).numcells st)
(hg : Parent.Guided G.graph tcLevel (parent G.graph tcLevel l st bs cell tv))
:
The receiving parent's canonical guide is also a guide for the frozen actual cell used by both native pruning filters.