def Hex.GraphIso.Nauty.Sparse.rawColor {n k : Nat} (G : Sparse.Colored n k) (v : Nat) : Nat

Read a colour without requiring an inhabitant of the empty colour type.

Equations

• Hex.GraphIso.Nauty.Sparse.rawColor G v = if h : v < n then ↑G.coloring.cells[⟨v, h⟩] else 0

def Hex.GraphIso.Nauty.Sparse.colorSeq {n k : Nat} (G : Sparse.Colored n k) : List Nat

Expected canonical colours, in the actual stable bucket order. Construction takes one native colour-bucket pass and a label scan.

Equations

• Hex.GraphIso.Nauty.Sparse.colorSeq G = List.map (Hex.GraphIso.Nauty.Sparse.rawColor G) (Hex.GraphIso.Nauty.Sparse.initialPartitionWith n k G.coloring.cells.toArray Fin.val).fst.toList

def Hex.GraphIso.Nauty.Sparse.labelColors {n k : Nat} (G : Sparse.Colored n k) (l : Label n) : List Nat

The colours of a checked label in its position-to-vertex convention.

Equations

• Hex.GraphIso.Nauty.Sparse.labelColors G l = List.ofFn fun (i : Fin n) => ↑G.coloring.cells[l.get i]

theorem Hex.GraphIso.Nauty.Sparse.colorSeq_length {n k : Nat} (G : Sparse.Colored n k) : (colorSeq G).length = n

theorem Hex.GraphIso.Nauty.Sparse.colorSeq_get {n k : Nat} (G : Sparse.Colored n k) (i : Fin n) : (colorSeq G)[↑i]! = ↑(Sparse.canon G).coloring.cells[i]

The executed initializer's colour sequence has the proved canonical colour at every position. The dense projection appears only in this proof.

theorem Hex.GraphIso.Nauty.Sparse.labelColors_get {n k : Nat} (G : Sparse.Colored n k) (l : Label n) (i : Fin n) : (labelColors G l)[↑i]! = ↑(G.relabel l).coloring.cells[i]

theorem Hex.GraphIso.Nauty.Sparse.labelColors_eq {n k : Nat} (G : Sparse.Colored n k) : labelColors G (Sparse.label G) = colorSeq G

The actual production label passes the canonical-colour check.