def Hex.GraphIso.Nauty.Sparse.Compact.usable {n : Nat} (gens : List (Perm n)) (lab ptn : Array Nat) (level : Nat) : Array (Array Nat × Array Nat)

Filter the production generators by the current ordered cells and retain their inverses for the graph-independent orbit-witness BFS. This is only a proposal filter: every emitted witness passes the sparse checker.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Compact.choose (n : Nat) (lab : Array Nat) (tc : Nat) (gens : Array (Array Nat × Array Nat)) (o : Nat) : Option (Nat × Array Nat)

Propose an earlier-to-current witness by inverting the BFS path from the current target vertex to an earlier one.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Compact.produceNode {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (gens : List (Perm n)) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → Key n → CertNode

Generate a compact proof subtree against the actual search's key. Successful witnesses prevent recursive expansion; every other target member uses the full sparse proof traversal. No dense graph is constructed.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.Compact.produceNode G tcLevel gens 0 x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = Hex.GraphIso.Nauty.Sparse.CertNode.leaf

theorem Hex.GraphIso.Nauty.Sparse.Compact.produceNode_ne_autom {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (gens : List (Perm n)) (fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (B : Key n) (earlier : Nat) (raw : Array Nat) : produceNode G tcLevel gens fuel level lab ptn active numcells B ≠ CertNode.autom earlier raw

Top-level producer records are ordinary nodes; references are only emitted inside the checked sibling context.