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

Produce proof records from the same stable colour buckets as the native sparse search. The claimed key is supplied by that search.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.canonSpecKey_zero {n k : Nat} {G : Sparse.Colored n k} (hn : n = 0) : canonSpecKey G = { codes := [codeSentinel], graph := G.graph }

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

With no logical limit, a root certificate always replays against the actual declarative maximum, including order zero.