theorem Hex.GraphIso.Nauty.Sparse.distvals_correct {n : Nat} (G : SparseGraph n) (root : Fin n) : Distances G root (distvals (Graph.ofGraph G) ↑root)

The executed packed-adjacency BFS computes shortest-path distances, including its early exit once all vertices have been discovered.

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.distvals_root {n : Nat} (G : SparseGraph n) (root : Fin n) : (distvals (Graph.ofGraph G) ↑root)[↑root]! = 0

theorem Hex.GraphIso.Nauty.Sparse.distvals_unreachable {n : Nat} (G : SparseGraph n) (root v : Fin n) : (distvals (Graph.ofGraph G) ↑root)[↑v]! = n ↔ ¬∃ (length : Nat), Walk G root v length

theorem Hex.GraphIso.Nauty.Sparse.distvals_relabel {n : Nat} (G : SparseGraph n) (p : Perm n) (root v : Fin n) : (distvals (Graph.ofGraph (G.relabel p)) ↑root)[↑v]! = (distvals (Graph.ofGraph G) ↑(p.get root))[↑(p.get v)]!

Relabelling changes queue order but preserves all computed distances.