theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.selected_lab {n : Nat} {σ : Renaming n} {level : Nat} (G : SparseGraph n) {s t : RefineSt n} (h : Equiv σ level s t) (hs : Valid level s) (ht : Valid level t) (hl : t.lab = s.lab) (pos : Nat) (hp : pos < s.queue.size) : (RefineSt.selected (Graph.ofGraph G) level pos s).lab = (RefineSt.selected (Graph.ofGraph G) level pos t).lab

Queue removal, hashing and the actual splitter branch retain literal label agreement between two admissible refinement states.

theorem Hex.GraphIso.Nauty.Sparse.Refinement.loop_lab {n : Nat} (G : SparseGraph n) (level : Nat) (s t : RefineSt n) (hs : RefineSt.Valid level s) (ht : RefineSt.Valid level t) (he : RefineSt.Equiv (renamingOf (Perm.id n)) level s t) (hl : t.lab = s.lab) : (loop (Graph.ofGraph G) level s).lab = (loop (Graph.ofGraph G) level t).lab

The complete native main loop preserves literal label equality through first-ten queue preference, swap/pop removal, both splitter branches and both stopping guards.