theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Pass.lab_eq {n level : Nat} {distance : Bool} {key : Nat → Nat} {xs : List Nat} {s a : RefineSt n} (h : Pass level distance key xs s a) {t b : RefineSt n} : Pass level distance key xs t b → s.lab.toList.Perm (List.range n) → s.ptn.size = n → t.lab = s.lab → t.ptn = s.ptn → Index.Valid n s.lab s.ptn level s.cellstart s.cellend → Index.Valid n t.lab t.ptn level t.cellstart t.cellend → a.lab = b.lab

The complete touched-cell fold gives identical labels from identical input arrays and semantic counts. Only processed cells constrain hits.