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

The colour of each position when classes are laid out contiguously in colour order.

Equations

• Hex.GraphIso.Nauty.sortedColorSeq G = List.flatMap (fun (c : Nat) => List.replicate (Hex.GraphIso.Nauty.colorClass G c).length c) (List.range k)

theorem Hex.GraphIso.Nauty.length_sortedColorSeq {n k : Nat} (G : Colored n k) : (sortedColorSeq G).length = n

theorem Hex.GraphIso.Nauty.mem_sortedColorSeq_lt {n k : Nat} (G : Colored n k) {c : Nat} (h : c ∈ sortedColorSeq G) : c < k

theorem Hex.GraphIso.Nauty.pairwise_sortedColorSeq {n k : Nat} (G : Colored n k) : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) (sortedColorSeq G)

theorem Hex.GraphIso.Nauty.count_sortedColorSeq {n k : Nat} (G : Colored n k) {c : Nat} (hc : c < k) : List.count c (sortedColorSeq G) = (colorClass G c).length

def Hex.GraphIso.Nauty.formOfKey {n k : Nat} (G : Colored n k) (rows : List (VSet n)) : Colored n k

The coloured graph whose adjacency is a key's rows and whose colours list G's classes contiguously. Arbitrary row bits are normalized into a simple graph: an edge needs the bit in both directions and the diagonal is dropped; on genuine keys, whose rows are symmetric and loopless, this is the identity.

Equations

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

def Hex.GraphIso.Nauty.specCanon {n k : Nat} (G : Colored n k) : Colored n k

The nauty-semantic canonical form of a coloured graph: the coloured graph determined by the rows of canonSpecKey G, with the colour classes laid out contiguously in colour order. It is defined for every input, with no certificate needed.

Equations

• Hex.GraphIso.Nauty.specCanon G = Hex.GraphIso.Nauty.formOfKey G (Hex.GraphIso.Nauty.canonSpecKey G).rows

theorem Hex.GraphIso.Nauty.colorList_formOfKey {n k : Nat} (G : Colored n k) (rows : List (VSet n)) : colorList (formOfKey G rows) = sortedColorSeq G

theorem Hex.GraphIso.Nauty.checkCanon_form_eq_formOfKey {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} {lab : Array Nat} {res : CanonResult n k} (h : checkCanon G cert B lab = some res) : res.form = formOfKey G B.rows

A checked canonical form is the form of its key.

theorem Hex.GraphIso.Nauty.checkCanon_form {n k : Nat} {G : Colored n k} {cert : CertNode} {B : Key n} {lab : Array Nat} {res : CanonResult n k} (h : checkCanon G cert B lab = some res) : res.form = specCanon G

A checked canonical form is specCanon of the input.

theorem Hex.GraphIso.Nauty.specCanon_invariant {n k : Nat} {G H : Colored n k} (hiso : Isomorphic G H) : specCanon G = specCanon H

specCanon is an isomorphism invariant: isomorphic coloured graphs have the same canonical form.