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

Compute the canonical form of a coloured graph together with the label producing it: the checked-label transcription of the pinned nauty search. Total; worst-case cost is factorial. Its answer is the one the certificate replay validates (canonicalize_eq_certifyCanon), which is how every theorem below reaches it.

Equations

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

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

The canonical form of a coloured graph.

Equations

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

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

The label producing the canonical form.

Equations

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

theorem Hex.GraphIso.canonicalize_eq_certifyCanon {n k : Nat} (G : Colored n k) : canonicalize G = Nauty.certifyCanon G

The transcription's answer is the certificate-checked one.

theorem Hex.GraphIso.canon_eq_specCanon {n k : Nat} (G : Colored n k) : canon G = Nauty.specCanon G

The canonical form is the declarative specification form.

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

Relabelling by the canonical label produces the canonical form.

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

The canonical form has contiguous colour cells in their original order.

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

Every coloured graph is isomorphic to its canonical form.

theorem Hex.GraphIso.canon_invariant {n k : Nat} {G H : Colored n k} (h : Isomorphic G H) : canon G = canon H

Isomorphic coloured graphs have equal canonical forms.

theorem Hex.GraphIso.iso_iff_canon_eq {n k : Nat} (G H : Colored n k) : Isomorphic G H ↔ canon G = canon H

Two coloured graphs are isomorphic exactly when their canonical forms are equal. The biconditional compares canonical coloured graphs, not the labels: label arrays refer to different input vertex names and generally differ for isomorphic inputs.

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

Find one isomorphism from G to H when one exists: the forward transporter through the two canonical forms, the canonical label of H composed with the inverse of the canonical label of G (in forward permutation convention).

Equations

• Hex.GraphIso.findIso G H = if Hex.GraphIso.canon G = Hex.GraphIso.canon H then some ((Hex.GraphIso.label H).toPerm.inv.comp (Hex.GraphIso.label G).toPerm) else none

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

The Boolean isomorphism decision.

Equations

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

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

Soundness of the search: any permutation it returns really is an isomorphism. This is the theorem to use after a successful findIso. It says nothing about the none case, for which see findIso_isSome_iff.

theorem Hex.GraphIso.findIso_isSome_iff {n k : Nat} (G H : Colored n k) : (findIso G H).isSome = true ↔ Isomorphic G H

Completeness of the search: it returns a permutation exactly when one exists. Together with findIso_sound this makes findIso a decision procedure rather than a one-sided test.

theorem Hex.GraphIso.isIso_eq_true_iff {n k : Nat} (G H : Colored n k) : isIso G H = true ↔ Isomorphic G H

The decision answers true exactly on isomorphic pairs.

theorem Hex.GraphIso.isIso_eq_false_iff {n k : Nat} (G H : Colored n k) : isIso G H = false ↔ ¬Isomorphic G H

The decision answers false exactly on non-isomorphic pairs. This is the negative direction the graph_iso tactic needs, and it is a genuine refutation rather than a failure to find a witness.

theorem Hex.GraphIso.isomorphic_of_isIso {n k : Nat} {G H : Colored n k} (h : isIso G H = true) : Isomorphic G H

A positive answer proves isomorphism.