theorem Hex.GraphIso.Nauty.certifyCanon?_isSome_zero {k : Nat} (G : Colored 0 k) : (certifyCanon? G).isSome = true

The empty graph is certified without any search.

theorem Hex.GraphIso.Nauty.certifyCanon?_isSome {n k : Nat} (G : Colored n k) : (certifyCanon? G).isSome = true

The certified canonicalization always succeeds.

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

Certificate-checked canonicalization: the search's answer, accepted through the single trusted checkCanon replay, which always succeeds.

Equations

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

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

theorem Hex.GraphIso.Nauty.certifyCanon_form {n k : Nat} (G : Colored n k) : (certifyCanon G).form = specCanon G

theorem Hex.GraphIso.Nauty.certifyCanon_relabel {n k : Nat} (G : Colored n k) : G.relabel (certifyCanon G).label = (certifyCanon G).form

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

The search agrees with the certificate-checked answer on every input.

theorem Hex.GraphIso.Nauty.searchResult?_isSome {n k : Nat} (G : Colored n k) : (searchResult? G).isSome = true

The search always answers.