theorem Hex.GraphIso.Nauty.Sparse.initialPartition_eq {n k : Nat} (G : Sparse.Colored n k) : initialPartitionWith n k G.coloring.cells.toArray Fin.val = Nauty.initialPartition G.toDense

The stable bucket loops implement the ordered-colour partition specification. The dense conversion in this statement is only a proof bridge: neither the bucket initializer nor the sparse search constructs dense adjacency.

theorem Hex.GraphIso.Nauty.Sparse.initialPartition_perm {n k : Nat} (G : Sparse.Colored n k) : (initialPartitionWith n k G.coloring.cells.toArray Fin.val).fst.toList.Perm (List.range n)

Stable bucketing neither loses nor repeats any vertex.

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.initialPartition_size {n k : Nat} (G : Sparse.Colored n k) : (initialPartitionWith n k G.coloring.cells.toArray Fin.val).fst.size = n

theorem Hex.GraphIso.Nauty.Sparse.initialPartition_sorted {n k : Nat} (G : Sparse.Colored n k) : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) (initialPartitionWith n k G.coloring.cells.toArray Fin.val).snd

theorem Hex.GraphIso.Nauty.Sparse.initialPartition_lt {n k : Nat} (G : Sparse.Colored n k) {e : Nat} (he : e ∈ (initialPartitionWith n k G.coloring.cells.toArray Fin.val).snd) : e < n

theorem Hex.GraphIso.Nauty.Sparse.initialPartition_last {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : n - 1 ∈ (initialPartitionWith n k G.coloring.cells.toArray Fin.val).snd

theorem Hex.GraphIso.Nauty.Sparse.initialPartition_count {n k : Nat} (G : Sparse.Colored n k) : (initialPartitionWith n k G.coloring.cells.toArray Fin.val).snd.length = k

The colouring is onto, so the initializer creates exactly k cells.