theorem
Hex.GraphIso.Nauty.child_shape
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{level numcells tc tv : Nat}
{st : Search n}
{cell : VSet n}
(first : Bool)
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(htarget : Generic.Target (fun (st : Search n) => st) level tc cell st)
(htv : cell.mem tv = true)
(hshape : NodeShape n level st.ptn)
:
The small-cell shape descends through the actual individualized child and its refinement; it depends only on the parent partition.
theorem
Hex.GraphIso.Nauty.cheap_shape
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{level numcells : Nat}
{st : Search n}
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(heq : Equitable ctx level st.lab st.ptn)
(hcheap : (cheapCheck false level st).noncheaplevel ≤ level)
:
An off-path sweep retaining a cheap boundary has passed its actual cheap-cell test at the current partition.
theorem
Hex.GraphIso.Nauty.recover_shape
{n k : Nat}
{G : Colored n k}
{level numcells : Nat}
{st out : Search n}
(hok : SearchOk G level numcells st)
(hout : SearchOut G level level st out)
(hs : st.noncheaplevel ≤ level → NodeShape n level st.ptn)
(hb : out.noncheaplevel = st.noncheaplevel ∨ level + 1 ≤ out.noncheaplevel)
(hr : (recover (n + 2) level out).noncheaplevel ≤ level)
:
Recovery retains a parent's small-cell shape whenever the returning child has not replaced its saved boundary by a deeper one.