theorem Hex.GraphIso.Nauty.Sparse.refine_node {n : Nat} (G : SparseGraph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (hp : lab.toList.Perm (List.range n)) (h : NodeOk n level lab ptn active) (hc : numcells = bcount ptn level n) : have r := refine (Graph.ofGraph G) level lab ptn active numcells; r.lab.toList.Perm (List.range n) ∧ NodeOk n level r.lab r.ptn r.active ∧ r.numcells = bcount r.ptn level n ∧ numcells ≤ r.numcells

Standalone sparse refinement preserves valid node data and exact counts, and never decreases the cell count.

theorem Hex.GraphIso.Nauty.Sparse.specLeaves_nonempty {n : Nat} (G : SparseGraph n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (hp : lab.toList.Perm (List.range n)) (h : NodeOk n level lab ptn active) (hc : numcells = bcount ptn level n) (hl : level ≤ numcells) (hf : n < fuel + numcells) : specLeaves G tcLevel fuel level lab ptn active numcells ≠ []

The unpruned specification cannot exhaust when its remaining recursion bound exceeds the number of possible further cell splits.

theorem Hex.GraphIso.Nauty.Sparse.rootLeaves_nonempty {n k : Nat} (G : Sparse.Colored n k) : rootLeaves G ≠ []

Every native coloured graph has an attaining leaf in the finite sparse tree, including the empty graph.