theorem Hex.GraphIso.Nauty.Sparse.Refinement.distance_lab {n : Nat} (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) (hk : t.hits = s.hits) (hv : ∀ (v : Nat), v < n → s.hits[v]! ≤ n) : (distance level s).lab = (distance level t).lab

The full distance-cell scan preserves literal label agreement when the captured native distance arrays agree. Valid scratch indices may differ.

theorem Hex.GraphIso.Nauty.Sparse.Refinement.shallow_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) (hq : s.queue.size = 1) : (distance level (distanceStart (Graph.ofGraph G) s)).lab = (distance level (distanceStart (Graph.ofGraph G) t)).lab

Native BFS starts at the same literal queued vertex for equal input labels. Its distances therefore agree before the complete shallow scan.