theorem
Hex.GraphIso.Nauty.Max.first_fixed
{n : Nat}
(ctx : Ctx n)
(tcLevel level numcells : Nat)
(st : Search n)
:
(cheapCheck true level (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd).fixedpts = st.fixedpts
First-node preparation leaves the individualized base unchanged.
theorem
Hex.GraphIso.Nauty.Max.first_terminal
{n k : Nat}
{G : Colored n k}
{tcLevel fuel level numcells : Nat}
{st : Search n}
{cs bs fs : List Nat}
{parents : Parents n}
(hi :
NodeInput G { g := rowsOf G } tcLevel fuel true { level := level, numcells := numcells, codes := cs, entry := st } bs
fs parents)
{base : List (Fin n)}
(hbase : ∀ (b : Fin n), st.fixedpts.mem ↑b = true ↔ b ∈ base)
(hdisc : (Generic.prepareFirst { g := rowsOf G } tcLevel level numcells st).fst = n)
{p : Perm n}
(hp : IsIso G G p)
(hfix : Perm.Fixes base p)
:
A discrete first node has trivial point stabilizer.