def
Hex.GraphIso.Nauty.Sparse.Compact.produceRoot
{n k : Nat}
(G : Sparse.Colored n k)
(gens : List (Perm n))
(B : Key n)
:
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.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Compact.produceRoot_replays
{n k : Nat}
(G : Sparse.Colored n k)
(gens : List (Perm n))
:
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.
Instances For
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_replays
{n k : Nat}
{G : Sparse.Colored n k}
{c : CertCandidate n}
(h : produceCand G = some c)
:
theorem
Hex.GraphIso.Nauty.Sparse.Compact.produceCand_key
{n k : Nat}
{G : Sparse.Colored n k}
{c : CertCandidate n}
(h : produceCand G = some c)
:
theorem
Hex.GraphIso.Nauty.Sparse.Compact.produceCand_label
{n k : Nat}
{G : Sparse.Colored n k}
{c : CertCandidate n}
(h : produceCand G = some c)
:
def
Hex.GraphIso.Nauty.Sparse.Compact.validateKey?
{n k : Nat}
(G : Sparse.Colored n k)
(c : CertCandidate n)
:
Equations
Instances For
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)
:
Produce and replay a compact sparse canonical-key certificate.