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

Sparse replay with checked references to earlier siblings. Every ordinary record recomputes its refinement and target; references reuse only justified attainment flags, after checking the full child-partition automorphism.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Compact.checkNode_valid {n : Nat} {G : SparseGraph n} {tcLevel fuel level numcells : Nat} {lab ptn : Array Nat} {active : VSet n} {cert : CertNode} {B : Key n} {a : Bool} (hp : SpecNode G level lab ptn active numcells) (h : checkNode G tcLevel fuel level lab ptn active numcells cert B = some a) : Replay.Valid G B (specLeaves G tcLevel fuel level lab ptn active numcells) a

Accepted compact replay bounds every actual subtree leaf and records attainment exactly. The tree invariants are preserved by the literal native refinement and individualization operations.

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

Compact canonical-key replay from the actual ordered-colour initializer. An automorphism reference is invalid at the root and on the empty graph.

Equations

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

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