theorem Hex.GraphIso.Nauty.Sparse.cheap_reference {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root : RefineSt n} (inf tcLevel : Nat) (hn : 0 < n) (hr : RefineSt.Ready G.graph base root) (hshape : NodeShape n base root.ptn) (fuel level numcells : Nat) (st : State n) (href : FirstRef G.graph tcLevel base root st) (f : Label n) : 1 ≤ level → NodeInv G level numcells st → st.workperm.size = n → Label.ofArray? n st.firstlab = some f → CellsReach G.toDense st.firstlab → level ≤ href.last → FollowsPerm G.graph st.firsttc base root level (State.refined (Graph.ofGraph G.graph) level numcells st) → (State.refined (Graph.ofGraph G.graph) level numcells st).longcode = st.firstcode[level]! → st.eqlevFirst = level - 1 → st.gcaFirst < level → n < level + fuel → have out := Generic.node false (Graph.ofGraph G.graph) inf tcLevel fuel level numcells st; out.fst = Generic.Exit.unwind st.gcaFirst false ∧ LabelCarrier (Graph.context G.graph) st.firstlab out.snd.lab out.snd.genTrace

A native node matching a saved cheap descent follows its executed minimum cursors until it emits an automorphism carrying the saved label to the returned label. The proof follows the actual recursion bound and does not assume a return, a generated carrier, or a search maximum.

theorem Hex.GraphIso.Nauty.Sparse.DescentAt.child_returns {n k : Nat} {G : Sparse.Colored n k} {tcLevel base level numcells tc tv : Nat} {root : RefineSt n} {st : State n} {cell : VSet n} {f : Label n} (hd : DescentAt G.graph st.firsttc base root level numcells st) (href : FirstRef G.graph tcLevel base root st) (hdepth : level ≤ href.last) (hr : RefineSt.Ready G.graph base root) (hshape : NodeShape n base root.ptn) (hready : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hnc : numcells < n) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (htc : st.firsttc[level]! = Int.ofNat tc) (hw : st.workperm.size = n) (hf : Label.ofArray? n st.firstlab = some f) (hrf : CellsReach G.toDense st.firstlab) (heq : st.eqlevFirst = level) (hg : st.gcaFirst ≤ level) (first : Bool) (inf fuel : Nat) (hbudget : n < level + 1 + fuel) : have ch := Generic.Policy.child first level tc tv st; have out := Generic.node false (Graph.ofGraph G.graph) inf tcLevel fuel (level + 1) (numcells + 1) ch; out.fst = Generic.Exit.unwind st.gcaFirst false ∧ LabelCarrier (Graph.context G.graph) st.firstlab out.snd.lab out.snd.genTrace

A recovered cheap parent reaches its saved reference through every surviving target child. The conclusion includes the carrier in the actual emitted trace, and permits either native child-entry mode.