theorem
Hex.GraphIso.Nauty.Sparse.firstLeaf_boundary
{n : Nat}
{g : Graph n}
{tcLevel fuel level numcells last bound saved : Nat}
{st leaf : State n}
(path : Generic.FirstPath g tcLevel fuel level numcells st last leaf)
(hl : bound < level)
(h : st.noncheaplevel = saved ∨ bound < st.noncheaplevel)
:
The actual first descent retains an older boundary or replaces it strictly below a fixed ancestor.
theorem
Hex.GraphIso.Nauty.Sparse.firstPath_boundary
{n : Nat}
{g : Graph n}
{inf tcLevel fuel level numcells last : Nat}
{st leaf : State n}
(path : Generic.FirstPath g tcLevel fuel level numcells st last leaf)
(hl : 0 < level)
:
(Generic.node true g inf tcLevel fuel level numcells st).snd.noncheaplevel = st.noncheaplevel ∨ level ≤ (Generic.node true g inf tcLevel fuel level numcells st).snd.noncheaplevel
Completing the first node, including later siblings, cannot replace its incoming boundary strictly above that node.
theorem
Hex.GraphIso.Nauty.Sparse.CheapBoundary.firstNode
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells last : Nat}
{st leaf : State n}
(h : CheapBoundary G level st)
(hn : 0 < n)
(hl : 1 < level)
(hi : NodeInv G level numcells st)
(path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf)
:
CheapBoundary G level (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd
The complete first-child call preserves its still-active older pairs. This uses actual first-path existence and native frame preservation.