theorem
Hex.GraphIso.Nauty.Max.canonFloor
{n : Nat}
(ctx : Ctx n)
(inf tcLevel bound : Nat)
:
Generic.BoundedPolicy ctx inf tcLevel bound fun (st : Search n) => bound ≤ st.gcaCanon
Below a fixed level, installations and recovery retain that lower bound on the canonical ancestor.
theorem
Hex.GraphIso.Nauty.Max.firstPath_canon
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells last bound : Nat}
{st leaf : Search n}
(path : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
(hb : bound < level)
:
The actual first leaf installs a canonical ancestor below every strictly older receiving loop, and the remaining traversal preserves it.
theorem
Hex.GraphIso.Nauty.Max.node_order
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level numcells : Nat}
{st : Search n}
(hn0 : 0 < n)
(hl : 1 ≤ level)
(hok : SearchOk G level numcells st)
(hgf : st.gcaFirst < level)
(horder : st.gcaFirst ≤ st.gcaCanon)
:
An off-path call preserves the ordering of its two ancestor counters.