theorem Hex.GraphIso.Nauty.Sparse.canonlab_size {n k : Nat} (G : Sparse.Colored n k) : (runColored G).canonlab.size = n

Finishing native canonical rows retains the complete installed label.

theorem Hex.GraphIso.Nauty.Sparse.canonlab_cellsReach {n k : Nat} (G : Sparse.Colored n k) : CellsReach G.toDense (runColored G).canonlab

The returned canonical label retains every original ordered colour cell's vertices, including the empty input.

theorem Hex.GraphIso.Nauty.Sparse.canonlab_perm {n k : Nat} (G : Sparse.Colored n k) : (runColored G).canonlab.toList.Perm (List.range n)

The actual output array is a permutation, so its checked parser always succeeds. This theorem does not depend on certificate replay.

theorem Hex.GraphIso.Nauty.Sparse.canonlab_parse {n k : Nat} (G : Sparse.Colored n k) : ∃ (l : Label n), Label.ofArray? n (runColored G).canonlab = some l

theorem Hex.GraphIso.Nauty.Sparse.searchResult?_isSome {n k : Nat} (G : Sparse.Colored n k) : (searchResult? G).isSome = true

The diagnostic result succeeds unconditionally for every native sparse coloured graph. No default label or alternate search is needed.