theorem Hex.GraphIso.Nauty.Sparse.refineWith_saturated {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) (ha : active.card ≤ numcells) : have t := refineWith g level lab ptn active numcells scratch; t.queue.isEmpty = true ∨ n ≤ t.numcells

The production refinement loop reaches one of its stopping conditions within its existing n iterations. Only the initial active-cell count bound is needed for this operational exhaustion result. Partition validity will identify the second alternative with a discrete partition.