theorem Hex.GraphIso.Nauty.Sparse.Refinement.distance_equiv {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) (level : Nat) (s t : RefineSt n) (hs : RefineSt.Valid level s) (ht : RefineSt.Valid level t) (he : RefineSt.Equiv (renamingOf p) level s t) (hq : s.queue.size = 1) (hsingle : s.ptn[s.queue[0]!]! ≤ level) : have a := distance level (distanceStart (Graph.ofGraph G) s); have b := distance level (distanceStart (Graph.ofGraph H) t); RefineSt.Valid level a ∧ RefineSt.Valid level b ∧ RefineSt.Equiv (renamingOf p) level a b

The complete native distance branch transports from its actual sole queued singleton, including BFS initialization and every distance split.