structure Hex.GraphIso.Nauty.Sparse.SpecLeaf (n : Nat) : Type

An unpruned leaf carries its complete refinement-code chain and the labelling that attains its normalized sparse graph.

• codes : List Nat
• label : Label n

def Hex.GraphIso.Nauty.Sparse.SpecLeaf.key {n : Nat} (G : SparseGraph n) (leaf : SpecLeaf n) : Key n

Equations

• Hex.GraphIso.Nauty.Sparse.SpecLeaf.key G leaf = { codes := leaf.codes, graph := G.relabel leaf.label.perm }

def Hex.GraphIso.Nauty.Sparse.SpecLeaf.prepend {n : Nat} (code : Nat) (leaf : SpecLeaf n) : SpecLeaf n

Equations

• Hex.GraphIso.Nauty.Sparse.SpecLeaf.prepend code leaf = { codes := code :: leaf.codes, label := leaf.label }

def Hex.GraphIso.Nauty.Sparse.specLeaves {n : Nat} (G : SparseGraph n) (tcLevel : Nat) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → List (SpecLeaf n)

The finite unpruned sparse tree. Each node executes sparse refinement, uses hint-free sparse target selection, and includes every target member. Zero fuel produces no leaf; sufficient-fuel theorems exclude that case for valid roots and descendants. No production pruning enters this definition.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.specLeaves G tcLevel 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = []

def Hex.GraphIso.Nauty.Sparse.rootLeaves {n k : Nat} (G : Sparse.Colored n k) : List (SpecLeaf n)

Enumerate the unpruned tree from the actual stable sparse colour buckets. The empty graph has the unique empty labelling and terminal sentinel.

Equations

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