theorem Hex.GraphIso.Nauty.Sparse.Rows.Prefix.agreement {n : Nat} {R : Rows n} {H A : SparseGraph n} {count : Nat} (h : R.Prefix H count) (hcap : H.neighbors.size = A.neighbors.size) (he : ∀ (i : Fin n), ↑i < count → (A.nbrs i).toList = (H.nbrs i).toList) : R.Prefix A count

Equal rows have equal cumulative offsets. Thus a partial raw store can be reused for another graph with the same prefix and allocated edge count.

theorem Hex.GraphIso.Nauty.Sparse.testcanlab_prefix {n : Nat} (G H : SparseGraph n) (R : Rows n) (lab : Array Nat) (l : Label n) (hl : Label.ofArray? n lab = some l) (hR : R.Prefix H n) (hcap : H.neighbors.size = G.neighbors.size) : R.Prefix (G.relabel l.perm) (testcanlab (Graph.ofGraph G) R lab).snd

The returned equal-row prefix is precisely a valid installation prefix for the candidate, provided the canonical buffer has its edge capacity.

theorem Hex.GraphIso.Nauty.Sparse.testcanlab_update {n : Nat} (G : SparseGraph n) (R : Rows n) (lab : Array Nat) (l c : Label n) (hl : Label.ofArray? n lab = some l) (hR : R.Prefix (G.relabel c.perm) n) : (updatecan (Graph.ofGraph G) R lab (testcanlab (Graph.ofGraph G) R lab).snd).Prefix (G.relabel l.perm) n

Comparing against an installed canonical label supplies the exact prefix required by the executed canonical update, including for the empty graph.