theorem Hex.GraphIso.Nauty.Sparse.isautom_iff {n : Nat} (G : SparseGraph n) (p : Perm n) (raw : Array Nat) (hp : ∀ (i : Fin n), raw[↑i]! = ↑(p.get i)) : isautom (Graph.ofGraph G) raw = true ↔ ∀ (i j : Fin n), G.adj (p.get i) (p.get j) = G.adj i j

The executed sparse automorphism test accepts exactly the adjacency- preserving permutations. Its degree checks, reused generation marks, and fixed-vertex shortcut require no additional correctness assumptions.