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

Package a compact canonical certificate with a checked attaining label. One replay validates the key; graph and ordered-colour checks validate the label.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Compact.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

theorem Hex.GraphIso.Nauty.Sparse.Compact.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)

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

Compact certification preserves the production key and literal label from one optimized search and validates them with one sparse replay.

Equations

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

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