theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_budget {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : s.Budget (splitSingleton g level split s)

A singleton pass charges each activation to its binary cell split.

theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_budget {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : s.Budget (splitNontrivial g level split s)

Accumulating neighbour counts adds no activations. The following count splits compose the same queue potential, regardless of the touched-cell order.