theorem
Hex.GraphIso.Nauty.Sparse.canonFloor
{n : Nat}
(g : Graph n)
(inf tcLevel bound : Nat)
:
Generic.BoundedPolicy g inf tcLevel bound fun (st : State n) => bound ≤ st.gcaCanon
Native installation and recovery preserve a lower bound on the canonical ancestor while the traversal stays below that bound.
theorem
Hex.GraphIso.Nauty.Sparse.firstPath_canon
{n : Nat}
{g : Graph n}
{inf tcLevel fuel level numcells last bound : Nat}
{st leaf : State n}
(path : Generic.FirstPath g tcLevel fuel level numcells st last leaf)
(hb : bound ≤ level)
:
The first leaf installs its ancestor at its actual depth, and the rest of that first-path call retains every older receiving lower bound.
theorem
Hex.GraphIso.Nauty.Sparse.node_order
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells : Nat}
{st : State n}
(hn : 0 < n)
(hl : 1 ≤ level)
(hi : NodeInv G level numcells st)
(hf : st.gcaFirst ≤ level)
(ho : st.gcaFirst ≤ st.gcaCanon)
:
Every native off-path call preserves the order of the two ancestor counters. The canonical lower bound follows from executed provenance.