theorem Hex.GraphIso.Nauty.Sparse.updatecan_sizes {n : Nat} (g : Graph n) (R : Rows n) (lab : Array Nat) (samerows : Nat) : (updatecan g R lab samerows).offsets.size = R.offsets.size ∧ (updatecan g R lab samerows).neighbors.size = R.neighbors.size

Canonical row installation changes entries in the allocated arrays; it does not resize either array, including when installing only a suffix.

theorem Hex.GraphIso.Nauty.Sparse.testcanlab_bound {n : Nat} (g : Graph n) (R : Rows n) (lab : Array Nat) : (testcanlab g R lab).snd ≤ n

The diagnostic comparison always reports a prefix length at most n. Semantic correctness of those rows additionally requires a valid store.

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.distvals_size {n : Nat} (g : Graph n) (root : Nat) : (distvals g root).size = n

Breadth-first distances use a fixed array with one slot per vertex.

theorem Hex.GraphIso.Nauty.Sparse.autom_iff_moved {n : Nat} (G : SparseGraph n) (p : Perm n) : (∀ (i j : Fin n), G.adj (p.get i) (p.get j) = G.adj i j) ↔ ∀ (i : Fin n), p.get i ≠ i → ∀ (j : Fin n), G.adj (p.get i) (p.get j) = G.adj i j

In an undirected graph it suffices to check the rows of moved vertices. Edges incident to a fixed vertex are covered by their other end; an edge with both endpoints fixed is unchanged.