def Hex.GraphIso.Nauty.Sparse.Literal.checkNode {n : Nat} (G : SparseGraph n) (tcLevel : Nat) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → CertNode → Key n → Option Bool

Replay a sparse subtree against its claimed maximum suffix. Failure is inconclusive; success records whether an actual leaf attains the bound.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.Literal.checkNode G tcLevel 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = none
• Hex.GraphIso.Nauty.Sparse.Literal.checkNode G tcLevel fuel.succ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ (Hex.GraphIso.Nauty.Sparse.CertNode.autom earlier images) x✝ = none

def Hex.GraphIso.Nauty.Sparse.Literal.checkKey {n k : Nat} (G : Sparse.Colored n k) (cert : CertNode) (B : Key n) : Bool

Check a sparse key from the actual stable ordered colour buckets. The empty input retains its unique empty label and terminal sentinel.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Literal.checkNode_eq : @checkNode = @Sparse.checkNode

Literal replay follows exactly the specification checker. Only the bounded iterator spelling changes; native sparse operations and all proof rules retain their values.

theorem Hex.GraphIso.Nauty.Sparse.Literal.checkKey_eq : @checkKey = @Sparse.checkKey

theorem Hex.GraphIso.Nauty.Sparse.Literal.checkKey_sound {n k : Nat} {G : Sparse.Colored n k} {cert : CertNode} {B : Key n} (h : checkKey G cert B = true) : canonSpecKey G = B

Kernel acceptance of the literal sparse replay identifies the full canonical key.

theorem Hex.GraphIso.Nauty.Sparse.Literal.not_isomorphic_of_checkKeys {n k : Nat} {G H : Sparse.Colored n k} {cg ch : CertNode} {bg bh : Key n} (hg : checkKey G cg bg = true) (hh : checkKey H ch bh = true) (hd : checkDiff bg bh = true) : ¬Sparse.Isomorphic G H