theorem Hex.GraphIso.Nauty.Sparse.rows_emit {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} {f l : Label n} (hw : st.workperm.size = n) (hf : Label.ofArray? n st.firstlab = some f) (hl : Label.ofArray? n st.lab = some l) (hrf : CellsReach G.toDense st.firstlab) (hrl : CellsReach G.toDense st.lab) (hrows : G.graph.relabel l.perm = G.graph.relabel f.perm) (heq : st.eqlevFirst = level) : have c := classify (Graph.ofGraph G.graph) level n st; have out := leafExit c.fst level c.snd; c.fst = Generic.Leaf.autoFirst ∧ out.fst = Generic.Exit.unwind st.gcaFirst false ∧ LabelCarrier (Graph.context G.graph) st.firstlab out.snd.lab out.snd.genTrace

Matching native leaf graphs force first-reference admission. The actual scatter is appended to the unbounded trace and maps the saved label to the returned label, whether the cheap guard or adjacency scan accepts.

theorem Hex.GraphIso.Nauty.Sparse.matching_leaf {n k : Nat} {G : Sparse.Colored n k} {inf tcLevel fuel level numcells : Nat} {st : State n} {f l : Label n} (hn : 0 < n) (hlevel : 1 ≤ level) (hnode : NodeInv G level numcells st) (hw : st.workperm.size = n) (hf : Label.ofArray? n st.firstlab = some f) (hrf : CellsReach G.toDense st.firstlab) (hl : Label.ofArray? n (State.refined (Graph.ofGraph G.graph) level numcells st).lab = some l) (hnum : (State.refined (Graph.ofGraph G.graph) level numcells st).numcells = n) (hcode : (State.refined (Graph.ofGraph G.graph) level numcells st).longcode = st.firstcode[level]!) (hrows : G.graph.relabel l.perm = G.graph.relabel f.perm) (heq : st.eqlevFirst = level - 1) : have out := Generic.node false (Graph.ofGraph G.graph) inf tcLevel (fuel + 1) 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 matching discrete visit emits its reference carrier in the actual native node call, including cached refinement and code comparison.