theorem Hex.GraphIso.Nauty.Sparse.uniform_step {n k : Nat} {G : Sparse.Colored n k} {tcLevel level numcells : Nat} {st : State n} {targets : List Nat} {key : Key n} (hn : 0 < n) (hlevel : 1 ≤ level) (hnode : NodeInv G level numcells st) (hu : Generation.Uniform G.graph tcLevel level (State.refined (Graph.ofGraph G.graph) level numcells st) targets key) (hm : Generation.Matches G.graph level st targets key) (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); 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 ∧ ∃ (rest : List Nat), ∃ (tail : Key n), Generation.Uniform G.graph tcLevel (level + 1) (State.refined (Graph.ofGraph G.graph) (level + 1) (p.fst + 1) ch) rest tail ∧ Generation.Matches G.graph (level + 1) ch rest tail

A matching uniform native node continues through its actual minimum cursor. Its cached child retains the uniform suffix and the literal stored reference, without a cheap-shape or generation-completeness premise.