theorem
Hex.GraphIso.Nauty.Sparse.firstPath_frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells last : Nat}
{st leaf : State n}
(path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf)
(hn : 0 < n)
(hl : 1 ≤ level)
(hi : NodeInv G level numcells st)
:
The literal first descent retains the entry's cell contents and ancestor boundaries, including the native refinement at each level.
theorem
Hex.GraphIso.Nauty.Sparse.child_first_store
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv last : Nat}
{cell : VSet n}
{st leaf : State n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(first : Bool)
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(path :
Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st) last leaf)
:
The reference saved by a first-child call comes from that child's actual first descent. It respects the parent's cells and retains the selected vertex at the target position, even after later siblings return.