theorem
Hex.GraphIso.Nauty.Sparse.Ready.of_frame
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{st : State n}
(h : Ready G level numcells st)
{out : State n}
(hl : out.lab = st.lab)
(hp : out.ptn = st.ptn)
(hc : out.canonlab = st.canonlab ∨ out.canonlab = st.lab)
(hs : Scratch.Valid n out.lab out.ptn level out.canong.scratch)
:
Ready G level numcells out
Bookkeeping with an unchanged partition preserves the equitable parent invariant, including optional installation of the current canonical label.
theorem
Hex.GraphIso.Nauty.Sparse.Ready.frame
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{st : State n}
(h : Ready G level numcells st)
{out : State n}
(hl : out.lab = st.lab)
(hp : out.ptn = st.ptn)
(hf : out.firstlab = st.firstlab ∨ out.firstlab = st.lab)
(hc : out.canonlab = st.canonlab ∨ out.canonlab = st.lab)
(hs : Scratch.Bounded n out.canong.scratch)
:
FrameOut G level level st out
theorem
Hex.GraphIso.Nauty.Sparse.Ready.partition
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{st : State n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
:
NodeOk n level st.lab st.ptn VSet.empty
The parent's structural partition facts do not depend on the stale active set left by a completed descendant.
theorem
Hex.GraphIso.Nauty.Sparse.Ready.recover
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{st : State n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
{out : State n}
(hx : FrameOut G level level st out)
:
have r := Generic.Policy.recover (n + 2) level out;
Ready G level numcells r ∧ FrameOut G level level st r
A returned child is recovered to the exact parent partition. Reordering within its cells preserves equitability; the real policy invalidates indices.