theorem Hex.GraphIso.Nauty.Sparse.active_card {n : Nat} (active : VSet n) (ptn : Array Nat) (level : Nat) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) : active.card ≤ bcount ptn level n

Distinct active cell starts inject into the partition's cells.

theorem Hex.GraphIso.Nauty.Sparse.refineWith_stopped {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) : have t := refineWith (Graph.ofGraph G) level lab ptn active numcells scratch; t.queue.isEmpty = true ∨ discreteAt t.ptn level n = true

At every well-formed node, the executed bounded loop reaches an empty active queue or a discrete partition; its fuel cannot conceal pending work.