theorem Hex.GraphIso.Nauty.Sparse.label_colors {n k : Nat} (G : Sparse.Colored n k) {lab : Array Nat} {l : Label n} (hl : Label.ofArray? n lab = some l) (hr : CellsReach G.toDense lab) (i : Fin n) : ↑G.coloring.cells[l.get i] = (sortedColorSeq G.toDense)[↑i]!

Every parsed reachable label has the same ordered position colours.

theorem Hex.GraphIso.Nauty.Sparse.label_pair_colors {n k : Nat} (G : Sparse.Colored n k) {lab ref : Array Nat} {l c : Label n} (hl : Label.ofArray? n lab = some l) (hc : Label.ofArray? n ref = some c) (hrl : CellsReach G.toDense lab) (hrc : CellsReach G.toDense ref) (v : Fin n) : G.coloring.cells[(l.perm.comp c.perm.inv).get v] = G.coloring.cells[v]

Scattering between two reachable labels preserves the original ordered colours, independently of the adjacency proof.

theorem Hex.GraphIso.Nauty.Sparse.label_pair_iso {n k : Nat} (G : Sparse.Colored n k) {lab ref : Array Nat} {l c : Label n} (hl : Label.ofArray? n lab = some l) (hc : Label.ofArray? n ref = some c) (hrl : CellsReach G.toDense lab) (hrc : CellsReach G.toDense ref) (he : G.graph.relabel l.perm = G.graph.relabel c.perm) : Sparse.IsIso G G (l.perm.comp c.perm.inv)

Equal native leaf graphs and reachable labels give a full coloured automorphism, with the same direction as the workspace scatter.