theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_lab {n : Nat} (G : SparseGraph n) (level split len : Nat) (s t : RefineSt n) (hs : RefineSt.Valid level s) (ht : RefineSt.Valid level t) (hl : t.lab = s.lab) (he : t.ptn = s.ptn) (hc : IsCell s.ptn level split len) (hb : split + len ≤ n) : (splitNontrivial (Graph.ofGraph G) level split s).lab = (splitNontrivial (Graph.ofGraph G) level split t).lab

Admissible scratch reuse cannot change the literal label array of the complete native nontrivial splitter, including first-touch clearing and the ordered touched-cell fold.