theorem
Hex.GraphIso.Nauty.prepareFirst_noncheap
{n : Nat}
(ctx : Ctx n)
(tcLevel level numcells : Nat)
(st : Search n)
:
(Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd.noncheaplevel = st.noncheaplevel
Preparing the first path does not move the cheap boundary.
theorem
Hex.GraphIso.Nauty.firstLeaf_noncheap
{n : Nat}
{ctx : Ctx n}
{tcLevel fuel level numcells last bound : Nat}
{st leaf : Search n}
(hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
(hlevel : bound < level)
(hin : bound < st.noncheaplevel)
:
The initial descent keeps every earlier failed guard below its frozen ancestor.
theorem
Hex.GraphIso.Nauty.firstPath_noncheap
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells last bound : Nat}
{st leaf : Search n}
(hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
(hlevel : bound < level)
(hin : bound < st.noncheaplevel)
:
A full first-path call also preserves failed guards at its ancestors.
theorem
Hex.GraphIso.Nauty.firstCheap_small
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(hn0 : 0 < n)
(hlevel : 1 ≤ level)
(hok : SearchOk G level numcells st)
(heq :
Equitable ctx level (SearchState.refined ctx level numcells st).lab (SearchState.refined ctx level numcells st).ptn)
(hsmall : st.noncheaplevel < level → SubtreeOk ctx level (SearchState.refined ctx level numcells st))
(hcheap :
(cheapCheck true level (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd).noncheaplevel ≤ level)
:
SubtreeOk ctx level (SearchState.refined ctx level numcells st)
A first-path node that is cheap after the guard supplies the small-cell ancestor invariant.