theorem Hex.GraphIso.Nauty.rows_emit {n : Nat} {ctx : Ctx n} {level : Nat} {st : Search n} (hgsz : ctx.g.size = n) (hwork : st.workperm.size = n) (hfirst : st.firstlab.size = n) (hfirstPerm : st.firstlab.toList.Perm (List.range n)) (hlab : st.lab.size = n) (hlabPerm : st.lab.toList.Perm (List.range n)) (hrows : leafRows ctx st.firstlab = leafRows ctx st.lab) (heq : st.eqlevFirst = level) : have c := classify ctx 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 ctx st.firstlab out.snd.lab out.snd.genTrace

Equal reference rows at a matching leaf force the actual code-one classification, with its checked permutation in the emitted trace.

theorem Hex.GraphIso.Nauty.matching_leaf {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells : Nat} {st : Search n} {targets : List Nat} {key : Key n} (hgsz : ctx.g.size = n) (hwork : st.workperm.size = n) (hfirst : st.firstlab.size = n) (hfirstPerm : st.firstlab.toList.Perm (List.range n)) (hit : IterOk ctx level (SearchState.refined ctx level numcells st)) (hnum : (SearchState.refined ctx level numcells st).numcells = n) (hdisc : ∀ (q : Nat), q < n → (SearchState.refined ctx level numcells st).ptn[q]! ≤ level) (hm : Generation.Matches ctx level st targets key) (hp : Generation.HasLeaf ctx tcLevel level (SearchState.refined ctx level numcells st) targets key) (heq : st.eqlevFirst = level - 1) : have out := node false ctx inf tcLevel (fuel + 1) level numcells st; out.fst = Generic.Exit.unwind st.gcaFirst false ∧ LabelCarrier ctx st.firstlab out.snd.lab out.snd.genTrace

A discrete matching node emits its first-reference carrier in the actual search call, including refinement and comparison preparation.