theorem Hex.GraphIso.Nauty.Sparse.specLeaves_cellsReach {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (hp : lab.toList.Perm (List.range n)) (h : NodeOk n level lab ptn active) (hc : numcells = bcount ptn level n) (hl : level ≤ numcells) (hr : CellsReach G.toDense lab) (hcoarse : ∀ (q : Nat), (initPtn n (n + 2) (Nauty.initialPartition G.toDense).snd)[q]! ≤ 1 → ptn[q]! ≤ level) {leaf : SpecLeaf n} (hleaf : leaf ∈ specLeaves G.graph tcLevel fuel level lab ptn active numcells) : CellsReach G.toDense leaf.label.toArray

Every enumerated leaf preserves the original ordered colour classes. The induction follows every executed refinement and target rotation.

theorem Hex.GraphIso.Nauty.Sparse.rootLeaves_cellsReach {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) {leaf : SpecLeaf n} (hm : leaf ∈ rootLeaves G) : CellsReach G.toDense leaf.label.toArray

Every leaf of a nonempty coloured root has exactly the original contents in each ordered initial colour cell.

theorem Hex.GraphIso.Nauty.Sparse.canonSpecLabel_cellsReach {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : CellsReach G.toDense (canonSpecLabel G).toArray

The declarative maximum's labelling retains the ordered initial colours.

theorem Hex.GraphIso.Nauty.Sparse.canonSpecLabel_colors {n k : Nat} (G : Sparse.Colored n k) (i : Fin n) : ↑(G.relabel (canonSpecLabel G)).coloring.cells[i] = (sortedColorSeq G.toDense)[↑i]!

The declarative sparse form has the canonical sorted colour sequence, also at order zero.

theorem Hex.GraphIso.Nauty.Sparse.canonSpecKey_sorted {n k : Nat} (G : Sparse.Colored n k) (i : Fin n) : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) ((canonSpecKey G).graph.nbrs i).toList

The attaining graph has normalized, strictly increasing native rows.