theorem Hex.GraphIso.Nauty.Sparse.canon_graph {n k : Nat} (G : Sparse.Colored n k) : (Sparse.canon G).graph = (canonSpecKey G).graph

The graph component of the total production form is the declarative maximum's graph.

def Hex.GraphIso.Nauty.Sparse.checkCanon {n k : Nat} (G : Sparse.Colored n k) (c : CertCandidate n) : Option (Sparse.CanonResult n k)

Check an untrusted key, tree and label with one sparse replay. The label must attain the key's graph and the ordered canonical colours.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.checkCanon_sound {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} {r : Sparse.CanonResult n k} (h : checkCanon G c = some r) : canonSpecKey G = c.key ∧ r.form = G.relabel r.label ∧ r.form = Sparse.canon G

Accepted certificates identify the canonical key, return an actual relabelling, and give precisely the total sparse canonical form.

theorem Hex.GraphIso.Nauty.Sparse.produceCand_canon {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} (h : produceCand G = some c) : checkCanon G c = some (Sparse.canonicalize G)

Every produced candidate passes the full result checker with the literal production label, including its tie order.

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

Produce and check the complete native sparse result. The optimized search runs once; the checker replays the supplied certificate once.

Equations

• Hex.GraphIso.Nauty.Sparse.certifyCanon? G = (Hex.GraphIso.Nauty.Sparse.produceCand G).bind (Hex.GraphIso.Nauty.Sparse.checkCanon G)

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

Unlimited certification succeeds unconditionally and agrees with the executed direct API in both its canonical form and literal label.