theorem Hex.GraphIso.Nauty.Sparse.firstChild_route {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tv last : Nat} {st leaf : State n} (hn : 0 < n) (hl : 1 ≤ level) (hok : NodeInv G level numcells st) (htsize : n < st.firsttc.size) (hcsize : n + 1 < st.firstcode.size) (hopen : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).fst ≠ n) (htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.fst.nextElem none = some tv) (horbit : (cheapCheck true level (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd.snd).orbits[tv]! = tv) (hpath : have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel (level + 1) (r.fst + 1) (Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd)) last leaf) : have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st; have out := (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (r.fst + 1) (Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))).snd; have result := Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv (afterChildFirst level tv out)); RouteHistory G.graph tcLevel level level r.fst result

Completion of the actual first child initializes the general guided history at its recovered parent. Both the selected reference and current ancestor witness are derived from native execution, without a cheap guard.

theorem Hex.GraphIso.Nauty.Sparse.firstChild_recorded {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tv last : Nat} {st leaf : State n} (hn : 0 < n) (hl : 1 ≤ level) (hok : NodeInv G level numcells st) (htsize : n < st.firsttc.size) (hopen : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).fst ≠ n) (hpath : have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel (level + 1) (r.fst + 1) (Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd)) last leaf) : have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st; have out := (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (r.fst + 1) (Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))).snd; have result := Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv (afterChildFirst level tv out)); RouteRecorded G.graph tcLevel level r.snd.fst.toNat result

The first child's actual saved target supplies the guided choice for the remaining siblings, after every inner return and parent recovery.