inductive Hex.GraphIso.Nauty.Sparse.CertNode : Type

Sparse canonical proof records. Every branch names all target positions; codes, partitions and labels are recomputed by the native sparse checker.

• leaf : CertNode
• codePrune : CertNode
• autom (earlier : Nat) (images : Array Nat) : CertNode

  Reference a strictly earlier sibling through a checked raw automorphism. The expansion checker rejects references; compact replay checks their context.

• node (children : List CertNode) : CertNode

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instReprCertNode : Repr CertNode

Equations

• Hex.GraphIso.Nauty.Sparse.instReprCertNode = { reprPrec := Hex.GraphIso.Nauty.Sparse.instReprCertNode.repr }

partial def Hex.GraphIso.Nauty.Sparse.instReprCertNode.repr : CertNode → Nat → Std.Format

def Hex.GraphIso.Nauty.Sparse.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.checkNode G tcLevel 0 x✝⁶ x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = none
• Hex.GraphIso.Nauty.Sparse.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.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.