structure Hex.GraphIso.Nauty.Sparse.RefineSt.Budget {n : Nat} (s t : RefineSt n) : Prop

Each new queue entry is charged to a new partition cell. This potential does not require an a priori bound on the number of refinement passes.

• cells : s.numcells ≤ t.numcells
• queue : t.queue.size + s.numcells ≤ s.queue.size + t.numcells

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Budget.refl {n : Nat} (s : RefineSt n) : s.Budget s

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Budget.trans {n : Nat} {s t u : RefineSt n} (h : s.Budget t) (k : t.Budget u) : s.Budget u

theorem Hex.GraphIso.Nauty.Sparse.CountSort.finish_budget {n : Nat} (level first last : Nat) (distance : Bool) (s : RefineSt n) (w1 v2 w2 v3 : Nat) : s.Budget (finish level first last distance s w1 v2 w2 v3)

Installing count fragments adds at most one activation per new cell, including replacement of the largest inactive fragment.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_budget {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) : s.Budget (splitCounts level first distance s)

The complete count splitter adds at most one activation per new cell.