def Hex.GraphIso.Nauty.Sparse.Compact.produceRoot {n k : Nat} (G : Sparse.Colored n k) (gens : List (Perm n)) (B : Key n) : CertNode

Produce a compact root certificate from native stable colour buckets. The generator list supplies proposals, all checked before pruning.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceRoot_replays {n k : Nat} (G : Sparse.Colored n k) (gens : List (Perm n)) : checkKey G (produceRoot G gens (canonSpecKey G)) (canonSpecKey G) = true

Unlimited compact root production succeeds, even without usable generators. Full expansion supplies every branch without a checked witness.

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

Run the optimized search once, retaining its key, literal label and generator trace. Expand only those proof subtrees lacking checked witnesses.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceCand_eq {n k : Nat} (G : Sparse.Colored n k) : produceCand G = some { tree := produceRoot G (runColored G).generators (canonSpecKey G), key := canonSpecKey G, lab := (runColored G).canonlab }

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceCand_isSome {n k : Nat} (G : Sparse.Colored n k) : (produceCand G).isSome = true

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceCand_replays {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} (h : produceCand G = some c) : checkKey G c.tree c.key = true

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceCand_key {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} (h : produceCand G = some c) : c.key = canonSpecKey G

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceCand_label {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} (h : produceCand G = some c) : c.lab = (runColored G).canonlab

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

Equations

• Hex.GraphIso.Nauty.Sparse.Compact.validateKey? G c = if Hex.GraphIso.Nauty.Sparse.Compact.checkKey G c.tree c.key = true then some c.key else none

theorem Hex.GraphIso.Nauty.Sparse.Compact.validateKey?_sound {n k : Nat} {G : Sparse.Colored n k} {c : CertCandidate n} {B : Key n} (h : validateKey? G c = some B) : canonSpecKey G = B

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

Produce and replay a compact sparse canonical-key certificate.

Equations

• Hex.GraphIso.Nauty.Sparse.Compact.certifyKey? G = (Hex.GraphIso.Nauty.Sparse.Compact.produceCand G).bind (Hex.GraphIso.Nauty.Sparse.Compact.validateKey? G)

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