theorem Hex.GraphIso.Nauty.Sparse.FirstRef.next_depth {n : Nat} {G : SparseGraph n} {tcLevel base level : Nat} {root current : RefineSt n} {st : State n} (h : FirstRef G tcLevel base root st) (hdepth : level ≤ h.last) (hr : RefineSt.Ready G base root) (hshape : NodeShape n base root.ptn) (hp : FollowsPerm G st.firsttc base root level current) (hopen : discreteAt current.ptn level n ≠ true) : level < h.last

An open node following the saved cheap descent is strictly above its terminal depth, even after reordering inside recovered cells.

theorem Hex.GraphIso.Nauty.Sparse.chooseTarget_match {n : Nat} (g : Graph n) (tcLevel level numcells : Nat) (st : State n) (heq : st.eqlevFirst = level) : have out := chooseTarget false g tcLevel level numcells st; out.fst = st.firsttc[level]! → out.snd.snd.snd.eqlevFirst = level

Matching the saved target prevents the native target dispatch from demoting first-code agreement. This includes its scratch detachment.

theorem Hex.GraphIso.Nauty.Sparse.FirstRef.child_code {n : Nat} {G : SparseGraph n} {tcLevel base level : Nat} {root current : RefineSt n} {st : State n} (h : FirstRef G tcLevel base root st) (hdepth : level + 1 ≤ h.last) (hr : RefineSt.Ready G base root) (hc : RefineSt.Ready G level current) (hshape : NodeShape n base root.ptn) (hp : FollowsPerm G st.firsttc base root level current) {tc len o : Nat} (hcell : IsCell current.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (htc : st.firsttc[level]! = Int.ofNat tc) (scratch : Scratch) (hs : Scratch.Bounded n scratch) : (RefineSt.child (Graph.ofGraph G) level current tc current.lab[tc + o]! scratch).longcode = st.firstcode[level + 1]!

Every actual cached child at a stored target has the next saved code below a cheap ancestor. The parent may have been reordered by completed sibling searches; only its cell contents and saved descent are needed.

theorem Hex.GraphIso.Nauty.Sparse.FirstRef.child_visit {n : Nat} {G : SparseGraph n} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (h : FirstRef G tcLevel base root st) (hdepth : level + 1 ≤ h.last) (hr : RefineSt.Ready G base root) (hshape : NodeShape n base root.ptn) (hd : DescentAt G st.firsttc base root level numcells st) (first : Bool) {tc len o : Nat} (hc : IsCell st.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (htc : st.firsttc[level]! = Int.ofNat tc) (hs : Scratch.Bounded n st.canong.scratch) : have next := Generic.Policy.child first level tc st.lab[tc + o]! st; have r := State.refined (Graph.ofGraph G) (level + 1) (numcells + 1) next; FollowsPerm G st.firsttc base root (level + 1) r ∧ r.longcode = st.firstcode[level + 1]!

Native child entry, scratch invalidation and refinement retain the saved-target history and read the next saved code after sibling recovery.