structure Hex.GraphIso.Nauty.Sparse.SpecNode {n : Nat} (G : SparseGraph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : Prop

Entry invariants of the unpruned sparse tree, including the certificate that supplies equitability after the actual refinement.

• label : lab.toList.Perm (List.range n)
• node : NodeOk n level lab ptn active
• count : numcells = bcount ptn level n
• depth : level ≤ numcells
• cert : CertInv (Graph.context G) level { lab := lab, ptn := ptn, active := active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }

theorem Hex.GraphIso.Nauty.Sparse.SpecNode.refined {n : Nat} {G : SparseGraph n} {level numcells : Nat} {lab ptn : Array Nat} {active : VSet n} (h : SpecNode G level lab ptn active numcells) : have r := refine (Graph.ofGraph G) level lab ptn active numcells; SpecNode G level r.lab r.ptn r.active r.numcells ∧ Equitable (Graph.context G) level r.lab r.ptn

Executed sparse refinement preserves the tree's entry invariants and returns an equitable partition, with no equitability premise.

theorem Hex.GraphIso.Nauty.Sparse.SpecNode.child {n : Nat} {G : SparseGraph n} {level numcells : Nat} {lab ptn : Array Nat} {active : VSet n} (h : SpecNode G level lab ptn active numcells) (heq : Equitable (Graph.context G) level lab ptn) {tc len o : Nat} (hc : IsCell ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) : have c := breakout n lab ptn (level + 1) tc lab[tc + o]!; SpecNode G (level + 1) c.fst c.snd.fst c.snd.snd (numcells + 1)

Every target member supplies the complete next-node invariant through the actual rotation and singleton activation.

theorem Hex.GraphIso.Nauty.Sparse.SpecNode.initial {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; SpecNode G.graph 1 p.fst (initPtn n (n + 2) p.snd) (initActive n p.snd) p.snd.length

Actual stable colour buckets establish every nonempty root invariant.