theorem Hex.GraphIso.Nauty.Sparse.uniform_reference {n k : Nat} {G : Sparse.Colored n k} (inf tcLevel : Nat) (hn : 0 < n) (fuel level numcells : Nat) (st : State n) (targets : List Nat) (key : Key n) : 1 ≤ level → NodeInv G level numcells st → Generation.Uniform G.graph tcLevel level (State.refined (Graph.ofGraph G.graph) level numcells st) targets key → st.workperm.size = n → CellsReach G.toDense st.firstlab → Generation.Matches G.graph level st targets key → 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 uniform matching native subtree follows its executed minimum cursors until it emits a checked first-reference carrier. This is a proof of the real recursion and scatter, without assumed generation or returns.