theorem Hex.GraphIso.Nauty.Sparse.Walk.eq_root {n : Nat} {G : SparseGraph n} {root v : Fin n} (h : Walk G root v 0) : v = root

theorem Hex.GraphIso.Nauty.Sparse.Walk.one {n : Nat} {G : SparseGraph n} {root v : Fin n} : Walk G root v 1 ↔ G.adj root v = true

theorem Hex.GraphIso.Nauty.Sparse.Distances.adj_iff {n : Nat} {G : SparseGraph n} {root : Fin n} {dist : Array Nat} (h : Distances G root dist) (hn : 1 < n) (v : Fin n) : dist[↑v]! = 1 ↔ G.adj root v = true

For graphs with at least two vertices, distance one is exactly adjacency to the root; the unreachable sentinel cannot be mistaken for an edge.

theorem Hex.GraphIso.Nauty.Sparse.Distances.adj_congr {n : Nat} {G : SparseGraph n} {root : Fin n} {dist : Array Nat} (h : Distances G root dist) (v w : Fin n) (he : dist[↑v]! = dist[↑w]!) : G.adj root v = G.adj root w

Equal distance keys have equal adjacency to the splitter, including the one-vertex graph where every adjacency value is false.

theorem Hex.GraphIso.Nauty.Sparse.Distances.count_congr {n : Nat} {G : SparseGraph n} {root : Fin n} {dist : Array Nat} (h : Distances G root dist) (v w : Fin n) (he : dist[↑v]! = dist[↑w]!) : List.count (↑v) ((Graph.ofGraph G).row ↑root) = List.count (↑w) ((Graph.ofGraph G).row ↑root)

The semantic neighbour count into a singleton is constant on a distance class, which is the key interpretation used by the shallow distance pass.