def Hex.GraphIso.Sparse.canonicalize {n k : Nat} (G : Colored n k) : CanonResult n k

The native sparse search result, extracted using unconditional parser success. The proof is erased; execution retains the optimized search.

Equations

• Hex.GraphIso.Sparse.canonicalize G = (Hex.GraphIso.Nauty.Sparse.searchResult? G).get ⋯

def Hex.GraphIso.Sparse.canon {n k : Nat} (G : Colored n k) : Colored n k

Equations

• Hex.GraphIso.Sparse.canon G = (Hex.GraphIso.Sparse.canonicalize G).form

def Hex.GraphIso.Sparse.label {n k : Nat} (G : Colored n k) : Label n

Equations

• Hex.GraphIso.Sparse.label G = (Hex.GraphIso.Sparse.canonicalize G).label

theorem Hex.GraphIso.Sparse.searchResult?_eq {n k : Nat} (G : Colored n k) : Nauty.Sparse.searchResult? G = some (canonicalize G)

The diagnostic and total entrypoints return exactly the same result.

theorem Hex.GraphIso.Sparse.relabel_label {n k : Nat} (G : Colored n k) : G.relabel (label G) = canon G

theorem Hex.GraphIso.Sparse.label_parse {n k : Nat} (G : Colored n k) : Label.ofArray? n (Nauty.Sparse.runColored G).canonlab = some (label G)

The public label is parsed from the literal production output array.

theorem Hex.GraphIso.Sparse.label_toArray {n k : Nat} (G : Colored n k) : (label G).toArray = (Nauty.Sparse.runColored G).canonlab

theorem Hex.GraphIso.Sparse.canon_iso {n k : Nat} (G : Colored n k) : Isomorphic G (canon G)

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

The actual canonical output has the original sorted colour sequence.

def Hex.GraphIso.Sparse.ColorSorted {n k : Nat} (G : Colored n k) : Prop

The original ordered colour classes occupy consecutive vertices.

Equations

• Hex.GraphIso.Sparse.ColorSorted G = ∀ (i j : Fin n), i ≤ j → G.coloring.cells[i] ≤ G.coloring.cells[j]

theorem Hex.GraphIso.Sparse.colorSorted_canon {n k : Nat} (G : Colored n k) : ColorSorted (canon G)

def Hex.GraphIso.Sparse.findIso {n k : Nat} (G H : Colored n k) : Option (Perm n)

Compose the native canonical labels when the two output forms agree.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.isIso {n k : Nat} (G H : Colored n k) : Bool

Equations

• Hex.GraphIso.Sparse.isIso G H = (Hex.GraphIso.Sparse.findIso G H).isSome

theorem Hex.GraphIso.Sparse.findIso_sound {n k : Nat} {G H : Colored n k} {p : Perm n} (h : findIso G H = some p) : IsIso G H p