theorem Hex.GraphIso.Nauty.Sparse.reference_step {n k : Nat} {G : Sparse.Colored n k} {tcLevel base level numcells : Nat} {root : RefineSt n} {st : State n} (hn : 0 < n) (hlevel : 1 ≤ level) (hnode : NodeInv G level numcells st) (href : FirstRef G.graph tcLevel base root st) (hr : RefineSt.Ready G.graph base root) (hshape : NodeShape n base root.ptn) (hdepth : level ≤ href.last) (hfollow : FollowsPerm G.graph st.firsttc base root level (State.refined (Graph.ofGraph G.graph) level numcells st)) (hcode : (State.refined (Graph.ofGraph G.graph) level numcells st).longcode = st.firstcode[level]!) (heq : st.eqlevFirst = level - 1) (hnc : (State.refined (Graph.ofGraph G.graph) level numcells st).numcells < n) : have p := prepareOther (Graph.ofGraph G.graph) tcLevel level numcells st; classify (Graph.ofGraph G.graph) level p.fst p.snd.snd.snd.snd.snd = (Generic.Leaf.internal, p.snd.snd.snd.snd.snd) ∧ ∃ (tv : Nat), p.snd.snd.snd.fst.nextElem none = some tv ∧ have ch := Generic.Policy.child false level p.snd.snd.fst.toNat tv (cheapCheck false level p.snd.snd.snd.snd.snd); level + 1 ≤ href.last ∧ SearchState.reference ch = SearchState.reference st ∧ NodeInv G (level + 1) (p.fst + 1) ch ∧ ch.gcaFirst = st.gcaFirst ∧ ch.workperm.size = st.workperm.size ∧ ch.firstlab = st.firstlab ∧ ch.eqlevFirst = level ∧ FollowsPerm G.graph ch.firsttc base root (level + 1) (State.refined (Graph.ofGraph G.graph) (level + 1) (p.fst + 1) ch) ∧ (State.refined (Graph.ofGraph G.graph) (level + 1) (p.fst + 1) ch).longcode = ch.firstcode[level + 1]!

A matching open node takes its actual minimum target vertex and retains the saved reference and matching code at the resulting cached child visit. All inputs describe native entry states and saved histories.