theorem Hex.GraphIso.Nauty.Sparse.ActiveQueue.empty {n : Nat} {active : VSet n} {queue : Array Nat} (h : ActiveQueue active queue) (he : queue.isEmpty = true) : active = VSet.empty

An exhausted sparse queue has no active splitter left.

theorem Hex.GraphIso.Nauty.Sparse.refineWith_equitable {n : Nat} (G : SparseGraph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) (hb : Scratch.Bounded n scratch) (hc : numcells = bcount ptn level n) (hinv : CertInv (Graph.context G) level { lab := lab, ptn := ptn, active := active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }) : have t := refineWith (Graph.ofGraph G) level lab ptn active numcells scratch; Equitable (Graph.context G) level t.lab t.ptn

With an accurate cell count the actual bounded sparse refinement returns an equitable partition. Both discrete and exhausted-queue exits are covered.

theorem Hex.GraphIso.Nauty.Sparse.initial_cert {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; CertInv (Graph.context G.graph) 1 { lab := p.fst, ptn := initPtn n (n + 2) p.snd, active := initActive n p.snd, numcells := p.snd.length, hint := 0, maxpos := 0, longcode := p.snd.length }

The actual sparse root supplies its certificate without a semantic assumption: every ordered colour cell is initially active.

theorem Hex.GraphIso.Nauty.Sparse.initial_equitable {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; have s := initial (Graph.ofGraph G.graph) p.fst p.snd; have t := refineWith (Graph.ofGraph G.graph) 1 s.lab s.ptn s.active p.snd.length s.canong.scratch; Equitable (Graph.context G.graph) 1 t.lab t.ptn

Root refinement is equitable for every nonempty sparse coloured graph.